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

Sintesi Tecnica: La Barriera a 1 Bit è Universale

Enunciato del Problema
La Trasformata Numerica Teorica (NTT) funge da spina dorsale computazionale per gli standard di crittografia post-quantistica (PQC) del NIST ML-DSA (FIPS 204) e ML-KEM (FIPS 203). Le implementazioni hardware di questi standard si affidano alla mascheratura aritmetica per resistere agli attacchi tramite analisi dei canali laterali, in particolare l'Analisi della Potenza Differenziale (DPA). Sebbene la mascheratura booleana su $GF(2^n)$ abbia stabilito framework di composabilità (ad esempio, PINI), la mascheratura aritmetica su $\mathbb{Z}_q$ per $q$ primo presenta sfide uniche.

I lavori precedenti nel programma QANARY (Carte 1–6) hanno stabilito analisi delle dipendenze strutturali e quantificato i margini di sicurezza per componenti specifici, dimostrando in particolare che la riduzione di Barrett soddisfa una "Barriera a 1 Bit" (PF-PINI(2)). Tuttavia, rimanevano due lacune critiche:

1. Profondità di Pipeline Arbitraria: I teoremi di composizione precedenti erano limitati a due stadi. Non esisteva alcuna garanzia formale per pipeline a $k$ stadi arbitrari con mascheratura fresca tra gli stadi.
2. Riduzione di Montgomery: Sebbene la riduzione di Barrett fosse stata caratterizzata, la riduzione di Montgomery — la seconda riduzione modulare standard utilizzata nell'hardware NTT (dominante nelle implementazioni ML-DSA e in alcune di ML-KEM) — mancava di una caratterizzazione formale PF-PINI.
3. Limiti Unificati End-to-End: Non esisteva un singolo limite di cardinalità verificato da macchina che assemblasse i risultati per pipeline arbitrarie composte da farfalle, riduzioni di Barrett e riduzioni di Montgomery.

Metodologia
Il documento utilizza la verifica formale mediante l'assistente di prova Lean 4. L'approccio è strettamente costruttivo, con zero sorry (assunzioni non dimostrate) e zero assiomi non standard. La metodologia si basa su:

• Definizione PF-PINI: Utilizzo del parametro Probe Isolating Non-Interference su Campo Primo (PF-PINI), che quantifica la perdita di un gadget a singolo filo sotto una singola mascheratura aritmetica. Un gadget è PF-PINI($M$) se la cardinalità dell'immagine inversa di qualsiasi valore di output è al massimo $M$.
• Modellazione della Pipeline: Definizione di una pipeline a $k$ stadi in cui ogni stadio $G_i$ è un gadget PF-PINI, separato da maschere casuali fresche. L'output della pipeline è calcolato ricorsivamente.
• Analisi Combinatoria: Dimostrazione che la mascheratura fresca tra gli stadi "cancella" i parametri di perdita degli stadi intermedi, lasciando il limite finale dipendente solo dal parametro dell'ultimo stadio.
• Modellazione Fedele all'Hardware: Modellazione della riduzione di Montgomery per tenere conto delle larghezze dei registri hardware e del comportamento di wraparound, analizzando specificamente l'offset di collisione $2^{w-s}$.

Contributi Chiave
Il documento apporta quattro contributi principali, tutti formalizzati in Lean 4:

