Google DeepMind verifica il codice di Signal: 6,5 milioni di righe di prove matematiche con l’AI

📌 In sintesi

• Google DeepMind verifica formalmente parti fondamentali di Signal. AlphaProof Code produce 6,5 milioni di righe di dimostrazioni matematiche per controllare proprietà di sicurezza dell’implementazione libsignal.
• La verifica arriva fino al codice macchina. Gli agenti AI analizzano un eseguibile AArch64 derivato dal codice Rust originale, utilizzando Lean per controllare matematicamente le dimostrazioni.
• La ricerca non dimostra che Signal o WhatsApp siano invulnerabili. Le garanzie riguardano proprietà e scenari specifici, non la sicurezza completa delle applicazioni, dei dispositivi o delle chat di gruppo.

Google DeepMind annuncia un risultato significativo nella verifica della sicurezza informatica: un sistema di agenti AI ha dimostrato matematicamente alcune proprietà crittografiche del codice utilizzato dal protocollo Signal. La ricerca, pubblicata il 10 novembre 2026, introduce AlphaProof Code, una piattaforma che combina modelli Gemini, supervisione umana e il linguaggio di dimostrazione formale Lean. Il progetto ha prodotto circa 6,5 milioni di righe di prove matematiche in quattro settimane, arrivando a verificare proprietà dell’eseguibile compilato, anziché limitarsi alla descrizione teorica del protocollo. Il risultato interessa direttamente la sicurezza delle comunicazioni cifrate, ma non equivale alla certificazione integrale di Signal, WhatsApp o delle altre applicazioni che adottano varianti dello stesso sistema crittografico.

AlphaProof Code verifica Signal fino al codice macchina

La novità emerge dalla ricerca originale pubblicata da Google DeepMind e dal relativo documento tecnico sulla verifica di libsignal. Tradizionalmente, la verifica formale dei protocolli crittografici si concentra sui modelli matematici che ne descrivono il funzionamento. Dimostrare che un protocollo è sicuro in teoria non significa però che il programma effettivamente eseguito sui dispositivi rispetti tutte le proprietà previste.

AlphaProof Code cerca di colmare proprio questa distanza tra specifica e implementazione. I ricercatori utilizzano agenti AI per costruire specifiche formali, sottoposte all’approvazione degli esperti, e per produrre dimostrazioni relative a un eseguibile compilato per l’architettura AArch64. Il lavoro parte dal codice Rust non modificato di libsignal, nella versione 0.105.4, e considera il comportamento delle istruzioni macchina attraverso un modello formale del processore. Il vantaggio è sostanziale: la verifica non deve presumere che la compilazione conservi automaticamente tutte le proprietà del sorgente, perché il ragionamento raggiunge il codice eseguibile.

Gemini Carbon genera milioni di prove, Lean controlla il risultato

Il progetto impiega un’architettura multi-agente nella quale Gemini Carbon contribuisce alla generazione delle dimostrazioni. Il sistema divide il lavoro tra definizione delle proprietà da verificare, costruzione delle prove e controllo dei risultati. Lean rappresenta l’elemento decisivo per l’affidabilità del processo. Le conclusioni prodotte dagli agenti non vengono accettate perché formulate da un modello linguistico: devono superare il controllo del verificatore matematico. Una dimostrazione errata, incompleta o non corrispondente alla proprietà richiesta non viene automaticamente considerata valida. Nel progetto sono state prodotte circa 6,5 milioni di righe di prove, a fronte di circa 26.000 righe di specifiche e semantica AArch64 che costituiscono una parte fondamentale della base da esaminare e considerare affidabile. Cinque ricercatori hanno coordinato il lavoro nell’arco di quattro settimane. Questo non elimina il ruolo umano. La scelta delle proprietà da dimostrare, la definizione delle ipotesi e l’approvazione delle specifiche rimangono responsabilità degli esperti. L’intelligenza artificiale accelera la costruzione delle dimostrazioni, non decide autonomamente che cosa debba significare sicurezza.

PQXDH e Triple Ratchet: quali garanzie sono state dimostrate

La verifica riguarda componenti fondamentali del protocollo Signal, inclusi PQXDH, utilizzato nello scambio iniziale delle chiavi, e Triple Ratchet, il sistema che aggiorna continuamente i segreti crittografici durante le conversazioni.Le proprietà esaminate comprendono riservatezza e autenticità dei messaggi, forward secrecy e sicurezza dopo una compromissione temporanea. La forward secrecy protegge le comunicazioni precedenti anche quando una chiave corrente viene esposta; la sicurezza post-compromissione mira invece a ristabilire la protezione delle comunicazioni successive attraverso il rinnovo delle chiavi, nelle condizioni previste dal modello. Si tratta dell’evoluzione tecnica già affrontata negli approfondimenti dedicati all’introduzione di PQXDH in Signal e al protocollo SPQR per la crittografia post-quantistica. Per verificare l’efficacia del metodo, Google DeepMind ha anche reintrodotto due vulnerabilità precedentemente corrette in una versione isolata del codice. AlphaProof Code è riuscito a dimostrare matematicamente che quelle implementazioni non rispettavano le proprietà di sicurezza richieste.

Perché Signal e WhatsApp non diventano automaticamente invulnerabili

Il risultato è circoscritto e il documento scientifico ne dichiara esplicitamente i limiti. Le prove riguardano un eseguibile sperimentale basato su libsignal, non l’intero software distribuito agli utenti. Non coprono tutte le funzionalità delle applicazioni, le conversazioni di gruppo, gli scenari multidispositivo e ogni possibile attacco all’ambiente operativo. Esiste anche una distinzione importante sul versante post-quantistico: le prove simboliche includono determinate proprietà contro futuri avversari quantistici, mentre le garanzie computazionali pubblicate riguardano attaccanti classici. Il lavoro non dimostra integralmente tutti i meccanismi di recupero post-compromissione contro un avversario quantistico. Restano inoltre assunzioni relative alle primitive crittografiche e all’ambiente di esecuzione. Non viene dimostrata l’assenza di ogni possibile vulnerabilità, né eliminato il rischio che un aggressore comprometta direttamente il dispositivo o sottragga le credenziali dell’utente. La distinzione è concreta: le campagne di phishing contro Signal documentate dall’FBI e analizzate nei precedenti attacchi russi agli account dimostrano che un attaccante può impossessarsi delle comunicazioni senza violare il protocollo crittografico.

La verifica formale può cambiare la sicurezza del software

Il risultato più importante riguarda il processo di sviluppo del software. AlphaProof Code suggerisce che le verifiche formali, storicamente riservate a progetti con risorse eccezionali, possano diventare più accessibili grazie all’automazione delle prove. Il metodo potrebbe essere esteso a librerie crittografiche, firmware e componenti delle infrastrutture critiche. Google DeepMind ha pubblicato codice e materiali di verifica affinché la comunità scientifica possa esaminarli. La novità non è un’intelligenza artificiale che dichiara sicuro un programma, ma un sistema che produce prove controllabili matematicamente. È questa differenza a rendere AlphaProof Code un progresso concreto: riduce il costo della verifica senza sostituire la necessità di specifiche corrette, revisione indipendente e analisi delle minacce che restano fuori dal modello.