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

1. Enunciato del Problema

Gli standard di Crittografia Post-Quantistica (PQC) come ML-KEM (FIPS 203) e ML-DSA (FIPS 204) si basano pesantemente su pipeline della Trasformata Numerica Teorica (NTT). Queste pipeline sono costituite da stadi lineari "a farfalla" e stadi non lineari di riduzione modulare, tipicamente implementati utilizzando la riduzione di Barrett.

Sebbene gli attuali framework di verifica formale (ISW, t-SNI, PINI, DOM) offrano garanzie solide per il mascheramento booleano su $GF(2)$, mancano di caratterizzazioni verificate formalmente per il mascheramento aritmetico su campi primi ($\mathbb{Z}_q$), specificamente per la riduzione di Barrett.

• Il Divario: Le implementazioni hardware (ad esempio, il design "Adams Bridge") spesso soffrono di vulnerabilità a canali laterali perché la sottrazione condizionale non lineare nella riduzione di Barrett rompe la struttura affine assunta dai teoremi di composizione standard.
• La Domanda: Sotto mascheramento aritmetico del primo ordine, qual è il limite preciso di fuga dei fili interni di un circuito di riduzione di Barrett? Gli strumenti precedenti non potevano fornire una risposta universale verificata formalmente, portando a incertezza nella certificazione FIPS 140-3.

2. Metodologia

Gli autori adottano un approccio di verifica formale utilizzando l'assistente alla dimostrazione Lean 4 e la libreria Mathlib.

• Formalizzazione: Definiscono la mappa dei fili interni di Barrett algebricamente su $\mathbb{Z}_q$ (dove $q$ è il modulo). La mappa $f_x(m)$ prende un segreto $x$ e una maschera casuale $m$, producendo un output basato su una struttura a due rami determinata da una sottrazione condizionale.
• Strategia di Dimostrazione: Invece di simulare istanze specifiche, dimostrano teoremi universali che valgono per tutti $q > 0$ e parametri di spostamento $s$.
• Concetto Chiave: Analizzano la cardinalità dell'immagine inversa: per un segreto fisso $x$ e un valore di output specifico $v$, quanti maschere distinte $m$ potrebbero aver prodotto $v$?
• Catena di Strumenti: L'artefatto contiene 12 risultati dimostrati con zero sorry (nessuna dimostrazione incompleta), garantendo che ogni passaggio sia verificato dal kernel di Lean.

3. Contributi Chiave

A. Il Teorema della Tricotomia

Il documento dimostra che la mappa dei fili interni di Barrett esibisce una struttura a tre valori per l'immagine inversa. Per qualsiasi segreto $x$ e qualsiasi output $v$, il numero di maschere $m$ tale che $f_x(m) = v$ è esattamente 0, 1 o 2.

• Meccanismo: La sottrazione condizionale crea due rami affini (traslazioni in $\mathbb{Z}_q$). L'immagine inversa di qualsiasi valore è un sottoinsieme di al massimo due candidati: $\{x - v, x - v + r\}$, dove $r = 2^s \mod q$.
• Universalità: Questo vale per qualsiasi modulo $q$ e spostamento $s$, indipendentemente dai parametri specifici della PQC.

B. La Barriera a 1 Bit

Sulla base della tricotomia, gli autori stabiliscono un limite universale di fuga:

• Massima Multiplicità: Poiché il numero massimo di maschere che producono un singolo output è 2, la probabilità massima di osservare un valore di output specifico è $2/q$.
• Limite di Min-Entropia: La min-entropia condizionale $H_\infty(\text{output} \mid x)$ è limitata inferiormente da $\log_2(q) - 1$.
• Interpretazione: La riduzione di Barrett disperde al massimo 1 bit di min-entropia per filo interno sotto sondaggio del primo ordine. Questo è un limite "conservativo" perché molti valori di output sono irraggiungibili (conteggio immagine inversa = 0), il che significa che la fuga effettiva è spesso strettamente inferiore a 1 bit.

C. Il Framework PF-PINI

Gli autori introducono PF-PINI (Prime-Field PINI), una nuova metrica di sicurezza per gadget aritmetici su $\mathbb{Z}_q$:

• Definizione: Un gadget è PF-PINI($k$) se la cardinalità dell'immagine inversa è limitata da $k$.
• Istanze:
  • Stadi a Farfalla: Soddisfano PF-PINI(1) (bijezione perfetta, fuga zero oltre la maschera).
  • Riduzione di Barrett: Soddisfa PF-PINI(2) (la Barriera a 1 Bit).
