Laboratoire interne de
vérification formelle
Cellule indépendante dédiée à la vérification formelle de systèmes logiciels critiques. Le CFVL ne développe pas de produit. Il analyse, valide ou invalide les systèmes qui lui sont soumis. Un avis négatif du CFVL bloque la validation du périmètre évalué.
Le CFVL exerce une mission
de vérification indépendante
Sa mission est méthodologique et normative. Un avis négatif du CFVL bloque la validation du périmètre évalué, indépendamment de toute contrainte commerciale ou calendaire.
Preuves machine
Produire des preuves formelles reproductibles, vérifiées mécaniquement par des noyaux de confiance.
Évaluation de couverture
Vérifier que chaque exigence de sécurité est couverte par au moins un théorème prouvé.
Documentation des lacunes
Identifier et publier explicitement ce qui n’a pas pu être vérifié, avec la même rigueur que les résultats.
Avis formel
Émettre un verdict : Conforme, Conforme avec réserves, ou Non conforme. Chaque avis engage le laboratoire.
Validation machine,
pas validation humaine
L’autorité du laboratoire ne repose pas sur une signature humaine. Elle repose sur un verdict machine reproductible.
Outils référencés par le CFVL — 21 outils, 6 catégories
Types de tests appliqués
en pré-évaluation CSPN
Le pipeline haute assurance du CFVL applique six familles de vérification complémentaires, couvrant les exigences AVA, ATE, ADV et ALC des Critères Communs (ISO 15408).
Preuves machine (ADV_SPM)
Absence d’erreurs (ADV_IMP)
Validation fonctionnelle (ATE_FUN)
Résistance aux attaques (AVA_VAN)
Conformité FIPS 202 (ADV_FSP)
Canaux auxiliaires (AVA_VAN)
Règles non négociables
Indépendance
Le CFVL peut déclarer un livrable non conforme, sans recours hiérarchique sur le périmètre formel évalué. Aucune release ne peut être publiée sous avis négatif.
Zéro compromis formel
Aucune preuve incomplète n’est acceptée. Aucune lacune n’est dissimulée. 0 sorry, 0 Admitted, 0 timeout, 0 FAIL — invariant vérifié à chaque évaluation.
Reproductibilité
Toute validation peut être reproduite par un tiers disposant des outils et versions documentés. Le CFVL fournit les commandes, les temps attendus, et les résultats attendus.
Transparence
Les hypothèses, les limites du modèle et les lacunes de couverture sont explicitement publiées dans chaque rapport. Un rapport lucide est plus crédible qu’un rapport parfait.
Une évaluation standardisée
Lorsqu’un système ou un composant est soumis au CFVL, le processus suivant s’applique — indépendamment de la nature ou de l’origine du livrable.
Réception
Le livrable est soumis avec sa spécification, ses preuves, et l’identification de version (tag + hash).
Recompilation
Toutes les preuves sont recompilées avec les versions d’outils documentées. Vérification que les sessions terminent sans erreur.
Vérification des invariants
Tous les invariants déclarés sont vérifiés mécaniquement : 0 sorry, 0 Admitted, 0 FAIL, 0 timeout.
Couverture des exigences
Chaque exigence de sécurité (SFR) est tracée vers au moins un théorème prouvé. La cartographie est produite.
Documentation des lacunes
Ce qui n’est pas couvert est explicitement documenté : lacunes, hypothèses non vérifiables, simplifications.
Avis formel
Le CFVL émet son avis : Conforme, Conforme avec réserves, ou Non conforme.
Rapport signé
Rapport d’évaluation engageant le CFVL, version taggée, SHA-256 documenté.
Recherche appliquée en méthodes formelles
Le CFVL s’inscrit dans la continuité des travaux issus de la tradition LCF, du programme de vérification seL4, des frameworks de raffinement Isabelle/HOL, de CompCert (INRIA) et de HACL*/F* (MSR/INRIA).
Architectures gouvernées
Formalisation des propriétés d’isolation, non-interférence, non-contournement, gouvernance décisionnelle et survie à compromission partielle.
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.
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.
Programmes ouverts
Vérification protocolaire, extension MLS dynamique, propriétés décisionnelles IA gouvernée, analyse side-channel, modélisation adversariale.
Un modèle de maturité en trois phases
L’indépendance de validation est garantie dès la phase initiale par les moteurs formels LCF, indépendamment de la structure organisationnelle.
Cohérence fondatrice
Validation par noyaux LCF. Corpus formel consolidé. Indépendance machine garantie.
● EN COURSSéparation fonctionnelle
Ingénieur formel senior. Revue croisée développement / validation. Élimination du biais de modélisation.
◯ PLANIFIÉValidation externe
Support à audit tiers (CESTI / ANSSI). Séparation complète développeur / évaluateur.
◯ PLANIFIÉDeux catégories distinctes
Les documents institutionnels décrivent le laboratoire. Les rapports d’évaluation évaluent les systèmes soumis. Cette séparation est un principe structurant.
Collaborations & partenariats
Le CFVL est ouvert aux collaborations académiques avec les laboratoires en méthodes formelles, sécurité systèmes, compilation vérifiée et cryptographie formelle.
CIFRE
Conventions industrielles de formation par la recherche
Co-encadrement
Doctorats et post-doctorats en méthodes formelles
Publications
Articles et communications conjoints
ANR / France 2030
Appels à projets recherche appliquée