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.
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.
