Méthodologie formelle
Outils, critères d’acceptation, seuils de rejet et processus d’évaluation du CFVL. Ce document définit comment une évaluation est conduite et ce qui constitue un résultat acceptable.
Vérification formelle mécanisée
Le CFVL s’appuie exclusivement sur des méthodes de vérification formelle mécanisée — c’est-à-dire des preuves vérifiées par un noyau de confiance logiciel (kernel LCF), et non par un humain seul.
Cette approche se distingue de l’audit conventionnel, de la revue de code manuelle et des tests : elle ne cherche pas à trouver des bugs, mais à prouver leur absence pour un ensemble de propriétés formellement spécifiées.
Une preuve formelle peut démontrer l’absence d’une classe entière de défauts.
Stack de vérification
Chaque outil est sélectionné pour son noyau de confiance (LCF kernel), sa maturité industrielle et sa compatibilité avec les composants cibles.
Isabelle/HOL
Proof assistant principal. Noyau LCF vérifié. Utilisé pour les preuves de raffinement, non-interférence et propriétés d’isolation (tradition seL4/L4.verified).
PRIMAIRECoq
Proof assistant complémentaire. Calcul des constructions inductives. Extraction de code certifié. Utilisé pour les propriétés algorithmiques et cryptographiques.
PRIMAIREFrama-C / WP
Vérification de code C par preuve déductive (plugin WP + SMT solvers). Contrats ACSL. Cible : implémentations bas niveau des composants TCB.
PRIMAIRETLA+ / TLC
Model checker pour les propriétés de systèmes concurrents. Spécification de protocoles de gouvernance et propriétés de vivacité.
COMPLÉMENTAIRECompCert
Compilateur C formellement vérifié (INRIA). Garantie que la compilation ne casse pas les propriétés prouvées au niveau source.
INTÉGRATIONProVerif / Tamarin
Vérification automatique de protocoles cryptographiques. Propriétés de confidentialité, authenticité, non-rejouabilité.
COMPLÉMENTAIRESeuils de conformité
Un livrable est évalué selon les critères suivants. Tout manquement entraîne un avis « Non conforme » ou « Conforme avec réserves ».
Complétude des preuves
Toutes les sessions de preuve terminent sans erreur. Invariant strict : 0 sorry (Isabelle), 0 Admitted (Coq), 0 timeout, 0 FAIL. Aucune preuve partielle n’est acceptée.
Couverture SFR
Chaque exigence de sécurité fonctionnelle (Security Functional Requirement) doit être tracée vers au moins un théorème formellement prouvé. La cartographie SFR → théorèmes est obligatoire.
Reproductibilité
Le build de vérification doit être reproductible bit-à-bit avec les versions d’outils documentées. Le CFVL publie les commandes exactes, les hash SHA-256 des artefacts et les temps de compilation de référence.
Documentation des lacunes
Ce qui n’est pas couvert est explicitement documenté : hypothèses non vérifiables, simplifications du modèle, propriétés hors périmètre. Le rapport est transparent sur ce qu’il ne prouve pas.
Version taggée
Le livrable évalué doit être identifié par un tag Git unique et un hash SHA-256. Le rapport d’évaluation est lié à cette version précise — aucune rétroactivité.
Sept étapes standardisées
Ce processus 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é. Archivage PRISM™.
Trois verdicts possibles
Conforme
Toutes les propriétés de sécurité déclarées sont formellement prouvées. Couverture SFR complète. Aucune lacune non documentée. Le livrable peut être intégré dans le cycle de release.
Conforme avec réserves
Les propriétés principales sont prouvées, mais des lacunes identifiées subsistent. Les réserves sont explicitement listées avec un plan de remédiation. Intégration possible sous conditions documentées.
Non conforme
Des preuves échouent, sont incomplètes ou absentes. Le livrable ne peut pas être intégré. Aucune release sous avis négatif. Un nouveau cycle d’évaluation est requis après correction.
CFVL-DOC-002 · Méthodologie · Version 1.0 · Février 2026