• Osservazione sulla Composizione: Osservano (sebbene non ancora formalmente dimostrato) che se gli stadi della pipeline sono separati da mascheramento fresco inter-stadio, la massima multiplicità della pipeline composta è $\max(k_1, k_2)$. Questo implica che la Barriera a 1 Bit si propaga attraverso l'intera pipeline NTT.

4. Risultati e Analisi

• Dimostrazioni Verificate Formalmente: L'artefatto include 12 teoremi verificati, inclusa la tricotomia, dimostrazioni di strettezza (che mostrano che il conteggio=2 è raggiungibile) e istanze PF-PINI.
• Scoperta del Divario di Supporto: L'analisi rivela valori di output "irraggiungibili" (conteggio immagine inversa = 0). Questa è una caratteristica di sicurezza, non un bug, in quanto riduce l'informazione effettiva a disposizione dell'avversario.
• Caso di Studio Adams Bridge: Il documento analizza l'implementazione hardware "Adams Bridge":
  • Guasto intra-stadio: Lavori precedenti (Documenti 1 e 2) hanno mostrato vulnerabilità dovute all'interazione delle quote senza mascheramento intermedio.
  • Guasto inter-stadio: Questo documento identifica che Adams Bridge non applica mascheramento fresco tra gli stadi. Di conseguenza, il limite di composizione PF-PINI non si applica, permettendo alla fuga di moltiplicarsi ($k_1 \times k_2$) invece di rimanere limitata dal massimo ($\max(k_1, k_2)$). Questo spiega perché il design è vulnerabile nonostante la Barriera a 1 Bit esista per le singole porte di Barrett.
• Impatto Quantitativo:
  • Per ML-KEM ($q=3329$): Fuga $\le 1$ bit (Min-entropia $\ge 10.70$ bit).
  • Per ML-DSA ($q=8.380.417$): Fuga $\le 1$ bit (Min-entropia $\ge 21.99$ bit).

5. Significato

• Prontezza per la Certificazione: La Barriera a 1 Bit fornisce un certificato universale e verificato formalmente per i progettisti hardware. Permette agli valutatori di certificare implementazioni basate su Barrett per FIPS 140-3 senza dover riesaminare set di parametri specifici.
• Linee Guida di Progettazione: Chiarisce che il requisito architettonico primario per la sicurezza è il mascheramento fresco inter-stadio. Se questo viene implementato, la natura non lineare della riduzione di Barrett non compromette la sicurezza della pipeline NTT oltre una perdita trascurabile di 1 bit.
• Cambiamento Metodologico: Il documento sposta l'analisi dei canali laterali dalla simulazione empirica e dal controllo basato su SAT a dimostrazioni algebriche verificate dal kernel, stabilendo un nuovo standard per la verifica hardware PQC.
• Completamento del Programma a Cinque Documenti: Questo lavoro colma il divario lasciato dai precedenti documenti della serie, passando dalla costruzione di strumenti (Documento 1) e quantificazione degli attacchi (Documento 2) alle basi algebriche (Documento 3), alla composizione lineare (Documento 4) e, infine, alla caratterizzazione non lineare (Documento 5).

6. Limitazioni e Lavori Futuri

• Dimostrazione di Composizione: L'affermazione che $\max(k_1, k_2)$ valga per pipeline composte con mascheramento fresco è attualmente un'osservazione, non un teorema formale.
• Mascheramento di Ordine Superiore: I risultati sono limitati al mascheramento del primo ordine ($t=1$). La sicurezza di ordine superiore richiede l'analisi di immagini inverse congiunte su più fili.
• Formalizzazione dell'Entropia: Sebbene il limite algebrico sia dimostrato, il limite di min-entropia informativo-teorico si basa su definizioni standard non ancora completamente integrate in Mathlib.
• Altre Riduzioni: I risultati sono specifici per la riduzione di Barrett; le riduzioni Montgomery e schoolbook richiedono analisi separate.

In sintesi, questo documento stabilisce che la riduzione di Barrett è fondamentalmente sicura sotto mascheramento aritmetico del primo ordine, disperdendo non più di 1 bit di informazione per filo, a condizione che venga applicato un mascheramento fresco tra gli stadi della pipeline. Questo fornisce una base matematica rigorosa per la sicurezza dell'hardware PQC di prossima generazione.