Un team di cinque persone e l'intelligenza artificiale hanno dimostrato il codice di Signal in quattro settimane

Quattro settimane. Tanto è durato per un team di cinque persone di Google DeepMind, che ha lavorato con agenti di intelligenza artificiale, per produrre prove verificate automaticamente delle principali proprietà di sicurezza nel codice compilato della libreria di chat principale di Signal. Le prove si estendono per circa 6,5 milioni di righe. Precedenti iniziative di rilievo su altri sistemi hanno richiesto anni di lavoro specialistico e, di solito, la scrittura di codice per la verifica.

Il documento di ricerca, datato 10 novembre 2026, illustra il metodo e i suoi limiti. Il documento tecnico allegato riporta i dati in modo più dettagliato. Questo lavoro non costituisce una validazione dell'app Signal nel suo complesso, né di altre app che utilizzano un design simile. Si tratta piuttosto di una validazione di specifiche proprietà di libsignal, la libreria di riferimento, per le sessioni one-to-one, estese al codice macchina compilato che viene effettivamente eseguito.

Ciò che è stato dimostrato

libsignal è la libreria che implementa il design di crittografia di Signal. In parole semplici, questo design è concepito per mantenere un messaggio privato anche se la chiave viene rubata in un secondo momento e per ripristinare la sicurezza dopo che un dispositivo è stato temporaneamente compromesso. Questi due concetti sono generalmente noti come forward secrecy e post-compromise security.

Il team ha compilato la libreria non modificata — versione 0.105.4, più la relativa crate SPQR alla versione 1.6.0 — con il normale compilatore Rust, ottenendo un piccolo strumento da riga di comando eseguibile su Arm Linux a 64 bit. Le dimostrazioni riguardano questo eseguibile, non una sua riscrittura ottimizzata. La libreria verificata ha una dimensione di circa 560 KB, ovvero circa 140.000 istruzioni macchina.

Il documento descrive l'handshake PQXDH, ovvero il metodo con cui due persone avviano una sessione privata, includendo una fase post-quantistica pensata per resistere a un futuro computer quantistico, e il Triple Ratchet, che genera una nuova chiave per ogni messaggio. Nel modello “simbolico”, che considera la crittografia sottostante come ideale, il documento afferma inoltre che l'handshake garantisce la segretezza contro un eventuale attacco futuro da parte di un computer quantistico. Le chat di gruppo, il mittente sigillato e il protocollo lato server sono invece oggetto di studi futuri.

Come è stato svolto il lavoro

La verifica formale consiste nello scrivere un'affermazione matematica precisa su ciò che il codice deve fare, per poi dimostrare che il codice soddisfa tale affermazione. Anche una sola ipotesi mancante può indebolire il risultato, quindi è comunque necessario che qualcuno scelga cosa dimostrare e approvi tale affermazione.

L'articolo è esplicito riguardo alla separazione dei ruoli. Gli esseri umani hanno selezionato le proprietà, risolto le ambiguità e approvato la specifica. Gli agenti hanno poi scritto le dimostrazioni. Queste dimostrazioni vengono accettate solo se Lean, un sistema di verifica delle dimostrazioni, le conferma. L'affidabilità del risultato, scrivono gli autori, non dipende dall'affidabilità degli agenti di verifica, perché il nucleo di Lean controlla la logica.

Il post di ricerca afferma che gli agenti di dimostrazione erano basati su Gemini Carbon. Il lavoro di dimostrazione vero e proprio è stato svolto da cinque ricercatori in quattro settimane, ognuno dei quali eseguiva un agente sulla propria workstation. Si tratta di una campagna breve per gli standard del settore. L'articolo osserva che il microkernel seL4, un famoso sistema di verifica precedente, ha richiesto venti anni-uomo, e che il compilatore C CompCert ne ha richiesti sei. Entrambi questi codebase sono stati scritti pensando alla dimostrazione. libsignal no.

Vuoi che l'intelligenza artificiale ti faccia risparmiare ore a settimana? La nostra guida gratuita ti mostra come fare.Scarica la guida gratuita →

Le dimostrazioni stesse possono essere lunghe perché riguardano il codice macchina. Circa 6,5 milioni di righe sono costituite da dimostrazioni: 5,3 milioni riguardano il codice binario, più file separati per i due modelli di sicurezza. Un lettore che desidera fidarsi delle affermazioni principali deve comunque leggere le parti considerate attendibili: circa 18.000 righe di specifiche nel repository, più circa 8.000 righe del modello di codice macchina Arm e dei nomi dei simboli mappati sull'eseguibile. Le routine crittografiche di basso livello, due funzioni di output e alcune chiamate di libreria sono date per scontate, non dimostrate.

Un controllo contro i vecchi bug

Per verificare se le affermazioni fossero sufficientemente solide, il team ha reintrodotto due bug che i ricercatori avevano precedentemente scoperto in libsignal e che nel frattempo erano stati corretti. In entrambi i casi hanno dimostrato che il teorema di sicurezza simbolica non è valido per il binario contenente il bug. Si tratta di una verifica utile: una specifica che “risulta valida” anche su codice noto per essere difettoso sarebbe troppo debole.

Uno di questi bug memorizzava lo stato di una nuova sessione, inclusa una copia di un segreto, dopo che un messaggio pre-chiave era stato decifrato solo in una sessione precedente. L'altro accettava un handshake la cui chiave di base era stata alterata, creando una seconda sessione con lo stesso segreto condiviso.

Ciò che il risultato non dice

Gli autori sono scrupolosi e i limiti sono importanti. Le dimostrazioni non coprono ogni parte di Signal, ogni possibile attacco o le primitive crittografiche stesse. I canali laterali sono esclusi dall'ambito di applicazione. La dimostrazione computazionale, che cerca di limitare la probabilità di successo di un attaccante reale, non offre alcuna garanzia contro un avversario quantistico e il suo limite diventa inefficace per sessioni lunghe e multiple con molti round.

Il documento osserva che varianti dello stesso protocollo sono utilizzate in WhatsApp, Meta Messenger e Google Messages. Queste app non erano l'artefatto oggetto della dimostrazione. Una dimostrazione relativa a libsignal non si estende automaticamente a ogni prodotto che utilizza un linguaggio simile.

Ehren Kret, responsabile tecnologico di Signal, viene citato nel post di ricerca affermando che la verifica rigorosa dell'implementazione del protocollo “ci dà ancora più fiducia nelle garanzie di privacy del nostro codice”.

Le dimostrazioni e le specifiche sono pubblicate in un archivio pubblico.

Perché è importante

La maggior parte delle persone che inviano un messaggio privato non vede mai la libreria che lo crittografa. Un metodo in grado di verificare il codice compilato di tale libreria, in poche settimane anziché in anni-persona, rappresenta un cambiamento concreto nel modo in cui questo tipo di software può essere sottoposto a verifica. Non si tratta di una certificazione che Signal, o qualsiasi altra app di chat, sia priva di difetti. È una verifica automatica di proprietà specifiche di una libreria fondamentale, prodotta con una rapidità tale da consentire che in futuro vengano verificate anche altre parti critiche del codice.

La maggior parte dei prodotti di chat di uso comune non offre ancora tale prova, e alcuni strumenti popolari non crittografano affatto i messaggi end-to-end. Un precedente rapporto aveva trattato uno strumento di chat per consumatori che invia messaggi di testo senza tale protezione.