💻 computer science

Formal Verification of Probing Security via Conditional Independence

Questo articolo propone un nuovo approccio di verifica formale per la sicurezza contro le sonde degli algoritmi crittografici mascherati, sfruttando la logica di separazione probabilistica (Lilac) per stabilire una connessione tra le proprietà di non interferenza e l'indipendenza condizionata.

Autori originali: Satoshi Kura, Katsuyuki Takashima

Pubblicato 2026-05-25

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Satoshi Kura, Katsuyuki Takashima

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di cercare di mantenere al sicuro una ricetta segreta in una cucina affollata e rumorosa. Nel mondo della crittografia, questa "ricetta segreta" è una chiave privata, e il "rumore" è un attacco a canale laterale. Gli attaccanti non cercano di violare la matematica; cercano di spiare le "perdite" (come il consumo energetico o i tempi di esecuzione) mentre il computer elabora i numeri per indovinare il tuo segreto.

Per fermare ciò, i crittografi utilizzano una tecnica chiamata Mascheramento. Pensa al mascheramento come a un frullatore che sminuzza la tua ricetta segreta in $t+1$ pezzi di carta (azioni). Ne dai uno a ciascuno di $t+1$ cuochi diversi. Finché un intercettatore può spiare solo $t$ pezzi (o meno), vede solo un nonsense casuale. Non può ricostruire la ricetta perché manca almeno un pezzo cruciale.

Tuttavia, dimostrare che una ricetta complessa (algoritmo) è davvero sicura è incredibilmente difficile. Se provi a controllarla a mano, potresti trascurare una minuscola perdita e l'intero sistema di sicurezza fallisce. È qui che entra in gioco il documento.

Il Problema: Controllare la "Perdita"

Gli autori vogliono costruire una prova formale (una garanzia matematica) che un algoritmo mascherato sia sicuro. Tradizionalmente, ciò viene fatto utilizzando il concetto di "Simulatore".

