💻 computer science

Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

Cet article présente les premiers théorèmes de composition vérifiés par machine pour le masquage arithmétique sur les corps premiers, démontrant qu'un masquage aléatoire frais entre les étapes du pipeline garantit une indépendance de sécurité vis-à-vis des étapes précédentes et utilisant ces résultats formels pour diagnostiquer une faille critique de masquage inter-étapes dans l'accélérateur PQC Adams Bridge de Microsoft.

Auteurs originaux : Ray Iskander, Khaled Kirah

Publié 2026-04-29

📖 6 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

Imaginez que vous essayiez d'envoyer un message secret à travers une chaîne de montage d'usine. Le message est sensible, vous ne voulez donc pas que quiconque observe la ligne puisse deviner de quoi il s'agit. Pour le protéger, vous décomposez le message en morceaux et mélangez chaque morceau avec un « bruit » aléatoire (un masque) avant qu'il ne passe à la station suivante. Cela s'appelle le masquage.

Dans le monde de la sécurité informatique, il existe deux types principaux de bruit :

Bruit booléen : Comme actionner des interrupteurs (marche/arrêt). Nous disposons déjà d'un manuel de règles parfait pour empiler ces interrupteurs en toute sécurité.
Bruit arithmétique : Comme additionner des nombres sur une horloge (où 12 + 1 = 1). C'est ce que la cryptographie moderne « post-quantique » utilise. Jusqu'à présent, nous n'avions pas de manuel de règles pour empiler ces masques basés sur les nombres en toute sécurité.

Ce papier fournit ce manuel de règles manquant. Voici l'histoire de ce qu'ils ont découvert, expliquée simplement.

1. Le Problème : Le Milieu « Fuyant »

Imaginez une chaîne de montage en deux étapes :

Station A : Prend votre secret, ajoute du bruit, et le transmet.
Station B : Prend ce que la Station A a transmis, ajoute plus de bruit, et envoie le résultat final.

Les chercheurs ont découvert un défaut dangereux dans la façon dont ces stations étaient connectées dans une puce de sécurité Microsoft célèbre (appelée « Adams Bridge »).

Dans la conception défectueuse, la Station A transmettait son résultat bruité directement à la Station B. En raison du fonctionnement des mathématiques (spécifiquement une étape appelée « réduction de Barrett », qui est une manière complexe de faire une division), le « bruit » sortant de la Station A n'était pas parfaitement aléatoire. Il présentait un motif.

L'Analogie : Imaginez que la Station A est un mixeur. Il mélange votre secret avec de la glace. Mais en raison de la façon dont les lames tournent, les morceaux de glace sortants sont légèrement irréguliers — certains endroits ont plus de glace, d'autres moins. Si un espion (un pirate informatique) se tient juste entre la Station A et la Station B et compte les morceaux de glace, il peut deviner une partie de votre secret. Cela s'appelle une attaque par canal auxiliaire.

