Immaginate di essere un maestro fabbro di serrature che cerca di dimostrare che la sua nuova cassaforte è indistruttibile. Non vi limitate a dire: "È forte!". Dovete mostrare una sequenza di passaggi: "Se non riesci a rompere questa minuscola serratura, non puoi rompere la porta; se non puoi rompere la porta, non puoi rompere la cassaforte". È così che funziona la crittografia moderna. Gli esperti utilizzano dei "giochi" per testare la sicurezza, dove un hacker cerca di indovinare un segreto, e la sicurezza di un sistema viene dimostrata mostrando che violarlo è difficile quanto risolvere un enigma noto e impossibile. Ma ecco il problema: eseguire queste dimostrazioni a mano è come cercare di bilanciare una casa di carte in un uragano. È facile commettere un piccolo errore, trascurare una sottile lacuna o perdersi nella complessità, e se si salta un solo passaggio, l'intera dimostrazione crolla. Ecco perché gli scienziati hanno cercato un modo per far sì che un computer controllasse ogni singola carta, assicurandosi che la casa rimanga in piedi.

È qui che entra in gioco il documento. Gli autori hanno costruito un laboratorio digitale chiamato HOPSCOTCH (un nome giocoso per un gioco di saltelli) all'interno di un potente programma per computer chiamato Lean 4. Pensate a HOPSCOTCH come a un correttore di bozze robotico super intelligente che non si limita a controllare la vostra matematica; comprende la storia della dimostrazione di sicurezza. Invece di costringere i crittografi a scrivere in un linguaggio strano e limitato, HOPSCOTCH permette loro di scrivere dimostrazioni utilizzando gli stessi strumenti che usano per tutta la loro altra matematica. Trasforma il processo di "salto tra i giochi" — saltare da uno scenario di sicurezza all'altro — in un oggetto chiaro, passo dopo passo, che il computer può ispezionare, verificare e persino automatizzare. Gli autori non si sono limitati a costruire lo strumento; lo hanno usato per dimostrare con successo la sicurezza di diversi metodi di cifratura famosi, inclusa una costruzione complessa chiamata GGM, dimostrando che questo "correttore di bozze robotico" può gestire sfide crittografiche del mondo reale senza confondersi.

Il quadro generale: Perché abbiamo bisogno di un robot correttore di bozze

Nel mondo della sicurezza digitale, ci affidiamo alla "sicurezza dimostrabile". Ciò significa che non speriamo solo che i nostri codici siano sicuri; cerchiamo di dimostrarlo. Il modo standard per farlo è l'approccio basato sui "giochi". Immaginate una guardia di sicurezza (il sistema) e un ladro (l'avversario). La guardia ha un segreto, e il ladro cerca di indovinarlo. Per dimostrare che la guardia è sicura, non diciamo solo "è brava". Creiamo una serie di "giochi" o scenari.

1. Il Gioco Reale: Il ladro cerca di violare il sistema effettivo.
2. Il Salto: Immaginiamo un gioco leggermente diverso che è quasi lo stesso ma più facile da analizzare. Dimostriamo che se il ladro può vincere nel Gioco Reale, può anche vincere in questo nuovo gioco, leggermente diverso.
3. La Catena: Continuiamo a saltare da un gioco all'altro, cambiando le regole solo un pochino ogni volta, finché non raggiungiamo un gioco finale che è ovviamente impossibile da vincere (come indovinare correttamente un lancio di moneta un milione di volte di seguito).

Se riusciamo a dimostrare che ogni singolo "salto" è sicuro, allora l'intera catena è sicura. Questo è chiamato una "dimostrazione di salto tra i giochi" (game-hopping proof).

Il problema è che gli esseri umani sono terribili nel fare questo in modo perfetto. Queste dimostrazioni sono lunghe, disordinate e piene di piccoli dettagli. Un singolo dettaglio trascurato può rendere l'intera dimostrazione errata e il sistema insicuro. Per anni, i ricercatori hanno cercato di costruire strumenti informatici speciali per controllare queste dimostrazioni, ma questi strumenti spesso parlano una lingua diversa dai matematici. Sono come un traduttore che parla solo "Sicurezza" ma non "Matematica", costringendo gli esperti a tradurre le loro idee avanti e indietro, il che è lento e soggetto a errori.

Entra in scena HOPSCOTCH: Il traduttore universale

Gli autori di questo documento, Stefan Dziembowski, Grzegor Fabiański, Daniele Micciancio e Rafał Stefański, hanno deciso di costruire un ponte. Hanno creato HOPSCOTCH, un framework all'interno di Lean 4, un popolare programma per computer utilizzato per verificare le dimostrazioni matematiche.

Ecco la magia di HOPSCOTCH:

