L’AI di Google DeepMind verifica con la matematica il codice di Signal

Ogni giorno mandi messaggi «cifrati end-to-end» e ti fidi che nessuno possa leggerli. Ma chi controlla che il codice mantenga davvero la promessa? Il 10 novembre Google DeepMind ha provato a rispondere con la matematica.

Il suo nuovo sistema si chiama AlphaProof Code. Ha esaminato il codice di cifratura di Signal e ha dimostrato che rispetta alcune proprietà di sicurezza fondamentali. È un passo interessante, ma con limiti precisi. Vediamoli insieme.

Test o dimostrazione: che differenza c’è

Di solito il software si controlla con i test. È come verificare un ponte facendoci passare cento camion. Se regge, bene, ma non sai cosa succede con il camion numero centouno.

Una dimostrazione invece è il calcolo che garantisce che il ponte regge qualsiasi carico fino a un certo peso. I ricercatori hanno fatto proprio questo: non si sono limitati a provare il codice, lo hanno dimostrato. Sempre entro certi presupposti, che vediamo più avanti.

L’oggetto del controllo è libsignal, la libreria open source che realizza il protocollo Signal, nella versione v0.105.4. Una libreria è un pacchetto di codice riusato da altri programmi. La verifica riguarda il codice macchina, cioè le istruzioni finali eseguite dai processori ARM a 64 bit, non solo il progetto sulla carta.

Come funziona AlphaProof Code

AlphaProof Code è un sistema di più agenti AI. Un agente è un programma che porta avanti un compito da solo, un passo dopo l’altro. Se vuoi capire meglio questa idea, trovi una guida nel nostro articolo sull’intelligenza artificiale agentica.

Il lavoro è diviso in modo chiaro. Gli esperti umani decidono cosa dimostrare e controllano le «regole» scritte in linguaggio formale. Poi gli agenti scrivono le dimostrazioni. Infine un programma chiamato Lean le verifica in modo meccanico.

Pensa a Lean come a un correttore pignolo. L’AI fa i compiti, Lean li corregge riga per riga e boccia anche un solo passaggio sbagliato. Per questo non conta se l’AI «si inventa» qualcosa: una dimostrazione sbagliata semplicemente non passa.

Secondo TNW, le specifiche sono state preparate e riviste da agenti basati su Gemini 4 Carbon e Claude Opus 5.5 di Anthropic, sotto controllo umano. Le dimostrazioni, invece, le hanno scritte squadre di agenti basati su Gemini 4 Carbon.

Cosa è stato dimostrato

Le parti verificate sono due. La prima è la «stretta di mano» iniziale tra due telefoni, chiamata PQXDH, pensata per resistere ai computer quantistici. La seconda è il Triple Ratchet, il meccanismo che rinnova le chiavi messaggio dopo messaggio.

Immagina di cambiare la serratura dopo ogni lettera. Se un ladro ruba una chiave oggi, non apre le lettere di ieri. E dopo un po’ non apre nemmeno quelle di domani. In termini tecnici: segretezza dei messaggi passati, autenticazione e recupero della sicurezza dopo una compromissione.

C’è stata anche una prova del nove. I ricercatori hanno reinserito due vecchi bug di libsignal, già corretti da Signal, in una copia isolata. In entrambi i casi il sistema ha dimostrato che la versione difettosa non era sicura. Come un metal detector che suona davanti all’oggetto nascosto per prova. Nelle parti esaminate non sono emersi difetti nuovi.

I numeri del lavoro

Ogni squadra contava di solito 40-80 agenti e lavorava per 24-72 ore su una singola macchina. In tutto sono nate circa 6,5 milioni di righe di dimostrazione in Lean. Secondo DeepMind, gli agenti hanno indicato le parti da far ricontrollare a una persona: circa l’1% del codice.

Secondo The Register il gruppo era di 5 persone e sono bastate 4 settimane. Per confronto, The Register ricorda che la verifica formale di seL4, il nucleo di un sistema operativo, aveva richiesto 20 anni-persona.

Il lavoro risponde alla sfida «Signal Shot», lanciata ad aprile 2026 da Signal, Beneficial AI Foundation e Lean FRO. Secondo il blog di DeepMind, Ehren Kret, CTO di Signal, ha definito «una svolta importante» l’uso di agenti AI per trasformare codice reale in teoremi verificabili.

I limiti da conoscere

Primo: è un rapporto tecnico pubblicato da Google DeepMind e non risulta ancora passato da una revisione esterna: va letto come un preprint. Le dimostrazioni però sono pubbliche, quindi chiunque può ricontrollarle. Finora non risultano commenti di crittografi indipendenti.

Poi ci sono i confini dichiarati dagli autori:

• vale solo per le chat uno a uno: i gruppi sono rimandati a lavori futuri e la generazione delle chiavi non è verificata;
• le garanzie riguardano la libreria compilata dai ricercatori, non le app installate sui telefoni;
• si dà per scontato che le funzioni crittografiche di base funzionino come previsto, per questo The Register parla di risultato «teorico»;
• restano fuori più dispositivi dello stesso utente, alcuni attacchi quantistici e certi aspetti del sistema operativo, come i thread.

E WhatsApp? Secondo TNW il protocollo Signal protegge anche WhatsApp, Messenger e Google Messages. Attenzione però: è stato verificato il codice di libsignal, non quello di queste app.

Infine, decidere cosa dimostrare resta un compito umano. Swarat Chaudhuri, tra gli autori, ha detto a The Register che la prossima frontiera non saranno le dimostrazioni ma le specifiche. A Wired, citato da TNW, ha ammesso che la strada per estendere il metodo a tutto il software è ancora lunga.

Perché ti riguarda? In futuro le aziende potrebbero chiedere ai fornitori di software critico, come banche e sanità, non solo «l’abbiamo testato», ma «l’abbiamo dimostrato». Per ora però è ricerca. Google ha reso pubbliche specifiche e dimostrazioni, ma secondo TNW non ha voluto dire se ne farà un prodotto commerciale.

Cosa puoi fare subito

• Non serve installare niente. Signal e le app che usano il suo protocollo funzionano come prima.
• Tieni aggiornate le app di messaggistica. Le correzioni di sicurezza arrivano proprio con gli aggiornamenti.
• Proteggi il telefono. La cifratura difende il messaggio durante il viaggio, ma non aiuta se qualcuno prende il tuo telefono sbloccato.
• Diffida dei titoli trionfali. Il risultato vale per le chat a due e con presupposti precisi, non per «tutto».
• Se sei curioso o sviluppatore, specifiche e dimostrazioni sono su GitHub con licenza Apache 2.0. Per ricontrollare tutto servono diverse ore di calcolo e un picco di circa 15-34 GB di RAM.

Fonti

• Introducing AlphaProof Code: a breakthrough in verifying complex software at depth – Google DeepMind Blog
• AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level – Google DeepMind
• Repository code-verification – GitHub
• Google DeepMind melds humans and AI agents to vet Signal’s secure messaging techniques – The Register
• Google DeepMind’s AI agents formally verify Signal’s encryption code – The Next Web
• Signal Protocol and Post-Quantum Ratchets – Signal Blog
• Signal Shot: The Platform Is Ready – Leonardo de Moura

Foto di copertina: Nino Barbieri, CC BY-SA 2.5, via Wikimedia Commons (rielaborata da RicercAttiva).