💻 computer science

Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators

Cet article présente une hiérarchie de vérification à quatre étapes qui permet d'étendre la preuve de sécurité des masquages d'ordre un aux modules arithmétiques de production à grande échelle, réduisant ainsi considérablement le nombre de signaux nécessitant une revue manuelle pour la certification FIPS 140-3 d'accélérateurs cryptographiques post-quantiques.

Auteurs originaux : Ray Iskander, Khaled Kirah

Publié 2026-04-17

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Ray Iskander, Khaled Kirah

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🛡️ Le Gardien des Secrets : Comment vérifier la sécurité des "Super-Ordinateurs" du Futur

Imaginez que vous construisez un coffre-fort ultra-moderne pour protéger des secrets contre des voleurs qui utilisent des ordinateurs quantiques (des machines capables de casser les codes actuels). Ce coffre-fort, c'est le Adams Bridge, un composant électronique complexe conçu pour sécuriser les communications de demain.

Le problème ? Pour être sûr qu'il est inviolable, il faut vérifier qu'aucun "fuite" d'information ne se produit, même si un espion regarde le coffre-fort de très près (en mesurant sa consommation électrique). C'est ce qu'on appelle l'analyse des canaux auxiliaires.

Ce papier présente un nouvel outil, nommé QANARY (comme l'oiseau canari qu'on utilisait autrefois dans les mines pour détecter le gaz toxique), capable de vérifier la sécurité de ces coffres-forts géants avant même qu'ils ne soient fabriqués.

Voici comment cela fonctionne, étape par étape, avec des analogies simples :

1. Le Problème : Le "Brouillard" des Partages

Pour protéger un secret, on ne le garde pas en un seul endroit. On le découpe en plusieurs morceaux (appelés "parts" ou shares) et on les mélange avec du bruit aléatoire.

L'analogie : Imaginez que vous avez un secret écrit sur un papier. Au lieu de le garder, vous le déchirez en deux morceaux. Vous donnez un morceau à Alice et l'autre à Bob. Si un espion vole le papier d'Alice, il ne voit rien. S'il vole celui de Bob, il ne voit rien non plus.
Le danger : Si, à un moment donné, les deux morceaux se rejoignent dans le circuit électronique (comme si Alice et Bob se passaient leurs morceaux à travers un tuyau), l'espion peut les reconstituer et lire le secret.

2. La Méthode : Une Enquête en Quatre Étages

Vérifier manuellement chaque fil d'un circuit de 1,17 million de composants est impossible (ce serait comme chercher une aiguille dans une montagne de foin). L'outil QANARY utilise une approche en 4 étages pour trier le bon du mauvais :

Étage 1 : Le Détecteur de Fuite Structurelle (D0/D1)
- L'analogie : C'est un détecteur de métaux rapide. Il scanne tout le circuit et dit : "Attention ! Ici, le fil d'Alice et le fil de Bob se croisent potentiellement."
- Résultat : Il est très prudent. Il sonne l'alarme pour beaucoup de choses qui ne sont pas forcément dangereuses (des "fausses alertes"). Mais il ne rate jamais une vraie fuite. C'est rapide (quelques secondes pour tout le circuit).
Étage 2 : Le Rafraîchissement (FM)
- L'analogie : Parfois, même si les fils se croisent, un "vent frais" (une nouvelle donnée aléatoire) passe juste avant et brouille les pistes. Cette étape vérifie si ce vent a sauvé la situation.
- Résultat : Cela élimine quelques fausses alertes, mais pas la majorité.
Étage 3 & 4 : Le Juge Mathématique (SADC)
- L'analogie : C'est ici que la magie opère. Au lieu de juste regarder si les fils se croisent, l'outil demande à un super-calculateur (un solveur mathématique) : "Si je change le secret, est-ce que le résultat final change vraiment ?"
- Il utilise deux méthodes : une pour les nombres simples (Booléens) et une pour les nombres complexes (Arithmétiques, comme dans les calculs de crypto).
- Le résultat : Il prouve mathématiquement que pour la moitié des fausses alertes, il n'y a aucun risque. Pour l'autre moitié, il dit : "Attention, ici, il faut que l'ingénieur regarde de plus près."

3. Les Résultats Concrets : Du Chaos à la Clarté

Sur le circuit géant "Adams Bridge" :

