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

1. Enunciazione del Problema

Il documento affronta una lacuna critica nella verifica formale della sicurezza dell'hardware per la Crittografia Post-Quantistica (PQC), specificamente per le implementazioni della Trasformata Numerica Teorica (NTT) utilizzate negli standard NIST (ML-KEM e ML-DSA).

• Il Contesto: Le implementazioni hardware della NTT si affidano alla mascheratura aritmetica su campi primi ($\mathbb{Z}_q$) per resistere ad attacchi tramite analisi di canali laterali come l'Analisi di Potenza Differenziale (DPA).
• La Lacuna: Mentre la mascheratura booleana (su $GF(2^n)$) dispone di una teoria della composizione matura (NI, SNI, PINI) con prove verificate meccanicamente, la mascheratura aritmetica su campi primi manca di teoremi di composizione analoghi.
• Il Problema Specifico: Nella mascheratura aritmetica, operazioni come la riduzione modulare (ad esempio, la riduzione di Barrett) interagiscono con le maschere in modi non banali. A differenza dell'XOR booleano, dove la mascheratura preserva perfettamente l'uniformità, la mascheratura aritmetica può risultare in distribuzioni di output non uniformi (molteplicità > 1).
• La Vulnerabilità: Analisi empiriche e studi strutturali precedenti hanno identificato vulnerabilità nell'acceleratore PQC "Adams Bridge" di Microsoft, dove i fili intermedi tra gli stadi della pipeline erano non uniformi, consentendo attacchi DPA. Tuttavia, mancava una spiegazione teorica formale del perché ciò accade e di come risolverlo tramite teoremi di composizione.

2. Metodologia

Gli autori impiegano la verifica formale utilizzando l'assistente di prova Lean 4 per derivare e dimostrare teoremi di composizione per la mascheratura aritmetica.

• Modello Formale: Definiscono una metrica di sicurezza quantitativa chiamata PF-PINI(k) (Prime-Field Probe Isolating Non-Interference).
  • A differenza delle nozioni binarie di sicurezza (sicuro/non sicuro), PF-PINI misura la molteplicità dei valori di output rispetto allo spazio delle maschere.
  • $k=1$ implica una distribuzione perfettamente uniforme.
  • $k=2$ implica una molteplicità massima di 2, che perde fino a 1 bit di informazione per filo.
• L'"Argomento di Rinnovamento": L'insight teorico fondamentale è che l'applicazione di una nuova maschera casuale tra due stadi della pipeline cancella completamente il parametro di sicurezza ($k_1$) del primo stadio dal filo intermedio, indipendentemente da quanto non uniforme fosse l'output del primo stadio.
• Collegamento Hardware: Gli autori colmano formalmente il divario tra modelli algebrici astratti ($\mathbb{Z}_q$) e l'aritmetica su numeri naturali fedele all'hardware (Nat) utilizzata nei progetti RTL, specificamente per la riduzione di Barrett.
• Ambito di Verifica: L'intero lavoro consiste in 18 teoremi verificati meccanicamente con zero stub sorry (nessuna assunzione non dimostrata), garantendo affidabilità di alto livello.

3. Contributi Chiave

Il documento apporta sei contributi principali:

