# DeepMind ha verificato con l’IA il codice crittografico di Signal

> AlphaProof Code ha verificato in quattro settimane alcune proprietà di sicurezza del codice compilato di Signal. La dimostrazione riguarda garanzie specifiche, non ogni componente di Signal.

Oossa · 2026-11-11 · https://oossa.com/it/deepmind-used-ai-to-verify-signal-s-cryptographic-code

Google DeepMind afferma di aver usato AlphaProof Code per verificare matematicamente alcune proprietà di sicurezza fondamentali di libsignal, l’implementazione di riferimento del protocollo di messaggistica Signal. Il lavoro è durato quattro settimane. DeepMind sostiene che in passato verifiche simili avrebbero richiesto anni di lavoro a gruppi di esperti.

Il sistema ha affiancato ricercatori umani ad agenti di IA. Ricercatori e IA hanno contribuito a tradurre gli obiettivi di sicurezza di Signal in specifiche matematiche, poi esaminate da persone. Gli agenti basati su Gemini Carbon hanno quindi generato circa 6.5 milioni di righe di codice di dimostrazione in Lean. Lean è un linguaggio di programmazione il cui verificatore può controllare se una dimostrazione matematica rispetta le regole. Gli agenti hanno segnalato circa l’uno per cento della base di codice per una revisione umana.

## Che cosa copre la dimostrazione?

I ricercatori hanno verificato il codice macchina compilato per l’handshake post-quantistico PQXDH di libsignal e per il Triple Ratchet. Hanno dimostrato proprietà specifiche, tra cui la segretezza in avanti, l’autenticazione e la protezione successiva alla compromissione di un dispositivo. Secondo il documento di ricerca, il codice è stato compilato da Rust non modificato con un compilatore standard e poi verificato come codice macchina AArch64.

Questo va oltre la dimostrazione della sicurezza di un progetto astratto: collega garanzie di sicurezza specificate al codice compilato. DeepMind la definisce la prima verifica formale, a questo livello di profondità, dell’implementazione di un protocollo crittografico ampiamente usato. Il gruppo ha anche reinserito in una versione isolata del codice due bug già corretti; il sistema ha prodotto dimostrazioni che mostravano come le versioni difettose non rispettassero le proprietà di sicurezza dichiarate.

## I limiti della dimostrazione

Non si tratta di una garanzia matematica che ogni componente di Signal, o ogni app che usa il protocollo, sia privo di problemi di sicurezza. La dimostrazione riguarda proprietà selezionate di libsignal, non l’intera app. Inoltre, si basa su specifiche approvate, sul verificatore di Lean e sui contratti relativi alle routine crittografiche di basso livello. The Register osserva che il risultato non dimostra la segretezza computazionale dei byte dei messaggi reali; il documento di DeepMind descrive dimostrazioni sia in modelli simbolici sia computazionali, che dipendono da ipotesi sulle primitive crittografiche sottostanti.

DeepMind afferma di rendere disponibili i materiali di verifica perché altri possano usarli. L’azienda spera di applicare questo approccio, tra gli altri ambiti, al firmware dei dispositivi medici e ai software delle reti elettriche, ma sottolinea che per estendere il metodo serviranno ulteriori ricerche. Il lavoro è un passo verso la verifica di una quantità maggiore di codice usato nel mondo reale, non la prova che questi altri sistemi siano stati verificati.

## I fatti

- Google DeepMind ha annunciato AlphaProof Code il November 10, 2026.
- Per il lavoro su libsignal, il sistema ha generato circa 6.5 milioni di righe di codice di dimostrazione in Lean.
- La verifica ha riguardato l’handshake PQXDH e il Triple Ratchet nel codice macchina AArch64 compilato.
- I ricercatori hanno reinserito due bug già corretti e il sistema ha dimostrato che le versioni interessate non rispettavano le proprietà di sicurezza specificate.

## Perché conta

Per chi usa Signal, il lavoro aggiunge una dimostrazione verificata da una macchina di specifiche proprietà di sicurezza nell’implementazione del protocollo di base. Non dimostra che l’intera app sia priva di bug e si basa su ipotesi relative ai componenti crittografici.

## Fonti e riferimenti

1. [Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years](https://the-decoder.com/google-deepminds-alphaproof-code-verified-signals-cryptographic-core-in-four-weeks-instead-of-years/) – The Decoder, 2026-11-11
2. [Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/) – Google DeepMind, 2026-11-10
3. [Google DeepMind](https://google-deepmind.github.io/code-verification/) – Google DeepMind
4. [The Register](https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/5308625) – The Register

Ultimo aggiornamento: 2026-11-11