Google DeepMind pubblica AlphaProof Code: gli agenti hanno dimostrato in Lean la sicurezza del codice compilato di Signal
Il 10 novembre Google DeepMind ha presentato in dettaglio AlphaProof Code, un sistema di agenti che ha prodotto circa 6,5 milioni di righe di dimostrazioni Lean sul codice macchina di libsignal, la libreria di riferimento del protocollo Signal. Le dimostrazioni coprono l'handshake post-quantistico PQXDH e il Triple Ratchet, con ipotesi e limiti dettagliati nel paper tecnico.
La dimostrazione era stata accennata in una riga durante il lancio di Gemini 4 Carbon; ora è documentata. Google DeepMind ha pubblicato il 10 novembre un post sul blog e un paper tecnico su AlphaProof Code, un sistema di agenti che ha dimostrato matematicamente le proprietà di sicurezza del codice di libsignal, la libreria di riferimento del protocollo Signal. Questo protocollo cifra anche, attraverso varie varianti, WhatsApp, Messenger e Google Messages.
Cosa è stato dimostrato
L’originalità risiede nel livello della dimostrazione. La maggior parte delle verifiche sui protocolli si ferma alla loro progettazione. In questo caso, i ricercatori hanno compilato libsignal con il compilatore Rust standard per processori AArch64 (Arm a 64 bit) su Linux, dimostrando poi che questo codice macchina rispetta le proprietà previste. Tali prove coprono l’handshake post-quantistico PQXDH e il Triple Ratchet: forward secrecy, autenticazione, sicurezza dopo la compromissione temporanea di un dispositivo e segretezza dell’handshake.
I numeri mostrano la scala dell’operazione: circa 6,5 milioni di righe di prove scritte in Lean, un linguaggio di dimostrazione il cui kernel verifica ogni singolo passaggio. Poggiano su circa 26.000 righe di specifiche e di descrizione del processore che devono, a loro volta, essere considerate affidabili. Il lavoro ha richiesto quattro settimane a un team di cinque persone. L’articolo ricorda che la verifica del microkernel seL4 aveva richiesto venti anni-persona, e quella del compilatore CompCert sei.
Come lavorano gli agenti
AlphaProof Code suddivide il lavoro come un team di ricerca. Gli esseri umani decidono cosa dimostrare e revisionano ogni specifica, redatta con l’aiuto di diversi modelli. Agenti basati su Gemini Carbon scrivono poi le dimostrazioni in modo autonomo. Un agente «guardiano» accetta una dimostrazione solo se Lean la convalida a fronte di una copia della specifica approvata: l’affidabilità del risultato non dipende quindi da quella degli agenti. Secondo Google DeepMind, gli agenti hanno successivamente revisionato il proprio lavoro e hanno segnalato solo circa l’1% del codice di prova per una verifica umana.
Per verificare che il sistema distingua il codice sicuro da quello difettoso, il team ha reintrodotto due bug reali, già corretti in precedenza, in una copia isolata di libsignal. In entrambi i casi, il sistema ha prodotto una prova verificata che la versione con i bug non era sicura. Il CTO di Signal, Ehren Kret, citato nel post, vi scorge un «grande passo avanti». Gli artefatti di verifica sono stati pubblicati come open source.
I limiti, messi nero su bianco
Il paper tecnico è preciso su ciò che non viene garantito. Le prove simboliche presuppongono una crittografia perfetta e non dicono nulla sulla segretezza computazionale dei byte. I limiti computazionali non valgono contro un avversario quantistico. La generazione delle chiavi non è verificata. La descrizione del processore copre 467 istruzioni e 31 chiamate di sistema, ma non modella i thread, i segnali né il dynamic linking. Infine, il risultato fa affidamento sul kernel di Lean, sulle primitive crittografiche e sui contratti di alcune routine richiamate dal programma.
La nostra lettura
La verifica formale ha sempre avuto un difetto: costa troppo per quasi tutti i software. AlphaProof Code dimostra che gli agenti possono produrre la maggior parte delle prove, a patto che gli esseri umani stabiliscano cosa dimostrare e Lean verifichi tutto il resto. Si tratta di un cambio di metodo più che di un exploit isolato: la fiducia passa dagli agenti, fallibili, a un verificatore meccanico. Tuttavia, il risultato riguarda un perimetro ben definito, un piccolo programma di test da riga di comando, un’architettura specifica e ipotesi crittografiche dichiarate. Il primato rivendicato e il costo computazionale effettivo rimangono da esaminare da parte di altri team, soprattutto perché Google DeepMind non specifica se lo strumento stesso sarà messo a disposizione di altri. Per le aziende sviluppatrici di software critico, la questione diventa concreta: chi scriverà e revisionerà le specifiche, che costituiscono ormai il principale lavoro umano?
Fonti
- Google DeepMind — Introducing AlphaProof Code: a breakthrough in verifying complex software at depth (10 novembre 2026) Fonte primaria
- Google DeepMind — AlphaProof Code: Verifying Signal's Security at the Machine-Code Level (paper tecnico e sviluppo Lean) Fonte primaria
- The Register — Google DeepMind melds humans and AI agents to vet Signal's secure messaging techniques Fonte secondaria
Una fonte primaria proviene direttamente dall'azienda, dal laboratorio o dall'ente interessato. Una fonte secondaria riporta l'informazione senza esserne l'autrice: la segnaliamo come tale. Un errore? Consulta la nostra politica di rettifica.
