Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware

1. Énoncé du problème

Les standards de cryptographie post-quantique (PQC) tels que ML-KEM (FIPS 203) et ML-DSA (FIPS 204) reposent fortement sur des pipelines de transformée de Fourier numérique (NTT). Ces pipelines sont composés d'étapes linéaires de type "papillon" et d'étapes non linéaires de réduction modulaire, généralement implémentées à l'aide de la réduction de Barrett.

Bien que les cadres de vérification formelle existants (ISW, t-SNI, PINI, DOM) offrent de solides garanties pour le masquage booléen sur $GF(2)$, ils manquent de caractérisations vérifiées par machine pour le masquage arithmétique sur les corps premiers ($\mathbb{Z}_q$), spécifiquement pour la réduction de Barrett.

• Le Vide : Les implémentations matérielles (par exemple, la conception "Adams Bridge") souffrent souvent de vulnérabilités de canal latéral car la soustraction conditionnelle non linéaire dans la réduction de Barrett brise la structure affine supposée par les théorèmes de composition standards.
• La Question : Sous un masquage arithmétique d'ordre un, quelle est la borne précise de fuite des fils internes d'un circuit de réduction de Barrett ? Les outils précédents ne pouvaient pas fournir de réponse universelle vérifiée par machine, entraînant une incertitude dans la certification FIPS 140-3.

2. Méthodologie

Les auteurs emploient une approche de vérification formelle utilisant l'assistant de preuve Lean 4 et la bibliothèque Mathlib.

• Formalisation : Ils définissent la carte des fils internes de Barrett algébriquement sur $\mathbb{Z}_q$ (où $q$ est le module). La carte $f_x(m)$ prend un secret $x$ et un masque aléatoire $m$, produisant une sortie basée sur une structure à deux branches déterminée par une soustraction conditionnelle.
• Stratégie de preuve : Au lieu de simuler des instances spécifiques, ils prouvent des théorèmes universels valables pour tous $q > 0$ et paramètres de décalage $s$.
• Concept clé : Ils analysent la cardinalité de l'image réciproque : pour un secret $x$ fixe et une valeur de sortie spécifique $v$, combien de masques distincts $m$ auraient pu produire $v$ ?
• Chaîne d'outils : L'artefact contient 12 résultats prouvés avec zéro sorry (aucune preuve incomplète), garantissant que chaque étape est vérifiée par le noyau de Lean.

3. Contributions clés

A. Le théorème de la trichotomie

Le papier démontre que la carte des fils internes de Barrett présente une structure d'image réciproque à trois valeurs. Pour tout secret $x$ et toute sortie $v$, le nombre de masques $m$ tels que $f_x(m) = v$ est exactement 0, 1 ou 2.

• Mécanisme : La soustraction conditionnelle crée deux branches affines (translations dans $\mathbb{Z}_q$). L'image réciproque de n'importe quelle valeur est un sous-ensemble d'au plus deux candidats : $\{x - v, x - v + r\}$, où $r = 2^s \mod q$.
• Universalité : Cela vaut pour tout module $q$ et tout décalage $s$, indépendamment des paramètres spécifiques du PQC.

B. La barrière à 1 bit

Sur la base de la trichotomie, les auteurs établissent une borne de fuite universelle :