Avant l'outil : Les ingénieurs voyaient des centaines de milliers de "fuites potentielles". C'était ingérable.
Après l'outil :
- L'outil a prouvé mathématiquement que 198 de ces "fuites" étaient en réalité sûres (c'est comme si on avait trouvé que le vent avait bien protégé le secret).
- Il a isolé 165 zones vraiment suspectes qui méritent une attention humaine.
- Il ne reste aucun doute (0 cas indécis).

C'est comme passer d'une liste de 363 suspects potentiels à une liste de 198 innocents (avec un certificat de sécurité) et 165 personnes à interroger.

4. Pourquoi c'est révolutionnaire ?

Avant, les outils de vérification étaient comme des microscopes puissants mais qui ne voyaient que des cellules individuelles (de petits circuits). Ils ne pouvaient pas voir l'organisme entier (le circuit complet de 1 million de composants).

QANARY est le premier outil capable de voir l'organisme entier, de détecter les fuites à travers les registres (les mémoires temporaires du circuit) et de donner des preuves mathématiques solides.
Il a été vérifié par deux "juges" différents (Z3 et CVC5) qui sont tombés d'accord sur tous les points, garantissant qu'il n'y a pas d'erreur de calcul.

En Résumé

Ce papier décrit un système d'alarme intelligent pour les coffres-forts du futur. Au lieu de paniquer face à des milliers d'alertes, il permet aux ingénieurs de dire : "Ok, 54% de ces alarmes sont fausses, prouvé par les maths. Concentrons-nous sur les 46% restants."

C'est une étape cruciale pour garantir que nos futures communications, protégées contre les ordinateurs quantiques, seront vraiment sécurisées avant même d'être fabriquées.

1. Problématique

La finalisation des standards de cryptographie post-quantique (ML-KEM et ML-DSA) en 2024 a intensifié le besoin d'accélérateurs matériels résistants aux canaux auxiliaires (side-channels). La contre-mesure dominante est le masquage, qui divise les secrets en plusieurs parts aléatoires. La sécurité repose sur l'invariant selon lequel aucune logique combinatoire ne doit permettre à deux parts d'un même secret de se recombiner.

Cependant, la vérification de cette propriété à l'échelle industrielle pose des défis majeurs :

Limites de l'échelle : Les outils de vérification formelle exacte (basés sur ROBDD ou SAT) ne s'appliquent qu'à des modules de quelques milliers de portes (généralement < 5 000 cellules). Ils ne peuvent pas traiter des accélérateurs complets de plusieurs millions de cellules.
Complexité du masquage arithmétique : Les algorithmes PQC (comme les Transformées de Fourier Numériques - NTT) utilisent un masquage arithmétique (modulo $q$ ) et des pipelines profonds. Les dépendances entre parts peuvent traverser plusieurs cycles d'horloge via des registres, rendant l'analyse combinatoire monocycle insuffisante.
Manque de preuves pré-silicium : Il est difficile de fournir des preuves de sécurité pour des designs de production avant leur fabrication, car les analyses basées sur des traces de puissance (DPA) nécessitent du matériel physique et peuvent manquer des fuites rares.

2. Méthodologie : QANARY

Les auteurs proposent QANARY (Quantum Canary), un outil d'analyse de dépendance structurelle conçu pour les grands circuits arithmétiques masqués. L'approche repose sur une hiérarchie de vérification en quatre étapes, allant d'une analyse rapide mais conservatrice à une vérification exacte sur les points critiques.

A. Analyse de Dépendance Structurelle (D0/D1)

C'est la première étape, rapide et sound (sans faux négatifs). Elle vérifie si une fil (wire) dépend combinatoirement de plus d'une part d'un secret.

Modèle : Un treillis de labels $\{ \bot, S_0, S_1, BOTH \}$ . Si une fil dépend de $S_0$ et $S_1$ , elle est marquée BOTH (potentiellement insecure).
Extension Multi-cycle (MC-D1) : Contrairement aux outils classiques qui traitent les sorties de registres comme des variables libres, MC-D1 propage les labels à travers les frontières de registres via une itération de point fixe. Cela permet de détecter les convergences de parts qui ne se produisent qu'après plusieurs cycles d'horloge.

B. Raffinement par Masquage Frais (FM)

Pour les fils marqués comme insécures, cette étape vérifie si une nouvelle source de hasard (randomness) agit comme un masque parfait (bijection) sur la sortie, rendant la fil statistiquement indépendante du secret.

C. Vérification Distributionnelle Statistique et Algébrique (SADC)

C'est l'innovation centrale pour réduire les faux positifs.