L'idea del Simulatore: Immagina una scatola magica (il simulatore) che cerca di ricreare esattamente ciò che vede l'intercettatore. Se la scatola magica può creare la stessa identica "perdita" utilizzando solo le informazioni pubbliche (come l'elenco degli ingredienti) e senza aver mai visto i pezzi della ricetta segreta, allora l'algoritmo reale è sicuro. L'intercettatore non impara nulla di nuovo.

Ma costruire questi simulatori a mano è soggetto a errori. Gli autori volevano un modo migliore per dimostrarlo.

La Soluzione: Un Nuovo Strumento Logico (Lilac)

Gli autori introducono una connessione tra i "Simulatori" e un concetto chiamato Indipendenza Condizionale.

L'Analogia: Immagina di cercare di indovinare il compleanno di un amico (il segreto).
- Scenario A: Conosci la sua età e il mese in cui è nato (Informazioni Pubbliche).
- Scenario B: Conosci anche la voce del suo diario segreto (Informazioni Segrete).
- Indipendenza Condizionale: Se conoscere la voce del diario non cambia la tua ipotesi sul compleanno una volta che già conosci età e mese, allora il diario è "condizionalmente indipendente" dal compleanno dato l'età/il mese.

Il documento dimostra che se esiste un simulatore, allora il segreto è condizionalmente indipendente dalla perdita, date le informazioni pubbliche.

Per verificare ciò matematicamente, utilizzano uno strumento chiamato Lilac.

Cos'è Lilac? Pensa a Lilac come a un regolamento molto rigoroso e superpotente per la probabilità. È come un gioco di logica in cui devi dimostrare che due mazzi di carte (variabili casuali) sono mescolati indipendentemente l'uno dall'altro.
La "Congiunzione Separante": In questo regolamento, c'è un simbolo speciale (come una bacchetta magica) che dice: "Questi due mazzi di carte sono totalmente separati e non si influenzano a vicenda".
L'Innovazione: Gli autori hanno aggiunto nuove regole a questo regolamento per gestire la "Condizionamento" (la parte "dato che..."). Questo permette loro di dimostrare che anche se l'intercettatore vede alcuni dati, ciò non rivela il segreto perché hanno già i dati pubblici.

Cosa Hanno Effettivamente Fatto

Gli autori non hanno parlato solo di teoria; hanno costruito un sistema per verificare algoritmi crittografici reali utilizzando questa nuova logica. Hanno applicato il loro metodo a tre specifici "ingranaggi" (mattoni fondamentali) utilizzati nella crittografia moderna:

MINIADDREPNOISE: Uno strumento utilizzato per aggiungere rumore casuale ai dati (come aggiungere sale a una zuppa per nascondere il sapore originale). Hanno dimostrato che anche se un attaccante spia parte della zuppa salata, non può capire il sapore originale.
REFRESH: Uno strumento che prende i pezzi sminuzzati del segreto e li rimescola in modo che appaiano nuovi di zecca, impedendo agli attaccanti di tracciarli nel tempo. Hanno dimostrato che questo rimescolamento è sicuro.
SECMULT (Moltiplicazione Sicura): Uno strumento che moltiplica due numeri segreti tra loro senza rivelare il risultato fino alla fine. Questa è una delle operazioni più difficili da proteggere. Hanno dimostrato che questa moltiplicazione è sicura contro gli attacchi "t-probing".

La Conclusione

Il documento afferma che traducendo il concetto complesso di "Simulatori" nel linguaggio dell'"Indipendenza Condizionale", possono utilizzare il sistema logico Lilac per verificare automaticamente e rigorosamente che questi strumenti crittografici siano sicuri.

Hanno dimostrato con successo ciò scrivendo prove formali per MINIADDREPNOISE, REFRESH e SECMULT, mostrando che questi specifici algoritmi soddisfano i rigorosi requisiti di sicurezza necessari per proteggere i segreti dagli attacchi a canale laterale. Non hanno affermato di risolvere tutti i futuri problemi di sicurezza o di applicare ciò a dispositivi medici; il loro lavoro riguarda strettamente la dimostrazione della sicurezza di queste specifiche operazioni matematiche crittografiche utilizzando un nuovo quadro logico.

Riepilogo Tecnico: Verifica Formale della Sicurezza contro le Sonde tramite Indipendenza Condizionata

Enunciato del Problema

Gli attacchi side-channel costituiscono una minaccia significativa per la sicurezza degli schemi crittografici, spingendo all'adozione diffusa del masking come contromisura. Il masking suddivide i valori segreti in condivisioni (share) per garantire che la fuoriuscita di informazioni da qualsiasi sottoinsieme di valori intermedi non riveli il segreto sottostante. Tuttavia, dimostrare la sicurezza degli algoritmi mascherati, in particolare sotto il modello di probing ISW (dove un avversario può sondare fino a $t$ valori intermedi), è notoriamente soggetto a errori se eseguito manualmente. Sono stati identificati diversi difetti nelle dimostrazioni di sicurezza manuali, rendendo necessaria la verifica formale.

Sebbene la logica di separazione probabilistica sia stata applicata con successo per verificare proprietà come l'indipendenza dagli input (ad esempio, nei one-time pad), non è ancora stata utilizzata per verificare la sicurezza contro le sonde (nello specifico la $t$ -noninterferenza) degli algoritmi mascherati. Gli strumenti esistenti di verifica formale spesso si basano su metodi basati sulla sostituzione o sull'inferenza di tipi, che possono mancare della modularità o dell'espressività necessarie per il ragionamento condizionale complesso sull'indipendenza intrinseco al masking.

Metodologia

Questo lavoro propone un approccio innovativo alla verifica formale stabilendo una connessione rigorosa tra le definizioni di sicurezza basate su simulatori e l'indipendenza condizionata. La metodologia si basa su Lilac, una logica di separazione probabilistica progettata per ragionare sull'indipendenza condizionata.

1. Fondamento Teorico: Simulatori e Indipendenza Condizionata

Gli autori riformulano la definizione standard di noninterferenza basata sui simulatori in termini di indipendenza condizionata.

Visione basata sui simulatori: Un algoritmo mascherato è sicuro se, per qualsiasi insieme di sonde $O$ (osservate da un avversario), esiste un simulatore in grado di generare la distribuzione di $O$ utilizzando solo un sottoinsieme di condivisioni di input $I$ , senza accesso alle restanti condivisioni segrete.
Visione basata sull'indipendenza condizionata: Questo requisito di sicurezza è equivalente all'affermazione che i valori osservati $O$ sono condizionalmente indipendenti dalle condivisioni di input segrete ( $\Delta \setminus I$ ) date le condivisioni di input pubbliche $I$ . Formalmente, ciò è espresso come $O \perp (\Delta \setminus I) \mid I$ .

Il documento dimostra che questa equivalenza vale all'interno del quadro semantico di Lilac, che modella l'indipendenza probabilistica utilizzando combinazioni indipendenti di spazi di probabilità e condizionamento tramite disintegrazione.

2. Estensione di Lilac

Per applicare Lilac alla sicurezza contro le sonde, gli autori estendono la logica con regole di prova specifiche che non erano presenti nella formulazione originale di Lilac:

Assiomi Semi-Graphoid: Il documento dimostra che gli assiomi semi-graphoid per l'indipendenza condizionata (Simmetria, Decomposizione, Debole Unione e Contrazione) valgono all'interno della semantica di Lilac. Questi assiomi sono cruciali per manipolare le affermazioni di indipendenza condizionata durante le dimostrazioni.
Regole di Composabilità: Vengono introdotte nuove regole per gestire la composizione delle proprietà di noninterferenza, specificamente per la composizione sequenziale e i cicli for. Queste regole consentono la verifica modulare di algoritmi complessi costruiti a partire da componenti più piccoli (gadgets).
Proprietà e Indebolimento: Regole aggiuntive facilitano il ragionamento sulla proprietà delle variabili casuali e sull'indebolimento delle proprietà di noninterferenza quando si trattano input non condivisi o sottoinsiemi di variabili.

3. Quadro di Verifica

Il processo di verifica comporta:

La traduzione degli algoritmi mascherati (scritti nel linguaggio di programmazione probabilistica APPL) in triple di Hoare all'interno di Lilac.
L'uso dell'equivalenza stabilita (Teorema V.1) per ridurre la verifica della $(I, O)$ -noninterferenza alla dimostrazione di una specifica tripla di Hoare di indipendenza condizionata:
$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$
L'applicazione dell'insieme esteso di regole di prova (inclusi i nuovi assiomi semi-graphoid e le regole di composabilità) per derivare le implicazioni richieste.

Contributi Chiave

Connessione Formale: Il documento stabilisce un'equivalenza formale tra le definizioni di sicurezza contro le sonde basate su simulatori e le proprietà di indipendenza condizionata esprimibili in Lilac. Questo colma il divario tra le nozioni di sicurezza crittografica e la logica di separazione probabilistica.
Estensione di Lilac: Gli autori forniscono una suite di regole di prova aggiuntive necessarie per verificare gli algoritmi mascherati, inclusi gli assiomi semi-graphoid per l'indipendenza condizionata e le regole di composabilità per la composizione sequenziale e i cicli.
Casi di Studio: L'efficacia dell'approccio è dimostrata verificando formalmente la sicurezza contro le sonde di tre algoritmi critici utilizzando Lilac:
- MINIADDREPNOISE: Una subroutine per aggiungere rumore uniforme ai valori mascherati.
- REFRESH: Un algoritmo fondamentale per il rinnovo delle condivisioni per prevenire l'accumulo di fuoriuscite di informazioni.
- SECMULT: Un algoritmo standard di moltiplicazione mascherata.
- ADDREPNOISEER: Una variante utilizzata nello schema di firma Raccoon (un candidato per la standardizzazione della Crittografia Post-Quantistica NIST), dimostrando che soddisfa la proprietà di $t$ -Strong Noninterference con Input Non Condiviso ( $t$ -SNIU).

Risultati

Il documento deriva con successo le triple di Hoare per gli algoritmi target, confermando le loro proprietà di noninterferenza.

Per MINIADDREPNOISE, la dimostrazione mostra che le condivisioni di output sono condizionalmente indipendenti dalle condivisioni di input non osservate, date le input osservate.
Per REFRESH, la dimostrazione verifica che l'algoritmo soddisfa la $t$ -Strong Noninterference ( $t$ -SNI), una proprietà più forte della noninterferenza standard, essenziale per la composabilità nel masking di ordine superiore.
Per SECMULT e ADDREPNOISEER, le dimostrazioni sfruttano le nuove regole di composabilità per gestire i cicli annidati e le complesse dipendenze dei dati intrinseche a questi algoritmi.

La verifica di ADDREPNOISEER è particolarmente significativa in quanto convalida un componente chiave della dimostrazione di sicurezza dello schema di firma Raccoon, che si basa sulla proprietà $t$ -SNIU.

Significato e Affermazioni

Gli autori affermano che questo lavoro fornisce la prima applicazione della logica di separazione probabilistica (nello specifico Lilac) alla verifica formale della sicurezza contro le sonde per gli algoritmi mascherati. Traducendo le dimostrazioni di sicurezza in ragionamenti sull'indipendenza condizionata, l'approccio offre un'alternativa modulare e logicamente rigorosa agli strumenti esistenti basati sulla sostituzione o sull'inferenza di tipi.

Il documento sottolinea che, sebbene l'idea sottostante di collegare i simulatori all'indipendenza condizionata sia concettualmente semplice, la sua formalizzazione in Lilac è tecnicamente non banale a causa della dipendenza della logica dalle combinazioni indipendenti piuttosto che dagli spazi di probabilità prodotto standard. La corretta derivazione del teorema principale e l'applicazione a componenti crittografici reali (Raccoon) dimostrano che questo quadro è fattibile per verificare schemi di masking complessi e di ordine elevato.

Il lavoro rimane modesto riguardo al suo ambito, notando che i risultati attuali sono limitati al contesto informazionale della sicurezza contro le sonde. Gli autori identificano l'estensione dell'approccio al contesto computazionale e l'implementazione del metodo in un dimostratore di teoremi interattivo come direzioni importanti per il lavoro futuro. Suggeriscono inoltre che il quadro potrebbe essere applicato ad altre proprietà di sicurezza basate su simulatori, come quelle presenti nel calcolo multipartito sicuro.