← CFVL · Document institutionnel
Publications & communications
Catalogue des publications internes, rapports d’évaluation et communications scientifiques du CFVL.
Les publications formelles sont versionnées, signées et archivées PRISM™.
35
Évaluations
2
Terminées
5
En cours
28
Planifiées
📚 Catalogue — Publications du laboratoire
Le CFVL produit deux types de documents : les documents institutionnels (qui décrivent le laboratoire) et les rapports d’évaluation (qui évaluent les composants). Cette page référence l’ensemble du corpus.
Documents institutionnels — Cadre du laboratoire
CFVL-DOC-001
Charte
Identité, mission, principes directeurs, gouvernance, périmètre de validation.
v1.0 · Fév. 2026
CFVL-DOC-002
Méthodologie
Outils, critères d’acceptation, seuils de rejet, processus d’évaluation.
v1.0 · Fév. 2026
CFVL-DOC-003
Journal R&D
Verrous scientifiques, résultats, échecs, décisions techniques.
v1.0 · Fév. 2026
CFVL-DOC-004
Template rapport
Structure standard des rapports d’évaluation formelle.
v1.0 · Fév. 2026
📋 Rapports d’évaluation — Évaluations formelles
Les rapports d’évaluation sont émis à chaque cycle de validation d’un composant. Ils sont versionnés, signés et archivés dans le journal PRISM™. Le CFVL évalue tous les modules de CORTEX ORIGIN™ — le niveau de rigueur est adapté à la criticité du composant.
✅ CFVL-EVAL-001 — OMEGA™ PolicyForge v2.0 (M10) DTE COMPLET
Dossier technique d’évaluation complet — CEM v3.1 R5 clause-par-clause — Template CFVL 42/42 — Prêt soumission CESTI/ANSSI
100%
TSF Proof (161/161 WP)
20/21
SAR Verdicts PASS
167
Isabelle lemmas · 0 sorry
12
Coq Qed · 0 Admitted
171
Tests PASS (3 compilers)
42/42
Template CFVL
Dossier d’évaluation (8 documents) :
CFVL-EVAL-001 v8.0
Rapport maître intégré
1055§ · 8 parties · 19 sections
CFVL-EVAL-001-ST v2.0
Security Target CEM
ASE complet · 9 SFR · matrices bidirectionnelles
CFVL-EVAL-002
Guide opérationnel
AGD_OPE.1
CFVL-EVAL-003
Guide préparatoire
AGD_PRE.1
CFVL-EVAL-004 v2.0
Vulnérabilités AVA_VAN.5
5 éliminées · 3 BEYOND HIGH (57 pts)
CFVL-EVAL-005
Spéc. fonctionnelle ADV_FSP.5
6 TSFI · Semi-formal + Formal
CFVL-EVAL-006
Politique CM ALC_CMC.5
Git signé · Docker · FLR · MANIFEST
Synthèse CODIR
Executive Summary
3 pages · Go/No-Go · 170-275K€ · 14-26 mois
| Classe | Composants SAR | Verdict |
|---|---|---|
| ASE | INT + CCL + SPD + OBJ + REQ + TSS | PASS (6/6) |
| ADV | ARC.1 + FSP.5 + IMP.2 + INT.3 + SPM.1 + TDS.5 | PASS (6/6) |
| ALC | CMC.5 + CMS.5 + DEL.1 + DVS.2 + FLR.3 + LCD.1 + TAT.3 | PASS (7/7) |
| ATE | COV.3 + DPT.4 + FUN.2 | PASS (3/3) |
| ATE | IND.2 | ⏳ Attente CESTI |
| AVA | VAN.5 | PASS |
| AGD | OPE.1 + PRE.1 | PASS (2/2) |
Avis formel : CONFORME · Signé : D. Salomon · Date : 1er mars 2026 · Archivé : PRISM-CFVL-2026-001
✅ CFVL-EVAL-002 — PRISM™ v2.0 (M02) DTE COMPLET
Dossier technique d’évaluation complet — CEM clause-by-clause — ISO/IEC 15408:2022 + ISO/IEC 18045:2022 — EAL6+ (ALC_FLR.3) — Prêt soumission CESTI/ANSSI
100%
TSF Proof (281/281 WP)
23/23
Coq Qed · 0 Admitted
155
Isabelle lemmas · 36 sorry/crypto
63
Tests PASS (3 compilers)
442
LOC C11 · CompCert 3.14
2236§
Rapport · 25 sections · 9 appendices
Dossier d’évaluation (rapport maître intégré) :
CFVL-EVAL-002 v3.0 Final
Rapport maître intégré EAL6+
2236§ · 25 sections · 9 appendices · 63 KB
Contenu intégré : Voix évaluateur CEM · Evidence Pack verbatim · TOE Boundary & TCB Definition · Crypto Axiom Register (Amendement C.01) · Tool Qualification Procedure · RTE/UB Analysis · Formal Refinement Chain ADV · Reproducibility Guide + MANIFEST SHA-256
| Classe | Composants SAR | Verdict |
|---|---|---|
| ADV | ARC.1 + FSP.6 + IMP.2 + TDS.5 | PASS (4/4) |
| ALC | CMC.5 + DVS.2 + FLR.3 | PASS (3/3) |
| ATE | FUN.2 | PASS |
| ATE | IND.2 | ⏳ Attente CESTI |
| AVA | VAN.5 | PASS |
| Formal Verif. | WP 281/281 + Isabelle 155 + Coq 23/23 | PASS |
Avis formel : CONFORME (PRELIMINARY — pending CESTI) · Signé : CFVL · Date : 1er mars 2026 · Archivé : PRISM-CFVL-2026-002
🔒 Couche TCB — Preuve formelle
Composants dont la compromission briserait les propriétés de sécurité.
CFVL-EVAL-001 — OMEGA™ PolicyForge v2.0 (M10)
✅ TERMINÉE
Point de passage décisionnel unique · BLP MAC 4 niveaux · ~490 LOC C · DTE complet CEM v3.1 R5
8 documents · 1055§ · 20/21 SAR PASS · TSF 161/161 (100%) · Isabelle 167 lemmas · Coq 12 Qed · CompCert 3.17 · AVA_VAN.5 34/34 PASS
CFVL-EVAL-002 — PRISM™ v2.0 (M02)
✅ TERMINÉE
Journal cryptographique immuable · Chaîne SHA-256 append-only · Module M02 du TCB CortexWall · DTE complet EAL6+ (ALC_FLR.3)
DTE complet v3.0 · 2236§ · 281/281 WP TSF · 155 Isabelle · 23 Coq Qed · 0 Admitted · CompCert 3.14 · 63 tests · ASan/UBSan 0 · Evidence Pack · Formal Refinement Chain
CFVL-EVAL-003 — M00 Kernel Cortex
● EN COURS
Bootstrap & isolation · Root of Trust · fail-closed gate
6 TH Coq + TCB.thy · I1/I2/I3/I4 — Reste : raffinement C, tests d’intégration seL4
seL4 : Preuve héritée de seL4 Foundation (Data61/UNSW). CORTEX ne la reprouve pas. Le CFVL vérifie l’intégration et la configuration capabilities (I13 : CDL → DOM_HIGH).
⚡ Couche Safety-Critical — Preuve partielle + tests
Composants critiques confinés par seL4.
CFVL-EVAL-004 — M05 Kernel exécutif
○ PLANIFIÉ
Fonctions critiques couvertes par seL4+M00
CFVL-EVAL-005 — M09 CircuitBreaker™
● EN COURS
Arrêt d’urgence, escalade automatique
QEMU PASS (cortex-killswitch) — Reste : Frama-C/WP, tests injection de fautes, MC/DC
🛡️ Couche Sécurité & Orchestration — Tests + confinement
Composants hors-TCB, confinés par seL4.
CFVL-EVAL-006 — M01 SENTINEL™
○ PLANIFIÉ
Sécurité active, qualification risque
CFVL-EVAL-007 — M03 ATLAS™
○ PLANIFIÉ
Analyse & corrélation (proposal-only)
CFVL-EVAL-008 — M08 AEGIS™
○ PLANIFIÉ
Exécution contrôlée, réponse graduée
CFVL-EVAL-009 — M11 TrustLink™
● EN COURS
Chaîne de confiance inter-composants
QEMU PASS (cortex-trustlink) — Reste : tests unitaires, fuzzing, scénarios d’attaque
CFVL-EVAL-010 — M17 Scheduler™
○ PLANIFIÉ
Ordonnancement déterministe
CFVL-EVAL-011 — M26 AVA™ / AVA-CPL™
● EN COURS
Analyse de vulnérabilités
100 théorèmes, 0 Admitted (ava_cpl) — Reste : tests d’intégration, rapport CFVL
CFVL-EVAL-012 — M27 InterfaceGateway™
● EN COURS
Passerelle d’interface, filtrage
QEMU PASS (cortical-gateway) — Reste : tests filtrage, scénarios non-escalade
CFVL-EVAL-013 — M27bis NAVI™
○ PLANIFIÉ
Interface non décisionnelle
🔄 Couche Résilience & Conformité — Tests fonctionnels + conformité
Composants hors-TCB, confinés par seL4.
CFVL-EVAL-014 — M13 Recovery™
○ PLANIFIÉ
Récupération, DR snapshot/restore
CFVL-EVAL-015 — M14 ResilienceManager™
○ PLANIFIÉ
Gestion de résilience, basculement
CFVL-EVAL-016 — M16 EcoFlux™
○ PLANIFIÉ
Gouvernance énergétique, frugalité
CFVL-EVAL-017 — M19 ArtifactStore™
○ PLANIFIÉ
Stockage d’artefacts, intégrité
CFVL-EVAL-018 — M20 MemoryCore™
○ PLANIFIÉ
Mémoire persistante, isolement
CFVL-EVAL-019 — M21 LearningLimiter™
○ PLANIFIÉ
Limiteur d’apprentissage
CFVL-EVAL-020 — M22 DataBoundary™
○ PLANIFIÉ
Frontière de données, classification
CFVL-EVAL-021 — M23 ComplianceMonitor™
○ PLANIFIÉ
Conformité NIS2/ACPR/ECB
CFVL-EVAL-022 — M24 Offline™
○ PLANIFIÉ
Mode déconnecté
CFVL-EVAL-023 — M25 AuditFreeze™
○ PLANIFIÉ
Gel d’audit, preuve d’intégrité
CFVL-EVAL-024 — M28 DeploymentGuard™
○ PLANIFIÉ
Garde de déploiement, rollback
CFVL-EVAL-025 — M29 QuotaManager™
○ PLANIFIÉ
Token bucket, sliding window, DoS protection
CFVL-EVAL-026 — M30 HealthMonitor™
○ PLANIFIÉ
Surveillance santé, timeout, préemption
CFVL-EVAL-027 — M31 AlertManager™
○ PLANIFIÉ
Alertes, déduplication, cycle de vie
CFVL-EVAL-028 — M32 ProofExporter™
○ PLANIFIÉ
Export preuves, chaîne de hachage, gzip, signature
🤖 Couche Orchestration IA — Tests + gouvernance
Composants d’orchestration LCM, hors-TCB.
CFVL-EVAL-029 — Multi-LCM / TRM Engine™
○ PLANIFIÉ
Orchestration IA gouvernée
CFVL-EVAL-030 — TRM Contrain Nano™
○ PLANIFIÉ
Contrainte LCM temps réel
CFVL-EVAL-031 — RAG™
○ PLANIFIÉ
Enrichissement de contexte gouverné
CFVL-EVAL-032 — WALL-DOME™
○ PLANIFIÉ
Confinement & isolation runtime
CFVL-EVAL-033 — MIRROR LAB™
○ PLANIFIÉ
Simulation environnement contrôlé
CFVL-EVAL-034 — MORPH GATES™
○ PLANIFIÉ
Passerelles adaptatives
CFVL-EVAL-035 — CHAMELEON™
○ PLANIFIÉ
Adaptation dynamique
Template CFVL-DOC-004 : Chaque rapport CFVL-EVAL suit la structure standard : identification, périmètre, SFR applicables, cartographie SFR→théorèmes, résultats de vérification, lacunes, avis (Conforme / Avec réserves / Non conforme), métadonnées (tag Git, SHA-256, versions outils). Tous les rapports sont archivés dans PRISM™.
📊 Avancement des évaluations
Estimation de l’avancement des évaluations en cours et terminées, basée sur les preuves formelles existantes et les jalons restants pour chaque couche de criticité.
Couche TCB — Preuve formelle complète
Spec abstraite → raffinement → code C → rapport CFVL signé
| Éval | Module | Preuves existantes | Reste à produire | Avancement |
|---|---|---|---|---|
| EVAL-001 | OMEGA™ (M10) | DTE complet v8.0 · 161/161 WP TSF · 167 Isabelle · 12 Coq Qed · CompCert 3.17 · 171 tests · AVA 34/34 · 42/42 template · 8 documents | ATE_IND.2 (CESTI uniquement) | ✅ 100% |
| EVAL-002 | PRISM™ v2.0 (M02) | DTE complet v3.0 · 281/281 WP TSF · 155 Isabelle · 23 Coq Qed · 0 Admitted · CompCert 3.14 · 63 tests · ASan/UBSan 0 · 2236§ · Evidence Pack · Formal Refinement Chain | ATE_IND.2 (CESTI uniquement) | ✅ 100% |
| EVAL-003 | M00 Kernel Cortex | 6 TH Coq + TCB.thy · I1/I2/I3/I4 | Raffinement C, tests d’intégration seL4 | ~50% |
Couche Safety-Critical — Preuve partielle + tests robustesse
Frama-C/WP, tests structurels, injection de fautes, MC/DC
| Éval | Module | Preuves existantes | Reste à produire | Avancement |
|---|---|---|---|---|
| EVAL-005 | M09 CircuitBreaker™ | QEMU PASS (cortex-killswitch) | Frama-C/WP, tests injection de fautes, MC/DC | ~30% |
Couche Sécurité & Orchestration — Tests + confinement seL4
Tests unitaires, fuzzing, scénarios d’attaque, non-escalade
| Éval | Module | Preuves existantes | Reste à produire | Avancement |
|---|---|---|---|---|
| EVAL-009 | M11 TrustLink™ | QEMU PASS (cortex-trustlink) | Tests unitaires, fuzzing, scénarios d’attaque | ~30% |
| EVAL-011 | M26 AVA™ / AVA-CPL™ | 100 théorèmes, 0 Admitted (ava_cpl) | Tests d’intégration, rapport CFVL | ~65% |
| EVAL-012 | M27 InterfaceGateway™ | QEMU PASS (cortical-gateway) | Tests filtrage, scénarios non-escalade | ~30% |
Les pourcentages sont des estimations internes basées sur le ratio preuves existantes / jalons requis pour la couche de criticité concernée. Ils ne constituent pas un engagement contractuel. L’avancement est réévalué à chaque cycle de validation.