# DeepMind usa l’IA per verificare parti del protocollo Signal

> AlphaProof Code di Google DeepMind ha dimostrato alcune importanti garanzie di sicurezza di Signal in un progetto pilota durato quattro settimane.

Oossa · 2026-11-10 · https://oossa.com/it/deepmind-uses-ai-to-formally-verify-parts-of-signal-protocol

I ricercatori di Google DeepMind hanno dimostrato che un sistema di IA può provare matematicamente alcune importanti proprietà di sicurezza del protocollo di messaggistica Signal. Il team ha usato un nuovo framework, chiamato AlphaProof Code, per verificare formalmente diverse garanzie crittografiche. Il lavoro è durato circa quattro settimane ed è stato svolto come progetto di ricerca, non come prodotto commerciale. Nelle parti esaminate non sono stati individuati nuovi bug, mentre l’IA ha segnalato correttamente vulnerabilità precedenti, già corrette, quando è stata applicata a versioni più vecchie del protocollo.

La verifica formale consiste nell’usare la matematica per controllare che un software si comporti esattamente come previsto, senza lasciare spazio a vulnerabilità nascoste. In passato, questo processo richiedeva a esperti di redigere specifiche dettagliate, tradurle in formule e poi costruire la dimostrazione: un lavoro impegnativo che poteva durare mesi. Affidando gran parte del lavoro a un’IA agentica, cioè capace di fissare e perseguire sotto-obiettivi autonomamente, DeepMind ha ridotto i tempi a poche settimane. I ricercatori affermano che l’IA ha comunque avuto bisogno della supervisione umana in passaggi cruciali, ma che è stata in grado di proporre e correggere da sola le dimostrazioni.

Ehren Kret, CTO di Signal, ha osservato che le verifiche precedenti riguardavano solo piccoli frammenti di codice. L’approccio di DeepMind, ha detto, consente di «ampliare notevolmente» ciò che è possibile controllare. Il team renderà pubbliche le specifiche e la dimostrazione realizzate, così che altri gruppi possano proseguire il lavoro. Il risultato è promettente, ma DeepMind avverte che applicare il metodo ad app intere o a intere catene di fornitura del software resta una sfida; inoltre, non è stato reso noto il costo di queste verifiche basate sull’IA.

## Perché è importante

Se l’IA riuscirà a dimostrare in modo affidabile la sicurezza dei protocolli crittografici, gli utenti di Signal, Google Messages, WhatsApp e app simili potranno avere maggiori garanzie che i loro messaggi restino privati. Per le aziende che fanno affidamento sulle comunicazioni cifrate — banche, strutture sanitarie e giornalisti — questa tecnologia potrebbe un giorno fornire garanzie verificabili sul piano legale che il software non contenga difetti critici.

## I fatti

- Secondo i ricercatori, il progetto di DeepMind è durato circa quattro settimane.
- AlphaProof Code ha individuato correttamente vulnerabilità note e già corrette nelle versioni precedenti di Signal.
- Il CTO di Signal, Ehren Kret, ha affermato che il nuovo approccio basato sull’IA consente di «ampliare notevolmente» le verifiche rispetto ai tentativi precedenti.
- I ricercatori hanno reso pubbliche le specifiche e la dimostrazione realizzate, mettendole a disposizione di tutti.
- Google non ha comunicato il costo dell’analisi né annunciato un prodotto commerciale.

## Perché conta

Per le persone comuni, la notizia significa che la crittografia che protegge le loro chat è ora affiancata da un’ulteriore verifica matematica, riducendo il rischio di bug nascosti. Per le aziende che devono dimostrare la conformità alle norme sulla privacy, la verifica assistita dall’IA potrebbe diventare un nuovo modo per attestare la sicurezza senza lunghe revisioni manuali.

## Fonti e riferimenti

1. [A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure](https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/) – Wired, 2026-11-10

Ultimo aggiornamento: 2026-11-10