• Multiplicité maximale : Puisque le nombre maximal de masques produisant une seule sortie est 2, la probabilité maximale d'observer une valeur de sortie spécifique est $2/q$.
• Borne d'entropie minimale : L'entropie min-entropie conditionnelle $H_\infty(\text{sortie} \mid x)$ est bornée inférieurement par $\log_2(q) - 1$.
• Interprétation : La réduction de Barrett fuit au plus 1 bit d'entropie minimale par fil interne sous une sonde d'ordre un. Il s'agit d'une borne "conservatrice" car de nombreuses valeurs de sortie sont inaccessibles (nombre d'image réciproque = 0), ce qui signifie que la fuite réelle est souvent strictement inférieure à 1 bit.

C. Le cadre PF-PINI

Les auteurs introduisent PF-PINI (Prime-Field PINI), une nouvelle métrique de sécurité pour les gadgets arithmétiques sur $\mathbb{Z}_q$ :

• Définition : Un gadget est PF-PINI($k$) si la cardinalité de l'image réciproque est bornée par $k$.
• Instantiations :
  • Étapes Papillon : Satisfont PF-PINI(1) (bijection parfaite, fuite nulle au-delà du masque).
  • Réduction de Barrett : Satisfait PF-PINI(2) (la barrière à 1 bit).
• Observation de composition : Ils observent (bien que non encore prouvé formellement) que si les étapes du pipeline sont séparées par un masquage frais inter-étape, la multiplicité maximale du pipeline composé est $\max(k_1, k_2)$. Cela implique que la barrière à 1 bit se propage à travers l'ensemble du pipeline NTT.

4. Résultats et analyse

• Preuves vérifiées par machine : L'artefact comprend 12 théorèmes vérifiés, incluant la trichotomie, des preuves de précision (montrant que le comptage=2 est atteignable) et des instantiations PF-PINI.
• Découverte de l'écart de support : L'analyse révèle des valeurs de sortie "inaccessibles" (nombre d'image réciproque = 0). Il s'agit d'une fonctionnalité de sécurité, et non d'un bug, car cela réduit l'information effective de l'adversaire.
• Étude de cas Adams Bridge : Le papier analyse l'implémentation matérielle "Adams Bridge" :
  • Défaillance intra-étape : Des travaux antérieurs (Papiers 1 et 2) ont montré des vulnérabilités dues à l'interaction des parts sans masquage intermédiaire.
  • Défaillance inter-étape : Ce papier identifie que Adams Bridge omet d'appliquer un masquage frais entre les étapes. Par conséquent, la borne de composition PF-PINI ne s'applique pas, permettant à la fuite de se multiplier ($k_1 \times k_2$) plutôt que de rester bornée par le maximum ($\max(k_1, k_2)$). Cela explique pourquoi la conception est vulnérable malgré l'existence de la barrière à 1 bit pour les portes de Barrett individuelles.
• Impact quantitatif :
  • Pour ML-KEM ($q=3329$) : Fuite $\le 1$ bit (Entropie minimale $\ge 10,70$ bits).
  • Pour ML-DSA ($q=8\,380\,417$) : Fuite $\le 1$ bit (Entropie minimale $\ge 21,99$ bits).

5. Importance

• Préparation à la certification : La barrière à 1 bit fournit un certificat universel vérifié par machine pour les concepteurs matériels. Elle permet aux évaluateurs de certifier les implémentations basées sur Barrett pour FIPS 140-3 sans re-vérifier des ensembles de paramètres spécifiques.
• Guidage de conception : Elle clarifie que l'exigence architecturale principale pour la sécurité est le masquage frais inter-étape. Si cela est mis en œuvre, la nature non linéaire de la réduction de Barrett ne compromet pas la sécurité du pipeline NTT au-delà d'une perte négligeable de 1 bit.
• Changement méthodologique : Le papier fait passer l'analyse de canal latéral de la simulation empirique et de la vérification basée sur SAT aux preuves algébriques vérifiées par noyau, établissant une nouvelle norme pour la vérification matérielle du PQC.
• Complétion du programme à cinq papiers : Ce travail comble le vide laissé par les papiers précédents de la série, passant de la construction d'outils (Papier 1) et de la quantification des attaques (Papier 2) aux fondements algébriques (Papier 3), à la composition linéaire (Papier 4), et enfin, à la caractérisation non linéaire (Papier 5).

6. Limites et travaux futurs

• Preuve de composition : L'affirmation selon laquelle $\max(k_1, k_2)$ vaut pour les pipelines composés avec masquage frais est actuellement une observation, et non un théorème formel.
• Masquage d'ordre supérieur : Les résultats sont limités au masquage d'ordre un ($t=1$). La sécurité d'ordre supérieur nécessite l'analyse des images réciproques conjointes sur plusieurs fils.
• Formalisation de l'entropie : Bien que la borne algébrique soit prouvée, la borne d'entropie minimale informationnelle repose sur des définitions standards pas encore entièrement intégrées dans Mathlib.
• Autres réductions : Les résultats sont spécifiques à la réduction de Barrett ; les réductions de Montgomery et de schoolbook nécessitent une analyse séparée.

En résumé, ce papier établit que la réduction de Barrett est fondamentalement sûre sous masquage arithmétique d'ordre un, ne fuyant pas plus d'1 bit d'information par fil, à condition qu'un masquage frais soit appliqué entre les étapes du pipeline. Cela fournit une base mathématique rigoureuse pour sécuriser le matériel PQC de nouvelle génération.