Secure Boot TF-A
Post-Quantique

F-1 à F-6.H · Chaque palier indépendamment vérifiable

Le sprint S73c-f a été conduit en onze paliers F-1 → F-6.H, chacun avec son périmètre isolé, ses tests, et son commit Git correspondant. La numérotation reflète l’ordre logique de construction : préliminaires plateforme, intégration des clés, ajout du backend HACL*, ajout du backend ML-DSA-87, intégration ATF/BL2, fixes runtime, et durcissement sécurité F-6.H final.

Symétrie SCTLR/CPTR autour des appels HACL*

Le palier F-6.H est le dernier de la séquence S73c-f. Il transforme une baisse de garde architecturale globale (établie en F-6.C/D pour permettre les stores SIMD non alignés de HACL*) en une fenêtre minimale strictement bornée à chaque appel cryptographique. C’est le palier qui permet à la chaîne d’être présentée à un évaluateur CESTI : la propriété architecturale n’est plus relâchée que pendant la durée d’exécution d’un verify, avec restauration symétrique stricte.

AUDIT-NOTE F-6.H · extrait du fichier hacl_crypto.c

Compromis différencié EL3 (BL1) vs S-EL1 (BL2)

En EL3 (BL1), le wrapping per-call strict suffit : le code C entre deux appels HACL* exécute peu d’instructions, GCC ne génère pas de stockages SIMD non alignés observables. En S-EL1 (BL2), le code TF-A entre deux appels HACL* est plus volumineux (load image I/O, INFO printf, fip_find, handoff build) et GCC génère régulièrement des str q sur la pile à des offsets non alignés 16B. Restaurer SCTLR_EL1.A=1 entre deux calls provoquerait un Data Abort silencieux.

Décision F-6.H : clear SCTLR_EL1.A une fois en S-EL1 à l’init du backend, restauration déférée au handoff BL31 (qui réinitialise CPTR_EL3 et SCTLR_EL3 via bl31_entrypoint.S / el3_common_macros). La fenêtre EL3 reste strictement bornée per-call ; la fenêtre S-EL1 est bornée à la durée de BL2 (~quelques millisecondes), ce qui reste compatible avec l’objectif d’audit CESTI dès lors que TBBR est mono-thread, IRQs masquées, sans canal d’entrée externe pendant la fenêtre.

L’hybridité tient au niveau de la chaîne, pas du cert isolé

Cette section documente explicitement et honnêtement la propriété de résistance post-quantique de la chaîne S73c-f. La distinction entre « hybride par chaîne » et « hybride par cert » est subtile mais essentielle pour toute communication audit-grade. Un évaluateur CESTI rigoureux pointera cette nuance — autant qu’elle soit documentée formellement par nos soins.

Propriété formelle garantie

Un adversaire disposant d’un ordinateur quantique cryptographiquement pertinent (CRQC) capable de casser Ed25519 via l’algorithme de Shor ne peut pas produire un firmware accepté par la chaîne complète BL1 → BL33. Cette propriété repose sur l’exigence cumulative de deux signatures séparées :

• Ed25519 (signature classique, héritée TBBR upstream) — vérifiée par BL1 sur le cert de BL2, puis par BL2 sur tous les certs des images chargées.
• ML-DSA-87 (signature post-quantique, ajoutée par CORTEX NK) — vérifiée par BL2 en batch sur les 6 certs TBBR après chargement complet, avant tout transfert à BL31.

Précision auditable honnête

L’hybridité tient au niveau de la chaîne complète, pas au niveau d’un certificat isolé. Les certificats X.509 du TBBR portent une signature Ed25519 unique au format upstream standard. La signature ML-DSA-87 est attachée séparément par sidecar FIP et vérifiée en batch par nk_mldsa87_verify_all_certs() en fin de chaîne BL2. La propriété PQ-résistante est donc garantie post-vérification BL2 complète, pas dès le premier byte vérifié en BL1.

Un adversaire CRQC capable de falsifier un cert Ed25519 isolé peut donc en théorie faire passer un cert modifié à BL1 (qui le vérifiera Ed25519-OK), mais BL2 détectera l’incohérence en fin de chaîne via la vérification ML-DSA-87 compagne. Le boot s’arrête par panic() avant tout saut BL31.

Caveat de portée documenté

Pendant la fenêtre intra-BL2 entre le chargement d’une image et sa vérification ML-DSA, un adversaire CRQC ayant compromis Ed25519 pourrait théoriquement faire accepter une image falsifiée par BL1. En pratique cette fenêtre n’est pas exploitable :

• BL2 s’exécute en S-EL1 single-thread, single-core boot
• IRQs masquées (DAIF.I = 1) jusqu’à l’exit de bl2_main
• Aucun canal d’entrée externe (pas de réseau, pas d’USB, pas d’I/O console)
• Aucun secret cryptographique manipulé pendant cette fenêtre — rien à exfiltrer
• Aucune exécution d’image utilisateur (BL33 pas encore atteint)

La vulnérabilité formelle existe (différence avec un schéma dual-sig par cert). La vulnérabilité exploitable n’existe pas dans le modèle de menace réel. Cette distinction est exactement ce que le vocabulaire audit-grade sert à exprimer.

Ce que nous ne prétendons pas

La transparence sur les limites est ce qui distingue un dossier audit-grade d’un slide marketing. CORTEX NK documente explicitement quatre frontières du sprint S73c-f, vérifiables dans le code et dans le rapport de validation. C’est cette honnêteté qui fait la crédibilité devant ANSSI / CESTI / DGA.

Menaces explicitement hors périmètre S73c-f

Le sprint S73c-f couvre la chaîne logicielle de vérification cryptographique BL1 → BL33. Les classes d’attaques suivantes sont explicitement hors périmètre du logiciel CORTEX NK et nécessitent des contre-mesures matérielles ou architecturales distinctes (TPM 2.0, secure element, mesures physiques de protection, mécanismes anti-glitch silicium). Elles sont mentionnées ici pour transparence audit.

Trois preuves indépendantes

Le sprint S73c-f s’inscrit dans la discipline méthodologique CORTEX NK : chaque livrable est vérifié par trois outils complémentaires qui se contrôlent mutuellement. La page dédiée Secure Boot natif (S1-S10) détaille ces résultats pour le module propriétaire ; cette page-ci en restitue l’application à la chaîne TF-A intégrée.

Trois outils internes. Une revue externe en cours. Zéro angle mort.