2. La Solution : Le « Masque Frais » (L'Argument de Renouvellement)

Le grand moment « Aha ! » du papier est étonnamment simple. Ils ont prouvé que si vous insérez un masque aléatoire frais et tout nouveau entre la Station A et la Station B, le problème disparaît instantanément.

L'Analogie :

Sans la correction : La Station A remet un tas de glace légèrement irrégulier à la Station B. La Station B essaie de le corriger, mais l'irrégularité est déjà intégrée.
Avec la correction : La Station A remet son tas irrégulier à un « Bouton de Réinitialisation ». Ce bouton vide le tas dans un seau géant d'eau parfaitement mélangée (le nouveau masque). Maintenant, lorsque la Station B prend une louche dans ce seau, elle est à nouveau parfaitement aléatoire.

Le papier prouve mathématiquement que ce masque frais efface complètement la mémoire de la Station A. Peu importe si la Station A était désordonnée ou parfaite ; une fois le masque frais appliqué, le fil reliant à la Station B est parfaitement uniforme. La sécurité de toute la ligne dépend alors uniquement de la qualité de la Station B.

3. La « Barrière à 1 Bit »

Les chercheurs ont découvert que pour les mathématiques spécifiques utilisées dans ces puces (réduction de Barrett), le bruit n'est jamais parfaitement aléatoire par lui-même. Il présente une « fuite » d'au maximum 1 bit d'information.

Pensez-y comme à une pièce légèrement déséquilibrée. Ce n'est pas une pièce équitable ; elle tombe sur « Face » légèrement plus souvent.
Ce n'est pas une erreur de conception ; c'est une propriété fondamentale des mathématiques. Le papier appelle cela la « Barrière à 1 Bit ».
Cependant, le papier prouve que si vous utilisez l'astuce du « Masque Frais » entre les étapes, cette fuite de 1 bit est cachée à l'intérieur du bruit frais et devient inutile pour un espion.

4. La Preuve : Vérifiée par Machine

Les auteurs ne se sont pas contentés de l'écrire sur papier ; ils ont utilisé un programme informatique appelé Lean 4 pour vérifier chaque étape de leur logique.

Ils ont écrit 18 preuves spécifiques.
L'ordinateur les a toutes vérifiées avec zéro erreur et zéro note du type « Je ferai cela plus tard » (appelées « stubs sorry »).
Cela signifie que les mathématiques sont solides comme du roc. Ce n'est pas juste une théorie ; c'est un fait vérifié.

5. Le Diagnostic : Pourquoi la Puce de Microsoft était Vulnérable

L'équipe a appliqué son nouveau manuel de règles à la puce « Adams Bridge » de Microsoft.

La Découverte : La puce avait deux étapes (Butterfly et Barrett) mais aucun masque frais entre elles.
Le Résultat : Le fil reliant ces deux étapes était « fuyant ». Il n'était pas uniforme. Cela a confirmé pourquoi d'autres chercheurs avaient déjà réussi à pirater cette puce en utilisant l'analyse de puissance (mesure de la consommation électrique).
La Correction : Le papier prescrit une correction simple : Ajouter un générateur de nombres aléatoires supplémentaire et une étape de soustraction entre les étapes. Cela rend le fil intermédiaire parfaitement sûr.

Résumé

Ce papier résout une pièce manquante du puzzle pour les puces informatiques sécurisées.

Le Problème : Lorsqu'on enchaîne des opérations mathématiques, le « bruit » utilisé pour cacher les secrets peut devenir désordonné et fuir des informations au milieu.
La Correction : Insérer une réinitialisation aléatoire et fraîche entre chaque étape.
La Preuve : Ils ont utilisé un ordinateur pour prouver que cette réinitialisation rend le fil intermédiaire parfaitement sûr, peu importe à quel point la première étape était désordonnée.
L'Application : Ils ont montré exactement pourquoi une célèbre puce Microsoft était vulnérable et comment la corriger avec un simple changement architectural.

En bref : Si vous voulez cacher un secret à travers un processus multi-étapes, ne comptez pas uniquement sur le déguisement de la première étape. Ajoutez un nouveau déguisement frais entre chaque étape, et le secret restera en sécurité.

1. Énoncé du problème

L'article comble une lacune critique dans la vérification formelle de la sécurité du matériel de Cryptographie Post-Quantique (PQC), spécifiquement pour les implémentations de la Transformée Numérique Théorique (NTT) utilisées dans les normes du NIST (ML-KEM et ML-DSA).

Le Contexte : Les implémentations matérielles de la NTT reposent sur un masquage arithmétique sur des corps premiers ( $\mathbb{Z}_q$ ) pour résister aux attaques par canal auxiliaire telles que l'analyse de la consommation différentielle (DPA).
La Lacune : Alors que le masquage booléen (sur $GF(2^n)$ ) bénéficie d'une théorie de composition mature (NI, SNI, PINI) avec des preuves vérifiées par machine, le masquage arithmétique sur les corps premiers manque de théorèmes de composition analogues.
Le Problème Spécifique : Dans le masquage arithmétique, des opérations comme la réduction modulaire (par exemple, la réduction de Barrett) interagissent avec les masques de manière non triviale. Contrairement au XOR booléen, où le masquage préserve parfaitement l'uniformité, le masquage arithmétique peut entraîner des distributions de sortie non uniformes (multiplicité > 1).
La Vulnérabilité : Des analyses empiriques et des études structurelles précédentes ont identifié des vulnérabilités dans l'accélérateur PQC "Adams Bridge" de Microsoft, où les fils intermédiaires entre les étages de pipeline étaient non uniformes, permettant des attaques DPA. Cependant, une explication théorique formelle du pourquoi cela se produit et du comment le corriger via des théorèmes de composition faisait défaut.

2. Méthodologie

Les auteurs utilisent la vérification formelle avec l'assistant de preuves Lean 4 pour dériver et prouver des théorèmes de composition pour le masquage arithmétique.

Modèle Formel : Ils définissent une métrique de sécurité quantitative appelée PF-PINI(k) (Prime-Field Probe Isolating Non-Interference).
- Contrairement aux notions de sécurité binaires (sûr/insûr), PF-PINI mesure la multiplicité des valeurs de sortie par rapport à l'espace des masques.
- $k=1$ implique une distribution parfaitement uniforme.
- $k=2$ implique une multiplicité maximale de 2, fuyant jusqu'à 1 bit d'information par fil.
L'Argument de Renouvellement : L'insight théorique central est que l'application d'un masque aléatoire frais entre deux étages de pipeline efface complètement le paramètre de sécurité ( $k_1$ ) du premier étage du fil intermédiaire, indépendamment de la non-uniformité de la sortie du premier étage.
Pont Matériel : Les auteurs comblent formellement le fossé entre les modèles algébriques abstraits ( $\mathbb{Z}_q$ ) et l'arithmétique sur les nombres naturels (Nat) fidèle au matériel utilisée dans les conceptions RTL, spécifiquement pour la réduction de Barrett.
Portée de la Vérification : L'ensemble du travail consiste en 18 théorèmes vérifiés par machine avec zéro stub sorry (aucune hypothèse non prouvée), garantissant des assurances de haute fiabilité.

3. Contributions Clés

L'article apporte six contributions principales :

Le Théorème de Renouvellement (Théorème 4.1) : Prouve que si un masque aléatoire frais est appliqué entre deux étages ( $G_1 \to G_2$ ), le fil intermédiaire devient parfaitement uniforme. L'ensemble des paires de masques produisant une valeur intermédiaire spécifique a une cardinalité exactement égale à $q$ , indépendante du paramètre de sécurité de $G_1$ .
Théorème de Composition Positive (Théorème 4.4) : Démontre qu'un pipeline à deux étages avec masquage frais satisfait PF-PINI( $k_2$ ). La sécurité de la sortie composée dépend uniquement du paramètre du second étage ( $k_2$ ) ; la faiblesse du premier étage ( $k_1$ ) est complètement effacée.
Théorèmes de Composition Négative (Théorèmes 5.1–5.3) : Prouve que sans masquage frais, le fil intermédiaire conserve la multiplicité du premier étage ( $k_1$ ). Si $k_1 > 1$ , le fil est non uniforme, créant une condition nécessaire pour les attaques DPA.
Pont Algébrique-Matériel (Théorème 6.1) : Prouve formellement que l'application de réduction de Barrett algébrique est équivalente à l'application d'arithmétique Nat fidèle au matériel dans des conditions de portée standard ( $q \le 2^s$ ). Cela valide que les bornes théoriques s'appliquent directement aux implémentations sur silicium.
Diagnostic Adams Bridge : Instancie formellement les théorèmes pour diagnostiquer l'accélérateur Adams Bridge de Microsoft. La preuve confirme que l'absence de masquage frais inter-étage laisse les fils de sortie de Barrett non uniformes (PF-PINI(2)), expliquant le succès des attaques DPA empiriques précédentes.
Barrière Universelle de 1 Bit : Fournit des preuves computationnelles que la borne PF-PINI(2) est universelle pour les réductions modulaires (tant Barrett que Montgomery), suggérant une "Barrière de 1 Bit" fondamentale pour ces opérations.

4. Résultats Clés

Preuve Formelle de Composition : L'article établit que le masquage frais inter-étage est la condition nécessaire et suffisante pour composer des gadgets arithmétiques de manière sécurisée.
Sécurité Quantitative :
- Avec Masquage Frais : Le fil intermédiaire est uniforme ( $k=1$ ). La sortie finale est bornée par le paramètre du second étage ( $k_2$ ).
- Sans Masquage Frais : Le fil intermédiaire est non uniforme (jusqu'à $k_1$ ). Cette non-uniformité est la cause racine des fuites par canal auxiliaire observées dans les attaques empiriques.
Correction Adams Bridge : Le diagnostic confirme que l'ajout d'un seul registre de masque aléatoire frais et d'une opération de soustraction entre les étages Butterfly et Barrett dans le pipeline Adams Bridge éliminerait la vulnérabilité DPA sur les fils intermédiaires sans modifier le paramètre de sécurité de la sortie finale.
Disponibilité de l'Artefact : Le code source complet Lean 4, incluant 18 théorèmes et un script de reproduction, est disponible publiquement, permettant une vérification indépendante des preuves.

5. Importance

Première Composition Arithmétique Vérifiée par Machine : Il s'agit du premier travail fournissant des théorèmes de composition vérifiés par machine pour le masquage arithmétique sur les corps premiers, comblant un vide théorique majeur dans la sécurité matérielle PQC.
Pont entre Théorie et Pratique : En reliant formellement les preuves algébriques abstraites à l'arithmétique fidèle au matériel, l'article fournit une base rigoureuse pour vérifier les conceptions réelles sur silicium, allant au-delà des tests empiriques.
Ligne Directrice de Conception : Il établit une règle de conception claire et prouvable pour le matériel PQC : Insérer toujours un masquage frais entre les étages de pipeline. Ce simple changement architectural garantit que la sécurité du pipeline composé est déterminée uniquement par le maillon le plus faible de l'étage final, et non par les étages intermédiaires.
Convergence des Preuves : La preuve formelle s'aligne parfaitement avec trois analyses antérieures indépendantes (analyse de puissance empirique, revue de code et analyse de dépendance structurelle), confirmant que le défaut architectural identifié dans l'accélérateur Adams Bridge est bien la cause racine de sa vulnérabilité.

En résumé, cet article fournit l'ossature mathématique et de vérification formelle requise pour concevoir des accélérateurs matériels sécurisés, composites et résistants aux canaux auxiliaires pour la nouvelle ère de la Cryptographie Post-Quantique.