Google usa l'AI per dimostrare quanto è sicuro il codice di Signal

Google ha utilizzato l’intelligenza artificiale per affrontare una delle sfide più complesse della sicurezza informatica: dimostrare matematicamente che il codice di un protocollo crittografico rispetta precise garanzie di sicurezza. Il risultato riguarda Signal, non tanto l’omonimo software di messaggistica istantanea quanto – nello specifico – la tecnologia di crittografia end-to-end alla base del suo funzionamento e di quello di app come WhatsApp e Google Messaggi.

Il 10 novembre 2026, Google DeepMind ha presentato AlphaProof Code, un sistema che combina agenti AI basati su Gemini, competenze umane e strumenti di dimostrazione matematica. I ricercatori sono riusciti a verificare importanti proprietà di sicurezza di libsignal, l’implementazione di riferimento del protocollo Signal, arrivando fino al codice macchina.

È un traguardo che, secondo Google, avrebbe richiesto anni di lavoro con gli strumenti tradizionali; il progetto ha invece completato le verifiche in appena 4 settimane.

Signal Protocol, pubblicato nel 2013, utilizza meccanismi crittografici progettati per impedire l’accesso alle conversazioni anche quando alcune chiavi di cifratura risultassero compromesse.

Già nel 2025, come avevamo spiegato su IlSoftware.it, Signal aveva introdotto SPQR, un meccanismo che aggiorna le chiavi crittografiche durante le conversazioni per resistere anche ai futuri attacchi quantistici.

Perché trovare vulnerabilità non equivale a dimostrare la sicurezza

Per comprendere la portata del risultato bisogna distinguere i metodi con cui normalmente si controlla la solidità di un software:

• I test funzionali verificano che un programma produca i risultati attesi con determinati input.
• Il fuzzing sottopone il codice a grandi quantità di dati imprevisti, malformati o generati automaticamente per provocare comportamenti anomali.
• Gli strumenti di vulnerability scanning cercano invece problemi noti, componenti vulnerabili o configurazioni rischiose.

Sono approcci utilissimi, ma nessuno dimostra che un programma rispetti una proprietà di sicurezza in tutti i casi previsti da un determinato modello.

La verifica formale affronta il problema da un altro punto di vista: descrive una proprietà attraverso formule matematiche e costruisce una dimostrazione della sua validità, partendo da ipotesi esplicite. Per esempio, si può dimostrare che un aggressore non riesca a ricostruire determinate chiavi crittografiche, anche conoscendo informazioni acquisite durante una compromissione.

Una dimostrazione riferita al progetto di un protocollo non garantisce però che il software lo implementi senza errori. Una gestione sbagliata della memoria, una transizione di stato imprevista o un problema introdotto durante la compilazione possono creare vulnerabilità che il modello astratto non contempla.

Come funziona AlphaProof Code: 6,5 milioni di righe di dimostrazioni

AlphaProof Code organizza il lavoro attraverso più agenti AI, ciascuno impegnato in attività specifiche. Gli esperti definiscono gli obiettivi di sicurezza e supervisionano la traduzione delle proprietà in specifiche matematiche. Gli agenti alimentati da Gemini Carbon sviluppano poi le dimostrazioni utilizzando Lean, un linguaggio e assistente alla dimostrazione di teoremi.

L’AI non stabilisce autonomamente che Signal sia sicuro: produce dimostrazioni che il verificatore di Lean controlla secondo regole formali. Una conclusione apparentemente convincente, ma priva dei passaggi matematici richiesti, non supera il controllo.

Secondo il documento tecnico pubblicato dai ricercatori, gli agenti hanno prodotto circa 6,5 milioni di righe di dimostrazioni Lean, basate su circa 26.000 righe di specifiche e definizioni considerate affidabili, comprese quelle che descrivono il comportamento dell’architettura AArch64.

La verifica riguarda proprietà crittografiche fondamentali, tra cui la forward secrecy, che protegge i messaggi precedenti a una compromissione delle chiavi, e la post-compromise security, che permette alla comunicazione di recuperare protezione dopo una compromissione temporanea, purché ricorrano le condizioni previste dal protocollo.

Signal è quindi matematicamente sicuro? Attenzione ai limiti

Ehren Kret, CTO di Signal, ha accolto positivamente il risultato condiviso da Google, sottolineando come l’impiego degli agenti AI consenta di ampliare notevolmente la verifica rispetto ai precedenti approcci, spesso limitati a porzioni più piccole del codice.

A onor del vero, Google non ha dimostrato l’assenza di qualsiasi vulnerabilità in Signal: le rassicurazioni riguardano proprietà definite con precisione, all’interno di ipotesi e scenari specifici.

Il materiale di verifica pubblicato da DeepMind chiarisce alcuni limiti: i risultati riguardano una particolare compilazione di libsignal utilizzata da riga di comando, non l’intera applicazione Signal per Android, iOS o desktop. Le dimostrazioni, quindi, non sostituiscono audit, fuzzing, test e aggiornamenti di sicurezza; offrono una forma di garanzia aggiuntiva, particolarmente preziosa per il codice crittografico più delicato.

Se l’AI dovesse contribuire a ridurre il costo della verifica formale, sarà possibile applicare controlli matematici approfonditi anche a componenti software oggi troppo complessi da analizzare manualmente: firmware, sistemi di autenticazione, librerie crittografiche e programmi impiegati nelle infrastrutture critiche.