AlphaProof Code di Google DeepMind verifica formalmente il protocollo crittografico di Signal

Google DeepMind afferma di aver raggiunto una pietra miliare nella sicurezza del software considerata da tempo una grande sfida: i suoi ricercatori hanno guidato agenti IA nella dimostrazione matematica delle proprietà di sicurezza chiave del codice reale alla base del protocollo di Signal, la tecnologia che protegge miliardi di conversazioni private in app come Signal e Google Messages, cifrando i messaggi end-to-end in modo che solo mittente e destinatario possano leggerli. L'annuncio è stato pubblicato sul blog di Google DeepMind da Pushmeet Kohli e Swarat Chaudhuri.

Il risultato è stato ottenuto con AlphaProof Code, un nuovo framework agentico per la verifica formale a una profondità senza precedenti che combina l'expertise umana con agenti IA. La verifica formale — la dimostrazione matematica che il codice funziona correttamente senza difetti — è il più alto standard di garanzia della sicurezza, ma è difficile e spesso onerosa in termini di lavoro. I test convenzionali campionano il comportamento di un programma; una dimostrazione formale esclude i difetti in ogni possibile esecuzione — un livello di garanzia così costoso da produrre che raramente ha raggiunto software ampiamente diffusi.

Secondo l'azienda, il lavoro segna la prima volta che l'IA viene utilizzata per verificare formalmente un protocollo crittografico ampiamente diffuso a questa profondità. È anche la prima volta che l'implementazione di un protocollo ampiamente diffuso di questo tipo viene verificata formalmente con qualsiasi metodo, con o senza IA.

Come Google DeepMind ha verificato Signal

AlphaProof Code è un framework agentico multi-LLM che suddivide il lavoro di verifica formale come farebbe un team di ricerca: gli esperti umani lavorano con l'IA per decidere cosa dimostrare, e un gruppo di agenti IA esegue le dimostrazioni.

In primo luogo, i ricercatori di Google DeepMind hanno collaborato con un mix di modelli per tradurre gli obiettivi di sicurezza di Signal in specifiche matematiche formali, con esperti umani che hanno rivisto ciascuna di esse. Gli agenti basati su Gemini Carbon hanno poi eseguito le dimostrazioni, generando oltre sei milioni di righe di Lean, un linguaggio informatico che dimostra matematicamente la correttezza del codice.

Gli agenti hanno poi verificato la dimostrazione ed evidenziato le aree che richiedevano un secondo esame da parte di un essere umano — appena l'uno percento della codebase, un risparmio di tempo che l'azienda definisce enorme. Poiché Lean controlla automaticamente il resto, gli esperti hanno potuto concentrare la loro revisione dove il giudizio umano conta di più.

Dimostrare la sicurezza fino al codice in esecuzione

I protocolli crittografici sono alla base di quasi tutte le comunicazioni digitali, dal banking online alla navigazione web, e un singolo difetto può esporre milioni di persone contemporaneamente. Per questo gli esperti le analizzano formalmente da decenni, anche se la maggior parte delle verifiche dei protocolli si ferma a livello di design.

Gli agenti di Google DeepMind sono andati oltre, dimostrando che il codice compilato soddisfa le proprietà di sicurezza chiave — come mantenere i messaggi protetti prima e dopo che un dispositivo venga temporaneamente compromesso, garanzie che i crittografi conoscono come forward secrecy e post-compromise security — fino al codice esatto in esecuzione sui dispositivi. Le vulnerabilità del mondo reale spesso si nascondono nel divario tra design e implementazione, e colmare quel divario rende queste dimostrazioni enormemente più complesse.

Anche a questo livello di complessità, il processo di verifica ha richiesto appena quattro settimane — un compito che storicamente richiede anni ai team di esperti, secondo l'azienda — stabilendo che il codice crittografico centrale di Signal garantisce le protezioni di sicurezza specificate dai ricercatori.

Per confermare che AlphaProof Code possa distinguere il codice corretto dal codice difettoso, il team ha reintrodotto due bug reali, già corretti in passato, in una versione isolata del codice di Signal. In entrambi i casi, il sistema ha prodotto una dimostrazione verificata da macchina secondo cui la versione difettosa non era sicura — un controllo importante, poiché un verificatore incapace di segnalare codice difettoso fornirebbe una falsa garanzia.

In AlphaProof Code, gli agenti IA aiutano gli utenti a scrivere una specifica e poi dimostrano autonomamente che l'implementazione la soddisfa. Ogni dimostrazione è controllata da Lean per verificare il lavoro degli agenti.

La risposta di Signal

"Mentre le precedenti verifiche formali si concentravano su porzioni più ridotte del codice, l'approccio di Google DeepMind consente un'espansione significativa", ha dichiarato Ehren Kret, Chief Technology Officer di Signal. "L'uso di agenti IA per tradurre codice attivo in teoremi Lean validi è una svolta importante. Man mano che crescono le minacce alla sicurezza guidate dall'IA, la verifica rigorosa dell'implementazione del protocollo di Signal ci dà una fiducia ancora maggiore nelle garanzie di privacy del nostro codice."

Il futuro della sicurezza

Google DeepMind sostiene che il superamento di questa storica sfida dimostra come l'IA possa portare una garanzia di sicurezza di livello eccellente ad aziende, governi e infrastrutture critiche, contribuendo a difendersi dalle minacce informatiche guidate da agenti. La verifica della crittografia centrale di Signal, afferma l'azienda, getta le basi per mettere in sicurezza altri sistemi vitali, dal firmware dei dispositivi medici al software delle reti elettriche.

Scalare queste tecniche richiede ricerca continua. Abbinate ad agenti di difesa automatizzati come CodeMender, la verifica formale può contribuire a contrastare la velocità e la scala delle moderne minacce informatiche e a creare software con prova matematica che le sue protezioni funzionano.

Google DeepMind sta rendendo open source i suoi artefatti di verifica formale per l'uso della comunità, disponibili su google-deepmind.github.io/code-verification. L'articolo tecnico completo è disponibile come PDF. Per la comunità della ricerca sulla sicurezza, quella pubblicazione offre un modo per esaminare direttamente le dimostrazioni verificate da macchina e la metodologia — e quanto la verifica a questa profondità si estenderà oltre Signal, nei sistemi medici, industriali e di infrastruttura citati dall'azienda, è l'evoluzione da seguire.

Riconoscimenti

La ricerca è stata sviluppata da Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton e Pushmeet Kohli.

Il team ha ringraziato Eric Wieser per l'aiuto nell'apertura del codice, Owen Jones per il supporto nella gestione del programma, e Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko e George Tsoukalas per le utili discussioni. I ricercatori hanno inoltre ringraziato Rolfe Schmidt, Michael Rosenberg ed Ehren Kret di Signal per il feedback sulla metodologia, oltre a Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis e Sundar Pichai per il loro sostegno al progetto.