The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

Résumé Technique : La Barrière 1-Bit est Universelle

Énoncé du Problème
La Transformée Numérique Théorique (NTT) sert de colonne vertébrale computationnelle pour les normes de cryptographie post-quantique (PQC) du NIST, ML-DSA (FIPS 204) et ML-KEM (FIPS 203). Les implémentations matérielles de ces normes reposent sur un masquage arithmétique pour résister aux attaques par canal auxiliaire, spécifiquement l'Analyse de Puissance Différentielle (DPA). Si le masquage booléen sur $GF(2^n)$ dispose de cadres de composition établis (par exemple, PINI), le masquage arithmétique sur $\mathbb{Z}_q$ pour un nombre premier $q$ présente des défis uniques.

Les travaux antérieurs du programme QANARY (Articles 1–6) ont établi des analyses de dépendance structurelle et quantifié les marges de sécurité pour des composants spécifiques, prouvant notamment que la réduction de Barrett satisfait une « Barrière 1-Bit » (PF-PINI(2)). Cependant, deux lacunes critiques subsistaient :

1. Profondeur de Pipeline Arbitraire : Les théorèmes de composition précédents étaient limités à deux étapes. Il n'existait aucune garantie formelle pour des pipelines à $k$ étapes arbitraires avec un masquage frais entre les étapes.
2. Réduction de Montgomery : Si la réduction de Barrett était caractérisée, la réduction de Montgomery — la seconde réduction modulaire standard utilisée dans le matériel NTT (dominante dans ML-DSA et certaines implémentations ML-KEM) — manquait d'une caractérisation formelle PF-PINI.
3. Bornes Unifiées de Bout en Bout : Il n'existait aucune borne de cardinalité unique et vérifiée par machine assemblant les résultats pour des pipelines arbitraires composés de papillons, de réductions de Barrett et de réductions de Montgomery.

Méthodologie
L'article utilise la vérification formelle avec l'assistant de preuve Lean 4. L'approche est strictement constructive, avec zéro sorry (hypothèses non prouvées) et zéro axiome non standard. La méthodologie repose sur :

• Définition PF-PINI : Utilisation du paramètre d'Isolation de Non-Interférence par Sonde sur Corps Premier (PF-PINI), qui quantifie la fuite d'un gadget à un seul fil sous un seul masque arithmétique. Un gadget est PF-PINI($M$) si la cardinalité de l'image réciproque de n'importe quelle valeur de sortie est au plus $M$.
• Modélisation de Pipeline : Définition d'un pipeline à $k$ étapes où chaque étape $G_i$ est un gadget PF-PINI, séparé par des masques aléatoires frais. La sortie du pipeline est calculée de manière récursive.
• Analyse Combinatoire : Démonstration que le masquage frais entre les étapes « efface » les paramètres de fuite des étapes intermédiaires, laissant la borne finale dépendante uniquement du paramètre de la dernière étape.
• Modélisation Fidèle au Matériel : Modélisation de la réduction de Montgomery pour tenir compte des largeurs de registres matériels et du comportement de dépassement, en analysant spécifiquement le décalage de collision $2^{w-s}$.

Contributions Clés
L'article apporte quatre contributions principales, toutes formalisées dans Lean 4 :

