Journal R&D

CortexWall C-Refine — vérifié machine

La session CortexWall_C_Refine comprend 27 théories Isabelle/HOL structurées en 3 couches, totalisant 3 896 lignes et 477 lemmes prouvés mécaniquement. Zéro sorry, zéro oops, zéro admitted.

Session PRISM v43 — Journal d’audit cryptographique

La seule preuve formelle complète d’un micro-noyau au monde

seL4 (Secure Embedded L4) est un micro-noyau développé par l’équipe Trustworthy Systems de Data61/CSIRO (ex-NICTA, UNSW Sydney). Il possède la preuve formelle complète la plus ambitieuse jamais réalisée pour un système d’exploitation : ~480 000 lignes de preuve Isabelle/HOL couvrant spécification abstraite, design exécutable, code C et code binaire ARM.

Propriétés prouvées par seL4 : isolation mémoire entre processus (aucun processus ne peut accéder à la mémoire d’un autre sans capability explicite), intégrité du noyau (le code noyau ne peut pas être modifié par le userspace), confidentialité des flux d’information (non-interférence entre domaines de sécurité différents), raffinement complet du code C vers la spécification abstraite.

Ce que CORTEX hérite de seL4 : l’isolation matérielle des domaines TCB et hors-TCB, le système de capabilities qui empêche tout composant non autorisé d’accéder aux interfaces TCB, et la garantie que le noyau lui-même ne peut pas être corrompu par un composant applicatif. CortexWall modélise explicitement cette frontière seL4 dans CortexWall_seL4_Config.thy (I13 : capabilities CDL → DOM_HIGH, exhaustion complète).

CORTEX ne reprouve pas seL4. La preuve est héritée de la seL4 Foundation et maintenue par l’équipe Trustworthy Systems. C’est explicitement documenté comme hypothèse de base dans le Security Target (ASE_REQ).

234/234 lemmes — 0 écart

Chaque invariant est prouvé formellement en Isabelle/HOL et lié à un fichier source identifié.

SENTINEL compromis par RCE — impact ?

« Si SENTINEL est compromis par exécution de code arbitraire (RCE), peut-il forcer OMEGA à prendre une décision incorrecte ? »

SENTINEL est hors-TCB, confiné par seL4 dans un domaine de capabilities restreint. NBC-1 prouve qu’un composant non-TCB ne peut pas appeler les interfaces internes TCB. NBC-3 prouve qu’aucun canal non autorisé ne traverse la frontière TCB. NBC-5 prouve que le TCB reste isolé et auto-protégé tant qu’il est actif et intègre. NBC-8 prouve la non-interférence forte : les actions HIGH ne sont pas observables par LOW.

Au pire : SENTINEL ne remonte plus d’alertes → OMEGA fonctionne en mode dégradé (moins d’information), pas en mode compromis (mauvaises décisions).

Tous les modules seront testés

Le CFVL ne se limite pas au TCB. Chaque module de CORTEX ORIGIN™ — de M00 à M32 — fera l’objet de tests et de vérifications par le laboratoire. Le niveau de rigueur est adapté à la criticité du composant.

Principe fondamental : un composant hors-TCB compromis ne doit jamais pouvoir briser les propriétés de sécurité du système. C’est garanti par seL4 + NBC. Mais le CFVL vérifie aussi que chaque module remplit correctement sa fonction propre : SENTINEL détecte bien les menaces, AEGIS exécute bien les réponses graduées, EcoFlux respecte bien les budgets énergétiques, etc. La sécurité architecturale (prouvée) ne dispense pas de la qualité fonctionnelle (testée).

Arrêt d’urgence vérifié formellement

Le module M09 CircuitBreaker™ (KillSwitch) a été porté de Python v17 vers C11 et soumis à une évaluation complète par le CFVL. FSM 3 états : IDLE → ARMED → TRIPPED (terminal irréversible). Couche Safety-Critical, hors TCB, confiné par seL4.

8 propriétés de sécurité vérifiées (P1–P8)

Rapport complet : CFVL-EVAL-005 v1.1 (23 sections, 947 LOC code source en annexe). Inclut Security Target extrait ASE, threat model formel A1–A6, traçabilité THR→OBJ→Fonction→Preuve→Test, justification cryptographique, analyse side-channel 5 canaux, et analyse de vulnérabilité AVA_VAN enrichie (8 types).
CBMC total TCB + M09 : 298 + 463 = 761 propriétés formelles, 0 échec.

3 couches + PRISM — de preuve

Noyau — 6 théories · 745 lignes · 91 lemmes

Phase 1 — 13 théories · 1 777 lignes · 270 lemmes

Isar structuré — 8 théories · 1 499 lignes · 144 lemmes

PRISM v43 — 1 théorie · 2 549 lignes · 215 lemmes

215 lemmes · 215 prouvés · 0 sorry · 0 obligation ouverte. Session indépendante. Finished PRISM (0:00:05 elapsed).

Note : abs_hash est une fonction déterministe à dépendance forte au timestamp. Ce n’est pas une fonction injective au sens cryptographique strict (collision non triviale sous hypothèses bornées).

Transparence sur les limites

Conformément au principe de transparence du CFVL, les lacunes connues sont explicitement documentées. Un rapport lucide est plus crédible qu’un rapport parfait.

Note : « proof-grade EAL6/EAL7 » signifie que l’architecture, les preuves formelles (692 lemmes Isabelle + 157 Coq, 0 obligation ouverte) et la traçabilité sont alignées sur les exigences CC EAL6–EAL7. La certification Critères Communs / CSPN n’a pas encore été réalisée en laboratoire (CESTI/CB). La preuve du microkernel seL4 est héritée de seL4 Foundation — CORTEX ne la reprouve pas.

CFVL-DOC-003 · Journal R&D · Version 2.4 · 10 mars 2026