La crittografia di Signal supera una prova IA da 6,5 milioni di righe

Il codice di crittografia di Signal può ora vantare qualcosa che quasi nessun software molto diffuso può dimostrare: una prova matematica che fa ciò che promette. Un gruppo di agenti IA ha passato al vaglio libsignal, la libreria su cui si basa il protocollo Signal, dimostrando che le chat individuali restano segrete, verificano l’identità dell’interlocutore e tornano a escludere un aggressore anche dopo il furto di una chiave. Non sono state individuate nuove vulnerabilità.

La portata del risultato va ben oltre gli utenti di Signal. Il protocollo è lo standard globale per la messaggistica con crittografia end-to-end, e le sue varianti proteggono le chat su WhatsApp, Messenger e Google Messages. Verificare a questo livello di dettaglio codice reale, già distribuito, era un’operazione così lenta che quasi nessuno ci provava: uno dei maggiori successi del settore, la verifica formale del kernel di un sistema operativo, aveva richiesto vent’anni-persona. Questo lavoro è durato quattro settimane.

Lo strumento, sviluppato da Google DeepMind, si chiama AlphaProof Code. Prima, esperti umani e modelli di IA hanno tradotto gli obiettivi di sicurezza di Signal in enunciati formali in Lean, un linguaggio di programmazione progettato per le dimostrazioni matematiche; una persona ha poi controllato ciascun enunciato. In seguito, gruppi da 40 a 80 agenti, basati su Gemini Carbon, hanno prodotto le dimostrazioni, lavorando per sessioni di 24-72 ore su una singola macchina. Il risultato è un corpus di circa 6,5 milioni di righe di Lean.

Non è necessario fidarsi di quelle milioni di righe. Il kernel di Lean controlla ogni passaggio e scarta qualsiasi dimostrazione non valida, perciò non importa quale modello l’abbia scritta né quante volte abbia sbagliato lungo il percorso. Ciò di cui ci si deve fidare è molto più limitato: circa 26.000 righe di specifiche e un modello di come un processore ARM esegue il codice.

Le dimostrazioni riguardano i componenti di Signal che proteggono una conversazione: l’handshake PQXDH, che avvia una chat, e il Triple Ratchet, che cambia la chiave a ogni messaggio, compreso il livello post-quantistico pensato per resistere ai futuri computer quantistici. In pratica, rubare le chiavi attualmente presenti su un telefono non permette di sbloccare i messaggi più vecchi, e il ladro perde nuovamente l’accesso quando i due interlocutori si scambiano nuove chiavi.

Per dimostrare che il sistema è in grado di distinguere il codice corretto da quello difettoso, i ricercatori hanno reintrodotto in libsignal due vecchi bug, già corretti. Il primo faceva sì che la libreria conservasse una copia di una chiave segreta che avrebbe dovuto eliminare. In entrambi i casi, AlphaProof Code ha prodotto una dimostrazione verificata dalla macchina del fatto che la versione difettosa non era sicura.

I limiti sono concreti. La dimostrazione riguarda solo le sessioni individuali e DeepMind indica la messaggistica di gruppo come possibile sviluppo futuro. Si applica alla versione 0.105.4 di libsignal, compilata con il compilatore Rust standard per ARM Linux all’interno di un piccolo programma di test, non alle app complete di Signal per iPhone, Android o desktop. Si presume che i componenti crittografici di basso livello siano sicuri, ma non lo si dimostra. Un errore nelle specifiche approvate da una persona indebolirebbe la garanzia; inoltre, WhatsApp e le altre app usano versioni proprie del protocollo, quindi il risultato non si estende automaticamente a loro. Google ha anche rifiutato di dire a Wired quanto sia costata l’analisi o se intenda offrirla come servizio a pagamento.

Signal ha accolto con favore il risultato. «Con la crescita delle minacce alla sicurezza basate sull’IA, verificare con rigore l’implementazione del protocollo Signal ci dà ancora più fiducia nelle garanzie di riservatezza del nostro codice», ha dichiarato in una nota Ehren Kret, direttore tecnico di Signal. Swarat Chaudhuri, ricercatore di DeepMind, ha usato toni più cauti e ha detto a Wired che «c’è ancora molta strada da fare» prima che il metodo possa estendersi «a tutto il software del mondo».

Per chi usa Signal non c’è nulla da installare né alcuna impostazione da modificare. La dimostrazione riguarda codice già presente nell’app.

DeepMind ha pubblicato il lavoro il 10 novembre, insieme a un articolo tecnico, e ha reso disponibili su GitHub le specifiche e le dimostrazioni come open source. L’azienda descrive il progetto su Signal come una tappa fondamentale verso una grande sfida di verifica formale lanciata ad aprile e indica i firmware dei dispositivi medici e i software delle reti elettriche tra i sistemi che vorrebbe verificare in futuro.

Chaudhuri ha anche precisato fin dove, a suo avviso, le macchine dovrebbero spingersi in questo lavoro. «Non vogliamo un mondo di questo tipo, tutto basato sulle vibe, in cui l’IA genera gli obiettivi e l’IA genera anche le dimostrazioni», ha detto a Wired. Sono ancora le persone a decidere che cosa significa essere sicuri; all’IA spetta soltanto dimostrarlo.

Tag: sicurezza informatica, Google DeepMind, AlphaProof Code, crittografia end-to-end, libsignal, Signal