Google DeepMind ha presentato AlphaProof Code, un sistema di agenti di intelligenza artificiale che, con la guida di ricercatori umani, ha dimostrato in forma matematica alcune proprietà di sicurezza chiave del codice compilato di libsignal, l’implementazione di riferimento del protocollo Signal. Il lavoro è durato quattro settimane, un compito che, secondo l’azienda, storicamente richiede anni a un team di esperti.
Nella pagina ufficiale DeepMind descrive il protocollo Signal come la tecnologia che protegge miliardi di conversazioni private in app come Signal e Google Messages. Nel documento tecnico precisa che varianti dello stesso protocollo sono in uso anche su WhatsApp e Messenger di Meta. La verifica riguarda libsignal, non le applicazioni complete e non il codice di WhatsApp.
Cosa è stato dimostrato
I ricercatori hanno dimostrato che il codice compilato soddisfa le proprietà di sicurezza fissate nelle specifiche, tra cui la protezione dei messaggi prima e dopo la compromissione temporanea di un dispositivo, l’autenticazione e la segretezza dell’handshake. Il perimetro è la sessione uno a uno di libsignal versione 0.105.4, con l’handshake post-quantistico PQXDH e il Triple Ratchet, compilata in linguaggio macchina AArch64. Restano fuori, tra l’altro, la messaggistica di gruppo, la generazione delle chiavi, i canali laterali, lo stato su più dispositivi e le app per smartphone.
Come funziona AlphaProof Code
AlphaProof Code divide il lavoro come farebbe un gruppo di ricerca. Gli esperti, insieme a un insieme di modelli, traducono gli obiettivi di sicurezza di Signal in specifiche matematiche formali e rivedono ciascuna di esse. Poi agenti basati su Gemini Carbon producono le dimostrazioni, con oltre sei milioni di righe in Lean, un linguaggio che permette di verificare in modo meccanico la correttezza delle prove. Gli agenti hanno anche controllato il risultato e segnalato per un secondo sguardo umano circa l’uno per cento del codice; Lean verifica il resto in automatico.
DeepMind definisce questo il primo caso in cui un’intelligenza artificiale verifica in modo formale, a questa profondità, un protocollo crittografico ampiamente in uso, e il primo in cui l’implementazione di un protocollo di questo tipo viene verificata formalmente, con o senza AI. Per mettere alla prova il sistema, i ricercatori hanno reintrodotto due bug reali, già corretti, in una versione isolata del codice: in entrambi i casi AlphaProof Code ha prodotto una prova, controllata da Lean, che la versione difettosa non era sicura.
Il CTO di Signal, Ehren Kret, ha detto che l’approccio consente un’espansione significativa rispetto alle verifiche precedenti, concentrate su porzioni più piccole del codice, e che la verifica rigorosa dell’implementazione del protocollo dà maggiore fiducia nelle garanzie di privacy. DeepMind ha reso disponibili gli artefatti della verifica. Sul sito abbiamo già raccontato altri lavori di Google DeepMind, come Genie 4, e l’arrivo di Gemini 4 Carbon.
Fonti: Google DeepMind, Introducing AlphaProof Code, documento tecnico, WIRED, The Register
Aiutaci a crescere: lasciaci un like :)