1. Il Teorema di Rinnovamento (Teorema 4.1): Dimostra che se viene applicata una nuova maschera casuale tra due stadi ($G_1 \to G_2$), il filo intermedio diventa perfettamente uniforme. L'insieme delle coppie di maschere che producono un qualsiasi valore intermedio specifico ha cardinalità esattamente $q$, indipendente dal parametro di sicurezza di $G_1$.
2. Teorema di Composizione Positiva (Teorema 4.4): Dimostra che una pipeline a due stadi con mascheratura fresca soddisfa PF-PINI($k_2$). La sicurezza dell'output composto dipende solo dal parametro del secondo stadio ($k_2$); la debolezza del primo stadio ($k_1$) viene completamente cancellata.
3. Teoremi di Composizione Negativa (Teoremi 5.1–5.3): Dimostra che senza mascheratura fresca, il filo intermedio mantiene la molteplicità del primo stadio ($k_1$). Se $k_1 > 1$, il filo è non uniforme, creando una condizione necessaria per gli attacchi DPA.
4. Ponte Algebrico-Hardware (Teorema 6.1): Dimostra formalmente che la mappa di riduzione algebrica di Barrett è equivalente alla mappa aritmetica su Nat fedele all'hardware in condizioni standard di ambito ($q \le 2^s$). Questo valida che i limiti teorici si applicano direttamente alle implementazioni su silicio.
5. Diagnosi di Adams Bridge: Istante formalmente i teoremi per diagnosticare l'acceleratore Adams Bridge di Microsoft. La prova conferma che la mancanza di mascheratura fresca tra gli stadi lascia i fili di output di Barrett non uniformi (PF-PINI(2)), spiegando il successo dei precedenti attacchi DPA empirici.
6. Barriera Universale a 1 Bit: Fornisce evidenze computazionali che il limite PF-PINI(2) è universale per le riduzioni modulari (sia Barrett che Montgomery), suggerendo una fondamentale "Barriera a 1 Bit" per queste operazioni.

4. Risultati Chiave

• Prova Formale della Composizione: Il documento stabilisce che la mascheratura fresca tra gli stadi è la condizione necessaria e sufficiente per comporre gadget aritmetici in modo sicuro.
• Sicurezza Quantitativa:
  • Con Mascheratura Fresca: Il filo intermedio è uniforme ($k=1$). L'output finale è limitato dal parametro del secondo stadio ($k_2$).
  • Senza Mascheratura Fresca: Il filo intermedio è non uniforme (fino a $k_1$). Questa non uniformità è la causa radice della perdita di informazioni tramite canali laterali osservata negli attacchi empirici.
• Correzione per Adams Bridge: La diagnosi conferma che l'aggiunta di un singolo registro di maschera casuale fresca e di un'operazione di sottrazione tra gli stadi Butterfly e Barrett nella pipeline di Adams Bridge eliminerebbe la vulnerabilità DPA sui fili intermedi senza modificare il parametro di sicurezza dell'output finale.
• Disponibilità dell'Artifatto: Il codice sorgente completo in Lean 4, inclusi 18 teoremi e uno script di riproduzione, è pubblicamente disponibile, permettendo la verifica indipendente delle prove.

5. Significato

• Prima Composizione Aritmetica Verificata Meccanicamente: Questo è il primo lavoro a fornire teoremi di composizione verificati meccanicamente per la mascheratura aritmetica su campi primi, colmando un vuoto teorico maggiore nella sicurezza hardware PQC.
• Collegamento tra Teoria e Pratica: Collegando formalmente le prove algebriche astratte all'aritmetica fedele all'hardware, il documento fornisce una base rigorosa per verificare progetti reali su silicio, andando oltre i test empirici.
• Linea Guida di Progettazione: Stabilisce una regola di progettazione chiara e dimostrabile per l'hardware PQC: Inserire sempre mascheratura fresca tra gli stadi della pipeline. Questo semplice cambiamento architetturale garantisce che la sicurezza della pipeline composta sia determinata esclusivamente dal punto debole nello stadio finale, non in quelli intermedi.
• Convergenza delle Evidenze: La prova formale si allinea perfettamente con tre analisi precedenti indipendenti (analisi di potenza empirica, revisione del codice e analisi delle dipendenze strutturali), confermando che il difetto architetturale identificato nell'acceleratore Adams Bridge è effettivamente la causa radice della sua vulnerabilità.

In sintesi, questo documento fornisce l'impalcatura matematica e di verifica formale necessaria per progettare acceleratori hardware sicuri, componibili e resistenti ai canali laterali per la nuova era della Crittografia Post-Quantistica.