Google DeepMind usa agenti IA per verificare il codice macchina fondamentale di Signal

Google DeepMind ha presentato AlphaProof Code il 10 novembre 2026, impiegando team di agenti IA per produrre dimostrazioni Lean verificate automaticamente di proprietà di sicurezza definite per il codice compilato di libsignal di Signal. Il team di ricerca, composto da cinque persone, ha completato il lavoro di dimostrazione in quattro settimane e ha reso pubbliche le specifiche e gli artefatti di verifica affinché possano essere esaminati da soggetti esterni.

Il lavoro è andato oltre un modello astratto della progettazione del protocollo di Signal, arrivando alla sua implementazione compilata. I ricercatori hanno racchiuso i crate libsignal v0.105.4 e SPQR v1.6.0, senza modificarli, in un piccolo programma di supporto a riga di comando; poi hanno usato la versione standard di rustc per creare un eseguibile Linux AArch64 collegato staticamente. L’articolo tecnico descrive il risultato come le prime dimostrazioni di sicurezza a livello di protocollo per il codice non modificato di un’implementazione di protocollo crittografico ampiamente diffusa.

Come AlphaProof Code ha suddiviso il lavoro

Cinque ricercatori hanno dedicato quattro settimane al lavoro di dimostrazione, facendo operare gli agenti ininterrottamente sulle proprie workstation e portando avanti in parallelo dimostrazioni simboliche e computazionali. Secondo l’articolo, gli agenti hanno generato circa 6,5 milioni di righe di codice di dimostrazione Lean verificato automaticamente, basandosi su circa 26.000 righe di specifiche fidate e semantica AArch64.

Gli esseri umani hanno selezionato le proprietà, risolto ambiguità e compromessi in materia di sicurezza, esaminato le specifiche e mantenuto l’approvazione finale. Agenti basati su Gemini 4 Carbon e Claude Opus 5.5 hanno redatto e revisionato quelle specifiche, includendo una revisione condotta da una famiglia di modelli diversa. I team di agenti Gemini 4 Carbon hanno poi generato tutto il codice delle dimostrazioni; nessuno degli autori ha scritto codice di dimostrazione. Le campagne tipiche impiegavano da 40 a 80 agenti su una sola macchina per periodi da 24 a 72 ore; un orchestratore e i responsabili dei team coordinavano gli agenti addetti alle dimostrazioni, mentre i ruoli di architetto e integratore mantenevano la base di dimostrazioni condivisa.

Un sistema di controllo accettava una dimostrazione solo dopo che il kernel di Lean l’aveva verificata e un comparatore aveva confermato che corrispondeva alla specifica approvata dagli esseri umani e tenuta separata, comprese tutte le definizioni raggiungibili per transitività, utilizzando soltanto gli assiomi standard di Lean. Gli agenti potevano proporre modifiche minori quando le dimostrazioni rivelavano problemi nelle specifiche, ma qualsiasi modifica alle ipotesi fidate richiedeva l’approvazione umana o una regola impostata dall’utente, e veniva registrata con le relative motivazioni. Questo controllo affronta un rischio documentato delle dimostrazioni generate dagli agenti: una specifica può essere indebolita indirettamente intervenendo su una delle sue definizioni.

Copertura della sicurezza e test su vulnerabilità storiche

L’obiettivo della verifica era il codice delle sessioni uno-a-uno, che comprendeva l’handshake PQXDH e la messaggistica Triple Ratchet. I ricercatori riferiscono di aver prodotto due dimostrazioni indipendenti: dieci teoremi simbolici basati su ipotesi crittografiche idealizzate e una dimostrazione computazionale che pone un limite al vantaggio di un attaccante mediante ipotesi crittografiche e termini statistici. Le proprietà considerate includono la segretezza in avanti, che protegge i messaggi precedenti in caso di furto dello stato corrente; l’autenticazione; la sicurezza dopo la compromissione, che riguarda il ripristino della sicurezza dopo una compromissione; e la segretezza dell’handshake. La dimostrazione simbolica copre inoltre la segretezza dell’handshake anche in caso di una successiva violazione di Diffie–Hellman.

Per verificare se quelle specifiche fossero in grado di individuare errori reali, il team ha annullato le correzioni di due bug di libsignal già risolti, noti come stato debole e sottogruppo piccolo, e ha ricompilato i binari modificati. In entrambi i casi, ha prodotto dimostrazioni Lean del fallimento del teorema di sicurezza simbolica. Il repository pubblico per la verifica organizza separatamente i materiali computazionali, simbolici, relativi al binario condiviso e alla semantica AArch64, e documenta come ricostruire e verificare le dimostrazioni in modo indipendente.

Ehren Kret, direttore tecnico di Signal, ha affermato che il lavoro «ci dà ancora più fiducia nelle garanzie di privacy del nostro codice».

Limiti e prossimi passi

Le garanzie sono ben lontane dal certificare le applicazioni complete di Signal. Riguardano la versione di libsignal-cli dei ricercatori eseguita come processo appena avviato; la generazione delle chiavi non è stata verificata, la messaggistica di gruppo è stata rimandata a lavori futuri, mentre i canali laterali e lo stato multi-dispositivo non rientrano nello scenario considerato. Le primitive crittografiche di basso livello e alcune routine selezionate di output e di libreria sono rappresentate da contratti fidati; il risultato dipende quindi anche da tali contratti, dalle specifiche approvate, dal kernel di Lean, dalla semantica AArch64 e dalle ipotesi sulle primitive.

L’articolo afferma che nessuna delle due dimostrazioni prova la capacità di recupero post-quantistica che SPQR è progettato per aggiungere: il teorema computazionale riguarda gli attaccanti classici, mentre i teoremi simbolici sul ratchet consentono all’attaccante di scegliere le chiavi SPQR. Il modello computazionale limita inoltre diverse azioni dell’attaccante e diventa vacuo quando il numero di messaggi e di sessioni raggiunge dimensioni sufficientemente grandi. Questi limiti definiscono ciò di cui un revisore esterno deve fidarsi prima di considerare le dimostrazioni verificate automaticamente una garanzia di sicurezza per una particolare implementazione.

I prossimi passi indicati dai ricercatori sono rafforzare i teoremi, ridurre la base fidata verificando un maggior numero di routine richiamate tramite hook e collegando i contratti crittografici a implementazioni verificate, ed estendere la copertura alla messaggistica di gruppo, a Sealed Sender e ai protocolli lato server. L’obiettivo di verificare le nuove versioni di libsignal prima della distribuzione è un traguardo di ricerca, non una distribuzione annunciata.

Il significato immediato del risultato risiede nella divisione del lavoro che dimostra: gli agenti si sono occupati di costruire le dimostrazioni, mentre la garanzia continua a basarsi su specifiche esaminate da esseri umani e su ipotesi esplicite. Pubblicare le dimostrazioni e le procedure di verifica offre ai revisori esterni un modo per testare queste fondamenta, mentre i ricercatori lavorano per integrare il flusso di lavoro nello sviluppo continuo di libsignal.