CORTEX NK™ — le socle de confiance borné
L’Intel Inside de la confiance cyber et IA souveraine.
COUVERTURE CRYPTO 9,5/10 · auto-évaluation CFVL · 16 primitives BINAIRE prouvées CT ET benchmarkées · HQC 🇫🇷 inclus
Cortex NK™ est un composant logiciel de confiance à périmètre borné — un noyau minimaliste, cloisonné et cryptographiquement agile, destiné à sécuriser l’exécution des fonctions critiques d’un système IA ou cyber et à porter une trajectoire de certification haute assurance EAL7. Stack crypto à 16 primitives formellement prouvées CT au niveau binaire (SHA-256/512 · HMAC · ChaCha20-Poly1305 · HKDF · SHA-3 · BLAKE2b · X25519 · Ed25519 · FrodoKEM-64 PQC), dont les 12 primitives du TCB cryptographique re-prouvées CT sur la toolchain de production exacte (gcc-O2 bare-metal). Ces 16 primitives sont aussi toutes benchmarkées en performance (implémentation HACL*), complétées par 8 primitives PQC/référence mesurées via liboqs (ML-KEM · ML-DSA · SLH-DSA · BIKE · HQC 🇫🇷). Il ne s’installe pas à la place de votre système — il s’installe en-dessous, comme racine de confiance.
2 287 LOC
TCB minimal · audit cloc reproductible
0,90 ns
Réaction TCB · best-case
10 538
Théorèmes Isabelle/HOL · 0 sorry
16 BINAIRE
Primitives crypto prouvées CT
12/12
TCB cryptographique · CT sur toolchain de prod
72 +
Preuves Binsec/Rel cross-arch
1 804/1 804
Frama-C/WP Module 14 · 100 %
2 305
CBMC · 0 failure
442
Tests E2E PASS cumulés
16,7 Mds+
Fuzzing NK · 48 h · 0 crash
9,5/10
Couverture crypto · auto-évaluation CFVL
99,90 %
Palier formel ferme
5 modules
TCB livrés · 4 PRs mergées + 1 en cours
20 700 lignes
Évidence formelle CT/NI · 20 661 artéfacts vérifiés
98,1 %
TCB strict · 4 modules Frama-C/WP ≥ 96 %
Ce que personne d’autre ne documente publiquement
Une série de résultats de pointe documentés et vérifiables en data room. À notre connaissance, CORTEX NK™ est le seul micronoyau crypto à combiner preuves CT au binaire, modules TCB applicatifs prouvés, orchestrations multi-modules et vérification PQC indépendante (ML-KEM-768, FrodoKEM-640) — parmi les projets publiquement documentés.
FrodoKEM CT au binaire — n=64 → prod 640
Preuve formelle de Constant-Time au niveau binaire de FrodoKEM : d’abord sur la variante de test n=64 (BINSEC-036, mai 2026), puis au paramètre de production FrodoKEM-640 NIST L1 (BINSEC-045). La comparaison FO ciblée par l’attaque Guo-Johansson-Nilsson 2020 est confirmée CT sur le binaire de prod. Vérification indépendante, complémentaire des travaux Formosa/libcrux côté ML-KEM. Hors TCB cryptographique BL2.
CFVL-BINSEC-036 / 045 · hors TCB BL2
X25519 ECDH binaire CT
Preuve formelle de Constant-Time au niveau binaire de X25519 (Elliptic Curve Diffie-Hellman), standard de facto pour TLS 1.3, WireGuard, Signal, SSH. Cross-architecture (Sprint 85.2), re-prouvé sur la toolchain de production exacte — BINSEC-041 COMPLETE, gcc-O2 bare-metal.
CFVL-BINSEC-030 / 041 · toolchain prod
Orchestration QUINTET NIVEAU 7-D
Première orchestration formellement prouvée CT de 5 modules TCB simultanés publiquement documentée, à notre connaissance (mesh + ipc_stub + audit_log + chacha_sodium + pqc_stack) avec 6 SECRETs distincts, convergence ARM64/x86-64 Δ=0 parfaite. Aucun concurrent connu ne documente plus de 2 modules.
CFVL-BINSEC-035 · Sprint 87 · 24 mai 2026
-O2 production-grade × 4 primitives
Preuve CT au binaire sous optimisation -O2 agressive sur 4 primitives critiques — SHA-256, HMAC-SHA-256, Poly1305, ChaCha20 — sans équivalent publié connu. CT préservée sous vectorisation NEON/AVX2. Argument production-grade direct.
CFVL-BINSEC-031/034 · Sprint 86 · 26 mai 2026
Secure Boot post-quantique S1-S10
À notre connaissance, première chaîne Secure Boot post-quantique formellement vérifiée publiquement documentée. Signature hybride Ed25519 + ML-DSA-87 (FIPS 204). Boot composé 0,55 ms · orchestré 1,51 ms. 211/211 tests E2E PASS · 6 théorèmes Isabelle/HOL.
CFVL-BENCH-SECBOOT-001 v2.0 · PR #16 · 21 mai 2026
Audit Log applicatif HMAC chaîné
À notre connaissance, premier journal d’audit applicatif formellement vérifié publiquement documenté, intégrant le chaînage cryptographique HMAC-SHA256 (HACL*), l’ancrage TPM 2.0 PCR, et la propriété anti-tamper formellement prouvée. Append 1,50 µs.
CFVL-EVAL-NK-AUDIT-001 v1.0 · PR #18 · 22 mai 2026
Auto-Containment Mémoire monotone
À notre connaissance, première couche d’auto-confinement au-dessus du MMU formellement prouvée publiquement documentée. Quarantaine mémoire monotone, journal cryptographique immuable, invariants structurels. MTTD moyen 18,76 ns · 339/339 Frama-C/WP (100%).
CFVL-BENCH-CONTAINMENT-001 v1.0 · PR #17 · 22 mai 2026
Mesh attestation PQC AND-strict
À notre connaissance, premier module d’attestation distante applicatif publiquement documenté combinant signature hybride AND-strict Ed25519 + ML-DSA-87 et preuve formelle complète de la propriété quantum-safe (2 théorèmes HOL dédiés). Vérification 137 ns.
CFVL-EVAL-NK-MESH-001 v1.0 · PR #19 · 24 mai 2026
La couverture crypto la plus large documentée publiquement
Comparaison par couverture crypto effective au niveau binaire — la métrique discriminante pour les systèmes critiques applicatifs — en auto-évaluation CFVL sur sources publiques. Sur cette grille, CORTEX NK™ devance le N°2 (EverCrypt) de 2,5 points en combinant primitives binaire CT, modules TCB application, orchestrations multi-modules et PQC.
| Rang | Projet | Score | Primitives BINAIRE | Modules TCB | Orchestration | PQC binaire | ECDH binaire |
|---|---|---|---|---|---|---|---|
| 1 🏆 | CORTEX NK 🇫🇷 France | 9,5/10 | 16 | 5 (NIV 7-D) | 5 | ✓ FrodoKEM-64 | ✓ X25519 |
| 2 | EverCrypt 🇺🇸 MSR | 7/10 | 15+ (F* logique) | 0 | 0 | ✗ | ✗ |
| 2 | Galois SAW 🇺🇸 USA | 7/10 | 8-12 binaire | quelques | partielle | ✗ | ✗ |
| 4 | HACL* (F*) 🇺🇸/🇫🇷 MSR/INRIA | 6/10 | 15+ (F* logique) | 0 | 0 | ✗ | ✗ |
| 5 | WolfSSL Cryptol 🇺🇸 | 4/10 | 3-5 binaire | minimal | 0 | ✗ | ✗ |
| 6 | BoringSSL 🇺🇸 Google | 2/10 | 0 (tests seulement) | 0 | 0 | ✗ | ✗ |
| 7 | seL4 🇦🇺 Linux Found. | 1/10 | 0 (hors crypto) | microkernel only | N/A | ✗ | ✗ |
| 8 | OpenSSL FIPS 🇺🇸 | 1/10 | 0 (tests seulement) | 0 | 0 | ✗ | ✗ |
| 9 | CompCert 🇫🇷 INRIA | 0/10 | 0 (hors crypto) | compilateur only | N/A | ✗ | ✗ |
Cinq problèmes qu’aucun système classique ne résout
Les systèmes d’exploitation traditionnels présentent une surface d’attaque trop large, des dépendances complexes et des privilèges trop élevés. Cortex NK™ ramène la sécurité à sa base — empêcher qu’une compromission locale devienne systémique.
Surface d’attaque excessive
Trop de code, trop de privilèges. Une faille devient escalade de privilèges, puis ransomware,
puis persistance furtive. Cortex NK™ ramène le TCB à 2 287 lignes de code C auditées
— soit près de quatre fois moins que seL4, le micronoyau de référence mondial. Audit
reproductible via cloc.
Isolation forte, séparation stricte.
Zero Trust théorique
La plupart des architectures Zero Trust reposent encore sur des composants permissifs. Cortex NK™ apporte un Zero Trust by Architecture — chaque composant isolé, authentifié, et limité à son strict périmètre.
Propagation des compromissions
Une machine compromise propage le risque à tout le SI. Cortex NK™ isole les couches critiques : une intrusion locale reste locale. Pas d’élévation, pas de mouvement latéral, pas d’exfiltration en masse. Module Auto-Containment monotone formellement prouvé (PR #17).
Confiance des systèmes critiques
Comment prouver qu’un composant critique est fiable ? Cortex NK™ sert de socle de confiance logiciel auditable et formellement vérifié — défense, santé, industrie, spatial, énergie, souveraineté numérique. 10 538 théorèmes Isabelle/HOL · 0 sorry.
Menace post-quantique
Les ordinateurs quantiques rendront caduques RSA et ECC dans la décennie. Avec ML-KEM, ML-DSA, SLH-DSA, BIKE et HQC-256 (INRIA France) mesuré à 4,72 ms intégrés via liboqs, + FrodoKEM-640 et ML-KEM-768 vérifiés CT au binaire (vérification indépendante, hors TCB), Cortex NK™ est résilient face à l’ère quantique — dès aujourd’hui.
Anatomie d’un Trusted Assurance Core
Cortex NK™ s’articule en quatre couches fonctionnelles, conçues pour être indépendamment vérifiables et certifiables. Chaque couche réduit drastiquement la surface d’attaque de la précédente, et l’ensemble constitue le socle de confiance de Cortex ORIGIN™.
Core Trust Layer
Noyau de confiance
Micro-noyau / separation kernel — isolation stricte des processus critiques, segmentation forte des privilèges, exécution déterministe, surface d’attaque minimisée. Trusted Computing Base ultra-réduit. Modèle de capabilities prouvé formellement (10 500 théorèmes Isabelle/HOL fondamentaux).
Crypto Assurance Layer
Cryptographie souveraine
16 primitives crypto BINAIRE prouvées CT (HACL* via CTPass + Binsec/Rel), dont les 12 du TCB cryptographique re-prouvées sur la toolchain de production exacte ; ces 16 sont aussi toutes benchmarkées en performance (HACL*), + 8 primitives mesurées via liboqs/libsodium (incluant HQC 🇫🇷). Agilité cryptographique : bascule d’algorithme sans redémarrage. PQC de production vérifié CT au binaire (FrodoKEM-640, ML-KEM-768 par noyaux), en vérification indépendante hors TCB.
Secure AI Runtime
Exécution sécurisée IA
La couche différenciante du programme Cortex. Confinement des agents IA, segmentation mémoire (Auto-Containment monotone prouvé, PR #17), contrôle d’intégrité, exécution sous politiques de confiance, auditabilité native (Audit Log HMAC chaîné, PR #18) — une IA qui tourne dans un environnement sécurisé par design.
Assurance Layer
Gouvernance & preuve
Journalisation immuable (Audit Log HMAC-SHA256 chaîné), preuve d’intégrité cryptographique, application des politiques de sécurité (Mesh attestation PQC hybride AND-strict, PR #19), observabilité, conformité réglementaire. C’est cette couche qui rend Cortex NK™ auditable et certifiable — NIS2, LPM, EAL.
Cortex NK™ s’installe en-dessous
Cortex NK™ n’est pas un logiciel utilisateur final. C’est une couche de confiance que l’on pose sous ou autour de composants critiques. Trois modèles d’installation, selon le niveau d’assurance recherché et la contrainte du parc existant.
Niveau 1 · Haute assurance
Sous l’OS / Micro-noyau
Cortex NK™ agit comme Root of Trust logiciel, en-dessous du système d’exploitation hôte. Modèle réservé aux environnements à plus haute exigence : défense, gouvernement, santé critique, finance sensible, infrastructures vitales.
Niveau 2 · Go-to-market
Runtime sécurisé au-dessus de l’OS
Déploiement plus simple sur serveurs, cloud privé, machines virtuelles, edge ou appliances cyber. Permet cloisonnement, contrôle d’intégrité et exécution sécurisée sans bouleverser l’infrastructure existante. Modèle privilégié pour démarrer.
Niveau 3 · Embarqué
Firmware / Edge
Approche adaptée aux environnements industriels, robotique, drones, IoT critique ou médical. Faible empreinte, faible surface d’attaque, forte isolation — exactement ce qu’un noyau minimaliste sait offrir.
Trois niveaux. Une assurance.
Ceinture et bretelles. Prouver le présent (Niveau 1), garantir le futur (Niveau 2), assurer la souveraineté (Niveau 3). La seule stack à triple niveau combinant preuves CT binaires (HACL*) et benchmarks PQC NIST (liboqs), à notre connaissance.
Niv. 1 — Résistance classique
Aujourd’hui · binaire CT prouvé
Primitives BINAIRE prouvées CT (HACL*)
SHA-256/512 · HMAC · ChaCha20-Poly1305 · HKDF · SHA-3 · BLAKE2b · X25519 · Ed25519
Sécurité
F*/Vale + Binsec/Rel · 0 violation CT · 0 fuite · 0 crash · 72+ preuves cross-arch
Immunisé contre les erreurs de programmation et attaques par canaux temporels. Preuve formelle au niveau BINAIRE (pas seulement F* logique).
Niv. 2 — Post-quantique NIST
2030+ · benchmark perf
Primitives benchmarkées (liboqs 0.10.1)
ML-KEM-1024 (FIPS 203) · ML-DSA-87 (FIPS 204) · SLH-DSA-256s (FIPS 205)
Sécurité
Standards mondiaux NIST · Niveau sécurité L5 · benchmarks mesurés réellement
Secrets d’État protégés contre les futurs ordinateurs quantiques. Données collectées aujourd’hui, illisibles demain. + FrodoKEM-640 prouvé CT au binaire (n=64 → 640 de production) et ML-KEM-768 vérifié par noyaux — vérification indépendante, hors TCB.
Niv. 3 — Souveraineté France 🇫🇷
Assurance-vie souveraine
Primitives Round 4 NIST (liboqs)
HQC-256 (INRIA France 🇫🇷) — mesuré 4 720,30 µs · BIKE-L3 — mesuré 1 326,91 µs
Sécurité
Mathématiques distinctes (code-based). Si Kyber est cassé, la France reste protégée.
Ceinture ET bretelles. 100 % souverain. Pépite française INRIA/UVSQ. Aucun concurrent connu ne mesure HQC dans son TCB.
Niv. 1 : prouver le présent (CT binaire) · Niv. 2 : garantir le futur (PQC NIST) · Niv. 3 : assurer la souveraineté (HQC 🇫🇷)
Du classique au post-quantique, preuves et performance
16 primitives BINAIRE prouvées CT (HACL* via CTPass + Binsec/Rel)
Preuves formelles de Constant-Time au niveau binaire ARM64 + x86-64 via Binsec/Rel. Méthodologie CT-slice + composition stricte HACL*. Reproductibilité en data room / sur demande.
| Primitive | Sprint / CFVL | Usage prod réel | Statut |
|---|---|---|---|
| SHA-256 (1 bloc) | 65 / BINSEC-009 | TLS, JWT, signatures | UTILISÉE |
| SHA-256 multi-bloc (4 bl.) | 83 / BINSEC-025 | Hachage volumes | UTILISÉE |
| HMAC-SHA-256 | 66 / BINSEC-010 | TLS, JWT, capability MAC | UTILISÉE |
| Poly1305-32 | 67 / BINSEC-011 | AEAD authentication | UTILISÉE |
| ChaCha20 | 68 / BINSEC-012 | Chiffrement flux (TLS, WireGuard) | UTILISÉE |
| ChaCha20-Poly1305 AEAD | 79 / BINSEC-022 | TLS 1.3, WireGuard, Signal | UTILISÉE |
| HKDF-extract / SHA-256 | 70 / BINSEC-014 | Dérivation clés TLS 1.3 | UTILISÉE |
| HKDF-expand / SHA-256 | 77-B / BINSEC-021 | Dérivation clés TLS 1.3 | UTILISÉE |
| SHA-3 / Keccak-256 | 69 / BINSEC-013 | Ethereum, NIST SP 800-185 | CATALOGUE |
| SHA-512 (2 blocs) | 84 / BINSEC-027 | RFC 6234, certificats | CATALOGUE |
| HMAC-SHA-512 | 84 / BINSEC-028 | IPsec, signatures longues | CATALOGUE |
| HMAC-BLAKE2b-32 | 83 / BINSEC-026 | Argon2, WireGuard | CATALOGUE |
| HKDF-expand / SHA-512 | 85.1 / BINSEC-029 | KDF haute sécurité | CATALOGUE |
| Ed25519 SIGN 🔒 | 89 / BINSEC-039 | Secure Boot, signatures TLS / JWT | ✓ TOOLCHAIN PROD |
| X25519 ECDH ⭐ | 85.2 / BINSEC-030 / 041 | TLS 1.3, WireGuard, Signal, SSH | ✓ TOOLCHAIN PROD |
| FrodoKEM-64 KEM 🔬 | 88 / BINSEC-036 | Recherche · variante test PQC | CT BINAIRE (n=64) |
16 primitives prouvées CT — toutes benchmarkées (impl HACL*)
Performance de l’implémentation HACL* — celle prouvée CT ci-dessus — sur Apple Silicon M2 · clang -O2 · CLOCK_MONOTONIC_RAW · warmup 1 000 + 10 000 mesures · mean / p99. FrodoKEM au paramètre de production 640. Réf. CFVL-BENCH-CT16-001 v0.1, vérifiable en data room.
| Primitive (impl HACL*) | Entrée | mean | p99 |
|---|---|---|---|
| SHA-256 | 64 B | 485 ns | 625 ns |
| SHA-256 (4 blocs) | 256 B | 1 196 ns | 1 459 ns |
| SHA-512 (2 blocs) | 128 B | 588 ns | 666 ns |
| SHA3-256 | 64 B | 764 ns | 834 ns |
| HMAC-SHA-256 | 64 B | 1 022 ns | 1 084 ns |
| HMAC-SHA-512 | 64 B | 968 ns | 1 041 ns |
| HMAC-BLAKE2b | 64 B | 593 ns | 667 ns |
| Poly1305 | 64 B | 72 ns | 125 ns |
| ChaCha20 | 1 KiB | 1 437 ns | 1 542 ns |
| ChaCha20-Poly1305 enc | 1 KiB | 2 228 ns | 2 292 ns |
| HKDF-extract / SHA-256 | 32 B | 709 ns | 750 ns |
| HKDF-expand / SHA-256 | 32→32 B | 717 ns | 791 ns |
| HKDF-expand / SHA-512 | 32→32 B | 933 ns | 1 000 ns |
| Ed25519 sign | msg 32 B | 38,33 µs | 56,46 µs |
| X25519 scalarmult | 1 op | 26,82 µs | 36,25 µs |
| FrodoKEM-640 keygen · hors TCB | n=640 | 1 233 µs | 1 414 µs |
| FrodoKEM-640 encaps · hors TCB | n=640 | 1 367 µs | 1 458 µs |
| FrodoKEM-640 decaps · hors TCB | n=640 | 1 360 µs | 1 466 µs |
+ 8 références mesurées (liboqs / libsodium · dont 5 PQC)
Mesures performance temporelle réelles sur Apple Silicon · clang -O2 · N=1000 · CLOCK_MONOTONIC_RAW · mean/p50/p95/p99. liboqs 0.10.1 + libsodium. Standards FIPS 203/204/205 + Round 4 NIST (BIKE, HQC).
| Primitive | Standard | Mesure |
|---|---|---|
| ChaCha20-Poly1305 encrypt 64B | RFC 8439 · libsodium | 310,90 ns |
| HMAC-SHA256 64B input | RFC 2104 · libsodium | 2 787,50 ns |
| HKDF-SHA256 Extract+Expand 32B | RFC 5869 | 3 805,84 ns |
| ML-KEM-1024 encaps | FIPS 203 · NIST PQC | 29,45 µs |
| ML-DSA-87 sign | FIPS 204 · NIST PQC | 494,96 µs |
| BIKE-L3 encaps | Round 4 · diversification | 1 326,91 µs |
| HQC-256 🇫🇷 encaps | Round 4 · INRIA France | 4 720,30 µs |
| SLH-DSA-256s sign | FIPS 205 · réserve ultime | 481,94 ms |
PQC de production — vérification CT au binaire (hors TCB)
Au-delà du TCB cryptographique, CORTEX a vérifié au binaire ARM64 (toolchain de production exacte) les noyaux sensibles au secret des KEM post-quantiques de sa stack (ML-KEM-768, ML-KEM-1024, FrodoKEM-640), par analyse Binsec/Rel indépendante. Étude complémentaire — hors TCB BL2, qui reste à 12/12.
| KEM post-quantique | Périmètre vérifié | Résultat (binaire ARM64 prod) | Réf. CFVL |
|---|---|---|---|
| ML-KEM-768 (FIPS 203) | Noyaux secret-sensibles — NTT/inv-NTT, réductions Montgomery/Barrett, CBD, compress/decompress, basemul, couture FO (verify + cmov) | 9 noyaux SECURE + couture FO SECURE au binaire + basemul clos par décomposition · SHAKE/SHA3 admis · 0 alerte |
043/044 · COMPO-001/002 |
| ML-KEM-1024 (FIPS 203 · L5) | Mêmes noyaux que 768 — invariance paramétrique prouvée (sources byte-identiques, K = borne publique) | Couture FO (1568 o) re-mesurée SECURE + basemul SECURE · 9 noyaux hérités · 0 alerte | MLKEM1024-001 |
| FrodoKEM-640 (niveau L1 · alternate) | 6 noyaux secret-sensibles — comparaison FO (ct_verify/ct_select), échantillonnage gaussien CDF, pack/unpack, add/sub, matmul | 6 noyaux CT — 5 SECURE au binaire + matmul clos par décomposition · correctif GJN-2020 · 0 alerte |
045 · FRODO-002 |
fixed_bound_loop_ct /
seq_compose_ct)
est désormais machine-prouvée en Isabelle/HOL 2025-2 (0 sorry, build-certifié) ; la liaison au binaire (corps CT, bornes publiques, adressage data-indépendant) reste établie par BINSEC par-noyaux + inspection. Seul résiduel sur ML-KEM : SHAKE/SHA3 admis CT par construction Keccak
(non vérifié au binaire). Ces travaux sont complémentaires des preuves publiées par
Formosa-Crypto (ML-KEM CT jusqu’à l’assembleur via le compilateur certifié Jasmin) et libcrux
(ML-KEM en Rust vérifié) — sans revendication d’antériorité absolue. ML-KEM est le standard FIPS 203 ;
FrodoKEM-640 est un alternate conservateur de défense-en-profondeur (non standardisé NIST). Rapports
CFVL-BINSEC-MLKEM-COMPO-001/002, CFVL-BINSEC-MLKEM1024-001,
CFVL-BINSEC-FRODO-002 et synthèses disponibles en data room.
16
Primitives BINAIRE prouvées CT
HACL* + CTPass + Binsec/Rel
12/12
TCB crypto · toolchain de prod
gcc-O2 bare-metal · BINSEC-039/040/041
16
Primitives prouvées CT benchmarkées
perf HACL* · + 8 réf liboqs/sodium
3
Standards NIST FIPS
203 · 204 · 205
🇫🇷
Souveraineté France
HQC INRIA · CEA Frama-C
Couverture PQC — état mesuré et trajectoire
Lecture synthétique de la couverture Constant-Time au binaire des primitives post-quantiques. Ce qui est mesuré ne se confond jamais avec ce qui est visé. Toutes ces primitives sont hors TCB BL2 — le TCB cryptographique reste 12/12, prouvé CT bout-en-bout sur la toolchain de production exacte.
| Algorithme | Standard / niveau | Bench | CT au binaire (BINSEC/Rel) | Statut |
|---|---|---|---|---|
| TCB crypto BL2 · 12 prim. | symétrique + ECC (HACL*) | ✓ | ✓ 12/12 bout-en-bout · toolchain prod exacte | DANS le TCB |
| ML-KEM-768 | FIPS 203 · L3 | ✓ | ✓ par décomposition · couture FO + 9 noyaux + basemul au binaire | hors TCB · prod |
| ML-KEM-1024 | FIPS 203 · L5 | ✓ | ✓ par décomposition · héritage paramétrique prouvé + FO 1568 re-mesurée | hors TCB · prod |
| FrodoKEM-640 | niveau L1 · alternate | ✓ | ✓ 6/6 par décomposition · matmul clos · correctif GJN-2020 | hors TCB · prod |
| ML-DSA-87 | FIPS 204 · L5 | ✓ | ◐ CT vis-à-vis de la clé secrète · noyaux arith. (NTT, c·s) SECURE au binaire · rejet = modèle de fuite documenté · SHAKE admis | hors TCB · mesuré |
| HQC-256 🇫🇷 | sélectionné NIST 2025 | ✓ | ○ non mesuré | preuve/stub |
✓ complet · « par décomposition » = noyau interne prouvé SECURE au binaire + composition structurelle (règle de composition machine-prouvée en Isabelle/HOL 2025-2, 0 sorry build-certifié ; liaison au binaire via BINSEC + inspection) · ◐ partiel (CT vis-à-vis du secret de long terme, sans temps constant) · ○ pas encore mesuré. Résiduel commun ML-KEM : SHAKE/SHA3 admis CT par construction Keccak. Travaux complémentaires de Formosa-Crypto (Jasmin → assembleur) et libcrux (Rust vérifié) — sans revendication d’antériorité absolue.
Trajectoire crypto — cinq chantiers
Chaque case verte de la matrice est adossée à un rapport CFVL-BINSEC-* nommé et reproductible. Quatre chantiers clos, un parqué (HQC).
20 661 lignes d’évidence CT/NI
L’évidence formelle Non-Interférence (Constant-Time) regroupe l’ensemble des artéfacts produits par la campagne Binsec/Rel cross-architecture ARM64 + x86-64 sur les primitives crypto HACL*. Chaque preuve est reproductible : code C harness, script Binsec, sortie vérifiée, rapport CFVL associé.
Chaque ligne est versionnée Git, chaque preuve est rejouable. Méthode CT-slice + composition formelle HACL* via Binsec/Rel. Toolchain documentée.
ARM64 (aarch64-linux-musl) + x86-64 (x86_64-linux-musl) — chaque primitive prouvée sur les deux architectures avec convergence Δ documentée.
Sprint 88 a introduit la méthode « calibrage progressif depth » (50K → 4M) appliquée à la vérification CT au binaire de FrodoKEM (n=64, puis paramètre de production 640).
Évidence disponible en data room / sur demande · calcul lignes wc -l reproductible · snapshot campagne Sprints 65-88. Évidence étendue depuis (non incluse dans ce total) : BINSEC-039/040/041 (TCB cryptographique re-prouvé sur toolchain de prod), 042 (Ed25519 verify), 043/044/045 (PQC de production ML-KEM-768 + FrodoKEM-640), documentée séparément.
Cinq modules formellement vérifiés
Chaque module CORTEX NK™ a été livré complet avec preuves Frama-C/WP, théorèmes Isabelle/HOL, tests E2E et benchmarks evidence-grade.
Module Secure Boot S1-S10
Chaîne de boot post-quantique avec signature hybride Ed25519 + ML-DSA-87 (FIPS 204), manifest signé, extension PCR TPM 2.0 réel (TSS2), anti-rollback et recovery avec ancrage NV. Boot composé 0,55 ms · orchestré 1,51 ms.
Module Auto-Containment Mémoire
Quarantaine mémoire monotone formellement prouvée. Journal cryptographique immuable, invariants structurels permanents. MTTD moyen 18,76 ns · 339/339 Frama-C/WP (100%) · 6/6 Isabelle/HOL (0 sorry).
Module Audit Log Immuable
Journal cryptographique chaîné via HMAC-SHA256 HACL* (INRIA Prosecco). Ancrage TPM 2.0 PCR. Propriété anti-tamper formellement prouvée. Append 1,50 µs · 426/443 Frama-C/WP (96,2%) · 8 théorèmes HOL.
Module Mesh v1 PQC hybride
Attestation distante hybride AND-strict Ed25519 + ML-DSA-87. Propriété PQC quantum-safe formellement prouvée par 2 théorèmes HOL dédiés. Vérification 137 ns · 4 partitions formellement vérifiées · 18 thm HOL · 76,5% WP.
Module 17 TCB · Crypto Layer
16 primitives crypto BINAIRE prouvées CT (Sprints 65-94) avec composition stricte HACL*, dont les 12 du TCB cryptographique re-prouvées sur la toolchain de production exacte. 5 orchestrations NIVEAU 7-B/7-C/7-D (jusqu’à QUINTET 5 modules). PQC de production vérifié CT au binaire hors TCB (ML-KEM-768, FrodoKEM-640).
Récap formel cumulé
10 538 théorèmes Isabelle/HOL · 0 sorry (10 500 fondamentaux + 39 modules). 3 450+ goals Frama-C/WP (76-100% selon module). 2 305 vérifications CBMC · 0 failure. 442 tests E2E PASS cumulés. Évidence disponible en data room.
Quatre modules du TCB strict ≥ 96 % WP
Au-delà des 5 modules d’évaluation publiés en mai (PR #16-#19), le Sprint S82 du 2 juin 2026 étend la couverture Frama-C/WP au TCB strict du micronoyau — les fonctions qui partagent les privilèges du noyau. Quatre modules consécutifs ≥ 96 %, méthode reproductible, infrastructure ACSL crypto cumulative (14 sections d’axiomes réutilisables).
Méthode S82 validée sur 3 sprints consécutifs. Extraction des blocs
combinatoires (memcpy, state updates, HMAC compute/verify) dans des helpers static
axiomatisés sous #ifdef __FRAMAC__
via extern
+ #define.
Frame ACSL ciblé → élimination de la combinatoire SMT.
Correction silent-skip mailbox. La couverture initiale du module (86,5 %)
masquait un silent-skip de Frama-C 32 sur les #define
dans annotations ACSL. Réécriture des contrats avec littéraux → la couverture vraie
passe de 115/133 à 400/408 (98,0 %). Documentée pour règle CORTEX NK systématique.
Le module nk_measure_quote.c
est hors scope Frama-C/WP par limite SMT structurelle sur arrays crypto >1 Ko
(mldsa_sig[4627]).
Couvert via combinaison Isabelle/HOL (10 théorèmes) + CBMC (533 propriétés vérifiées)
+ HACL* (axiomatisé) — complémentarité audit-grade documentée.
2 287 LOC vérifiables au cloc
Le chiffre de 2 287 lignes de code C ne sort pas d’un slide. Il est obtenu par exécution de
l’outil standard cloc
(Count Lines Of Code) sur le code source réel. Périmètre : noyau + raffinement capabilities +
binding crypto natif. Méthode comparable à celle utilisée pour seL4.
La règle de comparaison équitable des micronoyaux : on compte le cœur du noyau et ses dépendances directes, pas les bibliothèques crypto de référence externes. seL4 publie 8 700 LOC sans inclure OpenSSL. CORTEX NK publie 2 287 LOC sans inclure liboqs. Périmètres strictement comparables.
Le TCB pur (262 LOC) seul ne reflète pas l’opérationnalité. Un évaluateur CESTI demande systématiquement d’inclure le raffinement capabilities et le binding crypto natif, car ces composants partagent les privilèges du TCB et participent à la surface de confiance. Le périmètre 2 287 LOC est celui préparé pour l’évaluation CSPN.
Note méthodologique. Le code source CORTEX NK sera mis à disposition des CESTI agréés et des
partenaires institutionnels dans le cadre des évaluations CSPN ANSSI (2027) et Common Criteria
EAL4 (2028). Toute mesure publique repose sur l’outil cloc
(AlDanial/cloc, MIT licence) appliqué au périmètre déclaré ci-dessus, méthode identique à celle
employée pour seL4 par la Foundation seL4.
Ce que nous ne prouvons pas
La transparence sur les limites est ce qui distingue un dossier audit-grade d’un slide de vente. CORTEX NK documente explicitement ses frontières — communes à l’état de l’art mondial 2026. C’est cette honnêteté qui fait la crédibilité devant ANSSI/CESTI.
Ed25519 sign · résolu sur la toolchain de production
Un motif de réécriture introduit par le compilateur sous la configuration d’analyse clang-musl -O1 pouvait rompre la propriété Constant-Time — phénomène connu et publié, sensible à la chaîne d’outils. La source HACL* est CT par construction. Sur la toolchain de production exacte (gcc-O2 bare-metal), le binaire livré est CT-clean : BINSEC-039 SECURE — 64 494/64 494 CF, 230 940/230 940 MEM, 0 alerte.
Ed25519 verify · frontière outil (entrées publiques)
La fonction Curve25519_finv
(inversion modulaire, 255 squarings symboliques) provoque une explosion de chemins qui dépasse
Binsec/Rel sur les deux toolchains testées (BINSEC-017 et 042) — 0 alerte sur les chemins explorés.
Point clé : en EdDSA, verify n’opère que sur des entrées publiques (le secret n’y
entre jamais), donc le CT de verify n’est pas une propriété de sécurité. Fermeture
compositionnelle de finv en feuille de route (candidat CIFRE).
ML-KEM-768 (FIPS 203) · vérifié par noyaux au binaire
ML-KEM n’est pas dans la release stable HACL* 0.7.2 ; il est utilisé via liboqs (FIPS 203) en
production. CORTEX a vérifié au binaire ARM64 de prod ses 10 noyaux sensibles au secret
(BINSEC-043/044) — 9 SECURE + 1 par composition, compress
DIV-clean, 0 alerte. Travail complémentaire de Formosa-Crypto (ML-KEM CT jusqu’à
l’assembleur via Jasmin) et libcrux (Rust vérifié). Frontière résiduelle : la preuve machine
bout-en-bout. Hors TCB BL2.
ML-DSA-87 (Dilithium) · Frontière upstream HACL*
ML-DSA n’est pas non plus intégré dans HACL* 0.7.2. Utilisé via liboqs (NIST FIPS 204 standard) en production. Composition prouvée formellement dans le module Mesh v1 via théorème ME-HYBRID-pq_safe (résistance quantum-safe en cas de fall-back).
9 fonctions au cœur du noyau
Mesures terminal réelles, macOS Apple Silicon, clang -O1, hardening PAC/BTI + shadow stack actif. 7 fonctions sur 9 sous la barre des 10 nanosecondes — les deux opérations de modification de mapping sont volontairement plus coûteuses, car elles modifient les structures protégées.
| Fonction | Mean (ns) | p99 (ns) |
|---|---|---|
| nk_mmu_check_access [READ ok] Vérifier qu’une lecture mémoire est autorisée | 4,81 | 16 |
| nk_mmu_check_access [no mapping] Détecter une zone mémoire non cartographiée | 4,42 | 11 |
| nk_mmu_check_access [NULL ptr] Bloquer un accès à un pointeur nul | 4,21 | 8 |
| nk_mmu_check_wx [invariant W^X] Empêcher qu’une zone soit à la fois modifiable et exécutable | 4,71 | 15 |
| nk_mmu_switch_domain Basculer entre deux domaines de sécurité isolés | 4,03 | 5 |
| nk_mmu_init Initialiser la table mémoire protégée | 4,02 | 5 |
| nk_mmu_enable Activer la protection mémoire matérielle | 8,06 | 9 |
| nk_mmu_map [add mapping] Autoriser un nouvel accès mémoire — opération protégée | 83,41 | 111 |
| nk_mmu_set_readonly Verrouiller une zone en lecture seule — opération protégée | 86,63 | 172 |
CORTEX NK vs seL4
Comparaison fonction-à-fonction sur l’opération de référence des micronoyaux à capabilities. Sur la fonction de référence (capability check), CORTEX NK exécute 140 à 376 itérations dans le temps où seL4 en exécute 1.
| Fonction comparée | CORTEX NK | seL4 (sel4bench off.) |
|---|---|---|
| Capability check / fast path M02 PRISM blp_can_read | 0,90 ns | ≈ 338 ns |
| Domain transition PRISM tcb_transition | 1,16 ns | ≈ 219-338 ns |
| MMU access check nk_mmu_check_access | 4,21 ns | non publié |
| Boot step / Root of Trust M00 boot_step | 1,30 ns | non publié |
| Policy evaluation OMEGA policy_eval | 2,30 ns | non publié |
Ratio sur opération de référence : ×140 à ×376 · à confirmer ATE_IND.2 CESTI Q3 2026.
Pourquoi pas les autres
Six micronoyaux comparés sur onze critères, sources publiques vérifiées. À notre connaissance, CORTEX NK est le seul acteur combinant TCB minimal de 2 287 lignes, preuves formelles dont l’ampleur dépasse les exigences EAL7, trajectoire de certification officielle (CSPN puis EAL7 visé), souveraineté française, 16 primitives BINAIRE prouvées CT, toutes benchmarkées, + 8 références (dont 5 PQC) incluant HQC 🇫🇷.
| CORTEX NK 🇫🇷 France |
ProvenRun 🇫🇷 France |
seL4 / NICTA 🇦🇺 Australie |
Green Hills 🇺🇸 USA ⚠ |
Wind River 🇺🇸 USA ⚠ |
SYSGO PikeOS 🇩🇪 Allemagne |
|
|---|---|---|---|---|---|---|
| Certification Common Criteria | Preuves au-delà des exigences EAL7 cible EAL7 2030 |
EAL7 ✓ certifié 2019 |
Preuves au-delà des exigences EAL7 non passé en certif. |
EAL6+ | EAL4+ | EAL3+ |
| Certification CSPN ANSSI | Préparée cible Q1 2027 |
~ | ✗ | ✗ | ✗ | ✗ |
| Théorèmes Isabelle/HOL · 0 sorry | 10 538 0 sorry · multi-outils |
✓ | ~200k lignes jusqu’au binaire |
~ | ✗ | ✗ |
| Taille du TCB | 2 287 LOC × 3,8 plus petit |
non publié | ~8 700 LOC | propriétaire | propriétaire | propriétaire |
| 16 primitives BINAIRE prouvées CT SHA-256/512 · HMAC · ChaCha20-Poly1305 · HKDF · SHA-3 · BLAKE2b · X25519 · Ed25519 · FrodoKEM-64 🏆 — couverture la plus large documentée — |
✓ 16 | 0 | 0 | 0 | 0 | 0 |
| PQC NIST 2024 | ✓ HQC 🇫🇷 | ✗ | ✗ | ✗ | ✗ | ✗ |
| 16 primitives prouvées CT + mesurées SHA-256/512 · SHA-3 · HMAC · BLAKE2b · Poly1305 · ChaCha20-Poly1305 · HKDF · Ed25519 · X25519 (perf HACL*) · + 8 réf liboqs dont ML-KEM/ML-DSA/SLH-DSA/BIKE/HQC 🇫🇷 — sans équivalent publié connu — |
✓ | ✗ | ✗ | ✗ | ✗ | ✗ |
| Souveraineté France / UE | ✓ | ✓ | ✗ | ✗ | ✗ | ~ |
| Palier formel ferme (%) Niveau de confiance mathématique défendable · scope crypto applicatif + TCB strict |
99,90 % + TCB strict 98,1 % S82 |
~99,7 % scope TEE |
99,95 % scope microkernel · 0 crypto |
~99,5 % EAL6+ certifié |
~99,2 % EAL4+ certifié |
~99,0 % EAL3+ certifié |
De la preuve à l’EAL7
Cinq modules TCB livrés (4 PRs mergées + 1 ouverte), 39 théorèmes Isabelle/HOL modules, 72+ preuves Binsec/Rel, palier 99,90% ferme. Sprint S82 (juin 2026) : TCB strict 4 modules ≥ 96 % WP. Planification CSPN Q1 2027, projection EAL6 2029 et EAL7 à horizon 2030. Aucun raccourci — chaque jalon est documenté, daté, prouvé.
✓ Terminé
Module Secure Boot
PR #16 · S1-S10 · 211/211 tests · 21 mai 2026
✓ Terminé
Auto-Containment
PR #17 · 339/339 WP · 6 thm HOL · 22 mai 2026
✓ Terminé
Audit Log Immuable
PR #18 · 426/443 WP · 8 thm HOL · 22 mai 2026
✓ Terminé
Mesh v1 PQC
PR #19 · 18 thm HOL · 119 tests · 24 mai 2026
✓ Terminé
Module 17 TCB Crypto
PR #19 · 16 primitives BINAIRE · 12/12 TCB crypto sur prod
✓ Terminé · NEW
Sprint S82 · TCB strict
4 modules ≥ 96 % WP · 98,1 % moyenne · 2 juin 2026
Q3 2026
ATE_IND.2 CESTI
Validation indépendante plateforme cible
Q1 2027
CSPN ANSSI
Premier palier de certification
2028
EAL4
Méthodiquement conçu et testé
2029-2030
EAL6 → EAL7
Conception semi-formelle puis prouvée
Parlons souveraineté.
Rapports complets sur demande : CFVL-SYNTHESE-001 v1.0 · CFVL-CT-PROD-001 v1.0 (campagne TCB crypto toolchain prod) · CFVL-SYNTHESE-MLKEM-001 · CFVL-SYNTHESE-FRODO-001 (PQC de production, CT binaire hors TCB) · CFVL-BENCH-CT16-001 (perf des 16 primitives prouvées CT, HACL*) · CFVL-BENCH-SECBOOT-001 v2.0 · CFVL-BENCH-CONTAINMENT-001 v1.0 · CFVL-EVAL-NK-AUDIT-001 v1.0 · CFVL-EVAL-NK-MESH-001 v1.0 · Security Target CESTI · Bilan S82 TCB strict. Démonstrations sur scénarios CNES / DGA / OIV disponibles.
Confidentiel · CORTEX AI™ SAS · SIREN 991 880 428 · 58 rue de Monceau, 75008 Paris