Axes scientifiques
Programmes de recherche en méthodes formelles appliquées aux architectures gouvernées. Le CFVL s’inscrit dans la continuité des travaux fondateurs en vérification formelle de systèmes critiques.
Méthodes formelles appliquées
Le CFVL s’inscrit dans la continuité des travaux issus de la tradition LCF (Edinburgh/Cambridge), du programme de vérification seL4 (UNSW/Data61), des frameworks de raffinement Isabelle/HOL, de CompCert (INRIA) et de HACL*/F* (MSR/INRIA).
Quatre axes structurants
AXE 01 — Architectures gouvernées
Formalisation des propriétés d’isolation, non-interférence, non-contournement, gouvernance décisionnelle et survie à compromission partielle. Application aux composants TCB de CORTEX ORIGIN™.
AXE 02 — Bornage du TCB
Réduction du périmètre de confiance, exhaustion des capabilities, preuve de non-escalade de privilège, théorèmes de survie. Minimisation formelle de la surface d’attaque.
AXE 03 — Chaîne multi-niveaux
Spécification abstraite → raffinement concret → implémentation vérifiée → compilation vérifiée. Relation de simulation prouvée entre chaque niveau. Pont AutoCorres Isabelle → C.
AXE 04 — Programmes ouverts
Vérification protocolaire, extension MLS dynamique, propriétés décisionnelles IA gouvernée, analyse side-channel, modélisation adversariale. Frontière de la recherche formelle appliquée à l’IA.
Frontières de la recherche
Gouvernance IA formellement prouvée
Peut-on prouver formellement qu’un système d’IA gouverné ne peut pas prendre de décision autonome sans validation humaine explicite ? Formalisation de la propriété « human-in-the-loop » au niveau du modèle de transition.
Survie cryptographique post-quantique
Les propriétés d’intégrité de PRISM™ résistent-elles à un adversaire disposant d’un ordinateur quantique ? Modélisation formelle de la menace et analyse des primitives cryptographiques utilisées.
Composition de preuves
Comment combiner les preuves individuelles de chaque composant (M00, OMEGA™, PRISM™) en une preuve système globale ? Théorie de la composition sécurisée pour architectures hiérarchisées.
CFVL-REC-001 · Axes scientifiques · Version 1.0 · Février 2026