1. Le Théorème de Composition à $k$ Étapes (Théorème 3.1) :
   Ce théorème généralise le résultat précédent de composition à deux étapes à une profondeur arbitraire $k \ge 1$. Il prouve que pour un pipeline de gadgets $G_0, \dots, G_{k-1}$ avec un masquage frais entre les étapes, la cardinalité de l'image réciproque de la sortie est bornée par :
   $$| \{ (m, f) : \text{sortie du pipeline} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   Crucialement, la borne est déterminée par la dernière étape ; les paramètres de toutes les étapes intermédiaires sont effacés par les masques frais.

2. La Réduction de Montgomery est PF-PINI(2) (Théorème 4.3) :
   L'article prouve formellement que la réduction de Montgomery satisfait la propriété PF-PINI(2), reflétant la structure de la réduction de Barrett. Il démontre que l'application de Montgomery fidèle au matériel possède une structure « à deux branches » (dépendante de la survenue d'un dépassement), résultant en une cardinalité d'image réciproque d'au plus 2. Le Théorème 4.7 établit en outre la précision de cette borne, montrant que pour des paramètres standards (ML-KEM et ML-DSA), la multiplicité est exactement 2.

3. Borne de Multiplicité de Bout en Bout (Théorème 5.1) :
   En combinant le théorème de composition à $k$ étapes avec les résultats spécifiques PF-PINI(2) pour Barrett (Article 5), Montgomery (cet article) et les papillons (Article 4), l'article établit une borne unifiée. Pour tout pipeline à $k$ étapes où chaque étape satisfait $\text{maxMult} \le 2$, la cardinalité de l'image réciproque de la sortie est bornée par :
   $$2 \cdot q^{2k-2}$$
   Sous le modèle de sondage d'ordre un avec des masques uniformes, cela correspond à une borne de probabilité conditionnelle par observation de $2/q$, indépendante de la profondeur du pipeline $k$.

4. Ancrage Formel des Résultats Empiriques (Théorème 5.4) :
   L'article fournit une condition vérifiée par Lean stipulant que si une étape quelconque d'un pipeline a un $\text{maxMult} \ge 3$ (par exemple, une étape non masquée), l'hypothèse de la borne de bout en bout échoue. Cela ancre formellement les analyses empiriques et structurelles antérieures de l'accélérateur PQC « Adams Bridge » (Articles 1, 2 et travaux externes), confirmant que des configurations non masquées spécifiques dans cette conception tombent en dehors des conditions suffisantes pour la borne indépendante de la profondeur.

Résultats

• Universalité de la Barrière 1-Bit : L'article confirme que la « Barrière 1-Bit » (une cardinalité d'image réciproque de 2) s'applique aux deux réductions modulaires standard (Barrett et Montgomery) utilisées dans le matériel PQC du NIST.
• Indépendance de la Profondeur : Les preuves formelles démontrent que l'ajout d'étapes à un pipeline ne dégrade pas la borne de fuite par observation, à condition d'utiliser un masquage frais entre les étapes et que chaque étape satisfasse PF-PINI($\le 2$).
• Statut de Vérification : L'artefact entier se compose de 20 déclarations répartis sur trois modules de théorèmes, compilant en 1 753 tâches avec zéro erreur, zéro sorry et aucune procédure de décision native.

Signification et Revendications
L'article se positionne comme l'achèvement d'un programme de vérification formelle pour le matériel NTT masqué. Sa signification réside dans la fourniture d'une fondation compositionnelle quantitative et vérifiée par machine pour les concepteurs matériels.

• Pour la Certification : La borne de cardinalité dérivée ($2 \cdot q^{2k-2}$) fournit les preuves spécifiques requises pour les arguments de résistance à la DPA au niveau de l'architecture, complétant les outils de niveau porte comme SILVER et maskVerif.
• Pour les Concepteurs : Il offre une voie de remédiation prescriptive : pour atteindre une borne indépendante de la profondeur, les concepteurs doivent s'assurer que chaque étape est PF-PINI($\le 2$) et insérer des masques frais entre les étapes.
• Modestie des Revendications : Les auteurs déclarent explicitement que les interprétations de probabilité et d'entropie min (par exemple, $2/q$) sont des conséquences sémantiques informelles des bornes de cardinalité et ne sont pas mécaniquement formalisées dans Lean. De plus, concernant l'analyse d'Adams Bridge, l'article revendique uniquement que des configurations spécifiques échouent aux conditions suffisantes du Théorème 5.1 ; il ne revendique pas que le matériel est « cassé » ou « insecure », reconnaissant que des cadres alternatifs ou des modèles plus forts pourraient aboutir à des conclusions différentes. Le travail est présenté comme un outil pour l'analyse compositionnelle plutôt que comme un verdict de sécurité définitif sur des implémentations spécifiques.