1. Il Teorema di Composizione a $k$ Stadi (Teorema 3.1):
   Questo teorema generalizza il precedente risultato di composizione a due stadi a una profondità arbitraria $k \ge 1$. Dimostra che per una pipeline di gadget $G_0, \dots, G_{k-1}$ con mascheratura fresca tra gli stadi, la cardinalità dell'immagine inversa dell'output è limitata da:
   $$| \{ (m, f) : \text{output pipeline} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$$
   Crucialmente, il limite è determinato dall'ultimo stadio; i parametri di tutti gli stadi intermedi sono cancellati dalle maschere fresche.

2. La Riduzione di Montgomery è PF-PINI(2) (Teorema 4.3):
   Il documento dimostra formalmente che la riduzione di Montgomery soddisfa la proprietà PF-PINI(2), rispecchiando la struttura della riduzione di Barrett. Dimostra che la mappa di Montgomery fedele all'hardware ha una struttura a "due rami" (dipendente dal fatto che si verifichi un wraparound), risultando in una cardinalità dell'immagine inversa di al massimo 2. Il Teorema 4.7 stabilisce ulteriormente la strettezza di questo limite, mostrando che per parametri standard (ML-KEM e ML-DSA), la molteplicità è esattamente 2.

3. Limite di Molteplicità End-to-End (Teorema 5.1):
   Combinando il teorema di composizione a $k$ stadi con i risultati specifici PF-PINI(2) per Barrett (Carta 5), Montgomery (questo documento) e farfalle (Carta 4), il documento stabilisce un limite unificato. Per qualsiasi pipeline a $k$ stadi in cui ogni stadio soddisfa $\text{maxMult} \le 2$, la cardinalità dell'immagine inversa dell'output è limitata da:
   $$2 \cdot q^{2k-2}$$
   Sotto il modello di sonda del primo ordine con maschere uniformi, ciò corrisponde a un limite di probabilità condizionale per osservazione di $2/q$, indipendente dalla profondità della pipeline $k$.

4. Ancoraggio Formale dei Risultati Empirici (Teorema 5.4):
   Il documento fornisce una condizione verificata in Lean che afferma che se qualsiasi stadio in una pipeline ha $\text{maxMult} \ge 3$ (ad esempio, uno stadio non mascherato), l'ipotesi del limite end-to-end fallisce. Questo ancoraggio formalizza le precedenti analisi empiriche e strutturali dell'acceleratore PQC "Adams Bridge" (Carte 1, 2 e lavori esterni), confermando che specifiche configurazioni non mascherate in quel progetto rientrano al di fuori delle condizioni sufficienti per il limite indipendente dalla profondità.

Risultati

• Universalità della Barriera a 1 Bit: Il documento conferma che la "Barriera a 1 Bit" (una cardinalità dell'immagine inversa di 2) si applica a entrambe le riduzioni modulari standard (Barrett e Montgomery) utilizzate nell'hardware PQC del NIST.
• Indipendenza dalla Profondità: Le prove formali dimostrano che l'aggiunta di stadi a una pipeline non degrada il limite di perdita per osservazione, a condizione che venga utilizzata una mascheratura fresca tra gli stadi e che ogni stadio soddisfi PF-PINI($\le 2$).
• Stato di Verifica: L'intero artefatto consiste in 20 dichiarazioni distribuite su tre moduli di teoremi, compilati in 1.753 job con zero errori, zero sorry e nessuna procedura decisionale nativa.

Significato e Affermazioni
Il documento si posiziona come il completamento di un programma di verifica formale per l'hardware NTT mascherato. Il suo significato risiede nel fornire una base composizionale quantitativa e verificata da macchina per i progettisti hardware.

• Per la Certificazione: Il limite di cardinalità derivato ($2 \cdot q^{2k-2}$) fornisce la prova specifica richiesta per gli argomenti di resistenza alla DPA a livello di architettura, complementando strumenti a livello di porta come SILVER e maskVerif.
• Per i Progettisti: Offre un percorso prescrittivo di rimedio: per ottenere un limite indipendente dalla profondità, i progettisti devono garantire che ogni stadio sia PF-PINI($\le 2$) e inserire maschere fresche tra gli stadi.
• Modestia delle Affermazioni: Gli autori dichiarano esplicitamente che le interpretazioni di probabilità e entropia minima (ad esempio, $2/q$) sono conseguenze semantiche informali dei limiti di cardinalità e non sono formalizzate meccanicamente in Lean. Inoltre, riguardo all'analisi di Adams Bridge, il documento afferma solo che specifiche configurazioni non soddisfano le condizioni sufficienti del Teorema 5.1; non afferma che l'hardware sia "rotto" o "insicuro", riconoscendo che framework alternativi o modelli più forti potrebbero portare a conclusioni diverse. Il lavoro è inquadrato come uno strumento per l'analisi composizionale piuttosto che come un verdetto definitivo sulla sicurezza di implementazioni specifiche.