Principe : Au lieu de traiter les parts comme des entrées adverses, le SADC les reparamètre par rapport au secret sous-jacent et au masque (ex: $s_0 = x \oplus s_1$ pour le booléen, $s_0 = (x - s_1) \mod q$ pour l'arithmétique).
Vérification : Il utilise des solveurs SMT (Z3, CVC5) pour vérifier si la valeur de la fil est indépendante du secret pour toutes les combinaisons de masques et de hasard.
Arithmétique SADC : Spécialement conçu pour les circuits modulo $q$ (comme la réduction de Barrett), il gère les chaînes de retenue et les dépendances bit à bit complexes que les vérifications booléennes échouent à modéliser.

3. Contributions Clés

Vérification à l'échelle de production : Extension de l'analyse D0/D1 à l'accélérateur Adams Bridge (1,17 million de cellules, 30 sous-modules masqués), complétée en quelques secondes pour l'analyse monocycle.
Détection Multi-cycle (MC-D1) : Identification de 12 modules qui semblaient propres en monocycle mais qui sont structurellement compromis une fois les dépendances à travers les registres prises en compte.
Hiérarchie à 4 étapes avec SADC arithmétique :
- Sur le module de réduction de Barrett (5 543 cellules), la hiérarchie a permis de classer 198 fils (54,5 %) comme sécurisés par machine, réduisant la liste de vérification manuelle de 363 fils suspects à seulement 165 candidats (borne supérieure sûre).
- Aucun résultat n'est resté indéterminé.
Validation par double solveur : Chaque verdict SADC arithmétique est recoupé par deux solveurs indépendants (Z3 et CVC5) avec 0 désaccord sur les 363 fils analysés, éliminant les bugs d'implémentation des solveurs comme source d'erreur.
Infrastructure reproductible : Le code, les netlists synthétisées, et les scripts de preuve formelle sont publics, garantissant la reproductibilité des résultats.

4. Résultats Principaux

Échelle : Analyse complète de 27 modules sur les 30 d'Adams Bridge (les 2 plus grands ont dépassé le temps limite de 5h, ce qui est courant pour les outils exacts sur de telles tailles).
Performance :
- Analyse structurelle monocycle (SC-D1) : 8,7 secondes pour 1,17M de cellules.
- Analyse multi-cycle (MC-D1) : 231,8 secondes au total.
- Pipeline SADC complet sur le module Barrett : ~3 minutes sur un seul cœur.
Précision et Triage :
- Sur le module Barrett, le SADC arithmétique a éliminé 198 faux positifs structurels, fournissant des certificats de sécurité mathématiques.
- Les 165 fils restants sont identifiés comme des candidats pour une analyse manuelle approfondie ou une vérification exacte ultérieure, offrant un compromis optimal entre exhaustivité et coût de calcul.
Comparaison : L'outil a été comparé à Coco-Alma (outil exact SAT). Bien que Coco-Alma ne puisse pas scaler à la taille complète du module Barrett, les deux outils s'accordent sur les petits sous-ensembles testés. L'article note que les divergences observées sur un module "Papillon" (Butterfly) sont dues à des définitions différentes de la fuite (état stable vs état transitoire/glitch), et non à une erreur de l'outil.

5. Signification et Impact

Ce travail représente une avancée majeure pour la certification matérielle de la cryptographie post-quantique (FIPS 140-3) :

Passage de la théorie à l'industrie : Il démontre qu'il est possible de fournir des preuves de sécurité pré-silicium pour des accélérateurs PQC de taille industrielle, là où les outils formels exacts échouent.
Réduction de la charge de travail : En transformant des centaines de milliers d'alertes structurelles en une liste gérable de quelques centaines de candidats vérifiés mathématiquement, l'outil permet aux ingénieurs de se concentrer sur les vrais risques.
Complémentarité : L'approche ne remplace pas les vérifications exactes ou les tests physiques, mais elle agit comme un filtre puissant et évolutif. Elle identifie les points de convergence de parts (root causes) qui doivent ensuite être validés par des méthodes plus précises ou des mesures physiques.
Nouveauté méthodologique : C'est la première intégration d'une vérification de dépendance de valeur arithmétique (SADC) dans un pipeline de vérification structurelle à grande échelle, comblant le fossé entre l'analyse rapide et la preuve formelle exacte pour les circuits arithmétiques masqués.

En conclusion, QANARY offre une boucle de rétroaction rapide, explicable et actionnable pour les équipes de conception de matériel PQC, permettant d'itérer sur les stratégies de masquage partiel avec une confiance accrue avant la fabrication.