DeepMind dimostra la sicurezza della crittografia di Signal e WhatsApp
Il protocollo di Signal è da anni il metro di paragone della messaggistica cifrata. Adesso arriva una conferma di tipo diverso: un’analisi di Google DeepMind lo ha verificato formalmente. Non è un test andato meglio del previsto, è una dimostrazione matematica che le proprietà di sicurezza dichiarate valgono in tutte le condizioni previste dal modello.
La notizia arriva da 9to5Mac, che cita il lavoro raccontato da Wired. Il protocollo però non vive solo nell’app Signal: è alla base della cifratura end-to-end di WhatsApp e dei messaggi cifrati di Google Messages, quindi il risultato tocca centinaia di milioni di conversazioni, comprese quelle di chi Signal non l’ha mai installato.
Che cosa significa verificare formalmente un protocollo
La verifica formale è la pratica di dimostrare, con la matematica, che un algoritmo rispetta le promesse di sicurezza che dichiara. Non si cerca un errore specifico: si dimostra che, dentro un modello definito di attaccante, non esiste una sequenza di passaggi che rompa lo schema.
La differenza con il collaudo tradizionale è sostanziale. Un test cerca la falla e, quando non la trova, può solo dire che non ne ha trovate. Una dimostrazione dice che quella falla non può esistere, almeno nel perimetro considerato.
Cosa è stato verificato e cosa resta fuori
Il limite più importante va detto subito: la verifica riguarda il protocollo, non l’app Signal nella sua interezza. Il codice dell’app e la gestione delle chiavi sul dispositivo sono un altro capitolo.
C’è però un dettaglio che rafforza la fiducia: provando l’analisi su versioni vecchie di Signal con vulnerabilità già note, il sistema le ha individuate e le ha segnalate come non verificate. Uno strumento che promuove tutto non serve a nulla; questo boccia quando deve.
Perché conta per WhatsApp e Google Messages
WhatsApp usa il protocollo Signal per la cifratura end-to-end dal 2016 e lo ha integrato in ogni chat. Google Messages lo usa per i messaggi RCS tra utenti che hanno la funzione attiva. Sono implementazioni diverse dello stesso mattone crittografico, quindi se il protocollo regge, regge per tutti.
La sicurezza finale dipende però da come ogni app implementa il protocollo e gestisce le chiavi. La dimostrazione copre la parte matematica, non il codice di contorno.
Tip
Per controllare la cifratura di una chat WhatsApp apri la conversazione, tocca il nome del contatto e scegli Crittografia: compaiono 60 cifre da confrontare con l’altro telefono. In Google Messages il lucchetto accanto all’ora indica una chat cifrata. Se i codici non coincidono, la chat non è verificata e conviene fermarsi prima di mandare dati sensibili.
Quattro settimane di lavoro e un costo non dichiarato
L’analisi ha richiesto quattro settimane e non è stato reso noto quanto sia costata in risorse di calcolo. Google ha spiegato a Wired che usare l’AI per la verifica formale è promettente ma ancora molto esigente e che la scalabilità è il nodo aperto.
Swarat Chaudhuri, ricercatore DeepMind, ha messo le cose in prospettiva: il risultato entusiasma, ma la distanza da colmare prima di applicare il metodo a tutto il software del mondo è lunga.
Cosa cambia davvero per chi usa il telefono
Nell’immediato nulla: nessun aggiornamento e nessuna impostazione da attivare. Cambia il livello di fiducia in un pezzo di infrastruttura che nessuno vede e che tutti usano. Cambia anche l’idea di cosa può fare l’AI: qui un modello dimostra teoremi di sicurezza.
Se vuoi capire cosa protegge la cifratura sul telefono e dove finiscono i limiti, la nostra guida su come funziona la crittografia Android parte dalle basi. Sul fronte messaggistica, nella guida a foto e video modificabili prima dell’invio in Google Messages trovi le novità più recenti dell’app. E se il filone DeepMind ti interessa, il caso Genie 4 e i mondi generati con l’audio mostra un altro lato del laboratorio.
Domande frequenti
DeepMind ha trovato un modo per leggere i messaggi WhatsApp?
No. Il lavoro non attacca WhatsApp né Signal: dimostra che il protocollo di cifratura rispetta le sue proprietà di sicurezza. Nessuna chiave è stata recuperata e nessuna conversazione è stata decifrata.
La mia chat è più sicura da oggi?
Non è cambiato nulla nel software del tuo telefono. La differenza è nella garanzia teorica: il protocollo che protegge la chat ha una dimostrazione formale a supporto.
Che differenza c’è tra verifica formale e penetration test?
Il penetration test cerca falle concrete e mostra che il sistema resiste agli attacchi provati. La verifica formale dimostra che, nel modello considerato, non esistono attacchi efficaci. La seconda è più forte, ma vale solo dentro le assunzioni del modello.
Vale anche per Telegram?
Solo in parte. Telegram usa un protocollo proprio per le chat normali e le cosiddette chat “secure” sono un’altra cosa. La verifica riguarda lo schema Signal, quindi non si estende ai protocolli che Signal non sono.