• Nessun nuovo linguaggio: A differenza di altri strumenti che vi costringono a imparare un modo nuovo e ristretto di scrivere codice, HOPSCOTCH vi permette di scrivere dimostrazioni usando lo standard Lean. È come lasciare che uno chef cucini con i suoi coltelli preferiti invece di costringerlo a usare quelli di plastica.
• Dimostrazioni come oggetti: In HOPSCCTH, una dimostrazione non è solo un mucchio di testo. È un oggetto strutturato, come un modello Lego. Ogni "salto" nel gioco è un mattoncino Lego specifico. Potete incastrarli e il computer controlla se si incastrano perfettamente. Se provate a connettere due mattoncini che non corrispondono, il computer dice: "No, questo non funziona".
• Il trucco dell' "Astrazione": Una delle parti più difficili di queste dimostrazioni è mostrare che due sistemi diversi si comportano esattamente allo stesso modo. HOPSCOTCH usa un trucco intelligente chiamato "astrazione dello stato". Immaginate di avere due robot. Uno ha uno schema di cablaggio interno disordinato, l'altro ne ha uno ordinato. HOPSCOTCH vi permette di disegnare una mappa (una funzione di astrazione) che mostra come i fili disordinati corrispondano a quelli ordinati. Se la mappa è corretta, il computer sa che i robot sono identici nel comportamento, anche se appaiono diversi all'interno.

Cosa hanno effettivamente fatto e scoperto

Gli autori non si sono limitati a costruire lo strumento; lo hanno messo alla prova. Hanno usato HOPSCOTCH per verificare formalmente la sicurezza di quattro concetti crittografici principali:

1. Encrypt-then-MAC: Un metodo per rendere i messaggi sia segreti che immuni dalle manomissioni. Hanno dimostrato che se la cifratura sottostante e il "tagging" (MAC) sono sicuri, l'insieme è sicuro anche contro i hacker più intelligenti.
2. Cifratura ElGamal: Un famoso modo per inviare messaggi segreti utilizzando chiavi pubbliche. Hanno mostrato come dimostrare la sua sicurezza basandosi su un problema matematico difficile chiamato assunzione Decisional Diffie-Hellman (DDH).
3. Da Segretezza a Singola Utilizzo a IND-CPA: Hanno dimostrato che se un sistema è sicuro per un singolo messaggio, può essere reso sicuro per molti messaggi, un passaggio crucialo per costruire una cifratura robusta.
4. La Costruzione GGM: Questo è il punto cruciale. Il metodo GGM trasforma un semplice generatore di numeri casuali in una "funzione pseudocasuale" complessa (un generatore di numeri casuali finti che sembra reale). Le precedenti dimostrazioni informatiche potevano gestire solo versioni molto superficiali di questo (come un albero a 3 livelli). Gli autori hanno usato HOPSCOTCH per dimostrare la sicurezza di GGM per profondità non costante, il che significa che funziona per alberi di qualsiasi dimensione. Per quanto ne sappiamo, questa è la prima volta che un assistente alla dimostrazione general-purpose ha verificato con successo questa specifica e complessa costruzione.

Come l'hanno fatto (La meccanica del "Gioco")

Il documento spiega che HOPSCOTCH funziona scomponendo la dimostrazione in passaggi specifici, o "costruttori":

• Equivalenza Osservazionale: Dimostrare che due giochi sembrano uguali a un osservatore esterno.
• Riduzioni: Mostrare che se si può violare il Gioco A, si può violare il Gioco B.
• Sequenze di Ibridi: Concatenare molti piccoli passaggi.

Il framework include "tattiche" (aiutanti automatizzati) che cercano di risolvere questi passaggi per voi. Ad esempio, se dovete dimostrare che due oracle (i sistemi di gioco) sono uguali, il computer potrebbe cercare automaticamente una mappa di "astrazione dello stato". Se non riesce a trovarne una, lascia il passaggio affinché l'umano lo risolva, ma mantiene la struttura in modo che l'umano sappia esattamente dove si trova.

Gli autori hanno anche dimostrato un "teorema di correttezza computazionale". Questo è un modo elaborato per dire: "Se il computer dice che questa dimostrazione è valida, allora è effettivamente valida nel mondo reale". Hanno dimostrato che per ogni oggetto di dimostrazione creato da HOPSCOTCH, è possibile calcolare matematicamente esattamente quanto "vantaggio" avrebbe un hacker, basandosi sulle assunzioni utilizzate nella dimostrazione. Ciò garantisce che il computer non stia solo giocando con se stesso; sta fornendo una garanzia di sicurezza reale e concreta.

Conclusione

Il documento conclude che HOPSCOTCH riesce a colmare il divario tra la comodità degli strumenti specializzati per la sicurezza e la potenza degli assistenti matematici general-purpose. Permette ai crittografi di scrivere dimostrazioni più facili da leggere, più facili da controllare e meno soggette all'errore umano. Sebbene gli autori ammettano che il computer non controlli ancora se l' "hacker" stia eseguendo velocemente (un dettaglio tecnico chiamato tempo polinomiale), hanno gettato le basi per dimostrazioni di sicurezza completamente automatizzate e affidabili.

Suggeriscono anche il futuro: con questi oggetti di dimostrazione strutturati, potrebbe presto essere possibile usare l'IA per aiutare a scrivere queste dimostrazioni automaticamente, o estendere il sistema per gestire scenari ancora più complessi che coinvolgono "eventi negativi" e probabilità. Ma per ora, il traguardo principale è chiaro: hanno costruito un modo affidabile, flessibile e potente per permettere ai computer di aiutarci a dimostrare che i nostri segreti digitali sono al sicuro.