L'IA di DeepMind dimostra che il codice di cifratura di Signal mantiene le sue garanzie

Google DeepMind afferma che i suoi agenti di IA hanno dimostrato matematicamente che il codice di cifratura di Signal per le chat individuali mantiene le sue principali promesse di sicurezza. Il lavoro, presentato il 10 novembre, ha usato un nuovo sistema chiamato AlphaProof Code e ha verificato il programma compilato stesso, cioè il codice che viene eseguito davvero. Secondo DeepMind, è la prima volta che l'implementazione di un protocollo crittografico così diffuso viene verificata formalmente con qualsiasi metodo, con o senza IA. Nelle parti esaminate non sono emerse nuove falle.

Che cosa è stato dimostrato

La verifica formale consiste nello scrivere una proprietà di sicurezza come enunciato matematico e dimostrare che il programma la rispetta sempre, invece di provarlo su esempi. Gran parte delle analisi di protocolli come Signal si ferma al progetto. DeepMind è scesa fino al codice macchina: il team ha preso libsignal nella versione 0.105.4 e la libreria spqr, le ha compilate per Linux su ARM a 64 bit con il compilatore Rust standard e ha ragionato sull'eseguibile ottenuto, si legge nella descrizione tecnica.

Prima i ricercatori, insieme a diversi modelli di IA, hanno tradotto gli obiettivi di sicurezza di Signal in specifiche formali, ognuna rivista da una persona. Poi agenti basati su Gemini Carbon hanno scritto le dimostrazioni in Lean, un linguaggio il cui verificatore controlla automaticamente ogni passaggio. Il risultato è di circa 6,5 milioni di righe. Gli agenti ne hanno segnalato circa l'1% per la revisione umana, e l'intero progetto ha richiesto quattro settimane. Tra i dieci teoremi dimostrati ci sono la forward secrecy, che protegge i vecchi messaggi se una chiave trapela in seguito, e la sicurezza post-compromissione, che ripristina la protezione dopo che un dispositivo è stato violato temporaneamente.

Per verificare che il sistema distingua il codice corretto da quello difettoso, il team ha reinserito due veri bug di Signal, corretti da tempo, in una copia isolata del codice. In entrambi i casi AlphaProof Code ha prodotto una dimostrazione verificata dalla macchina che la versione con il bug era insicura.

Cosa resta fuori dalla dimostrazione

La descrizione elenca i limiti in dettaglio. Le app mobili non sono state verificate direttamente, e gli autori si aspettano solo che i risultati valgano anche per loro se eseguono il codice del protocollo senza modifiche. Le chat di gruppo sono rimandate a lavori futuri. I canali laterali, come le fughe di informazioni tramite tempi di esecuzione o consumo energetico, sono esclusi, così come la generazione delle chiavi e l'uso su più dispositivi. Le dimostrazioni presuppongono inoltre che i mattoni crittografici di base siano solidi. Il direttore tecnico di Signal, Ehren Kret, ha detto che il lavoro «ci dà ancora più fiducia» nelle garanzie di privacy del codice.

Il blog di DeepMind cita Signal e Google Messages tra le app che usano questo protocollo. WhatsApp ha adottato il protocollo Signal anni fa, ma la dimostrazione riguarda il codice libsignal di Signal e non il software di WhatsApp, quindi su WhatsApp non dice nulla di nuovo. Il lavoro si è basato in parte su una precedente verifica formale di Signal fatta senza IA. Il metodo è anche costoso: Google ha detto a Wired che richiede molta potenza di calcolo, e il ricercatore Swarat Chaudhuri ha osservato che c'è ancora «molta strada da fare» prima di poterlo applicare a tutto il software del mondo, riporta 9to5Mac. DeepMind ha pubblicato le dimostrazioni su GitHub, così esperti esterni possono controllarle.