I ricercatori di Google DeepMind hanno utilizzato un’IA agentica per dimostrare matematicamente diverse garanzie crittografiche chiave del protocollo Signal. Condotti in quattro settimane come progetto proof-of-concept, questi lavori si basano su un nuovo framework di IA chiamato AlphaProof Code.
- Google DeepMind usa un’IA agentica per dimostrare matematicamente le garanzie crittografiche del protocollo Signal.
- Il progetto, durato quattro settimane, si basa sul framework AlphaProof Code.
- Nelle parti esaminate non sono emerse nuove vulnerabilità, e lo strumento ha individuato falle note nelle vecchie versioni.
- L’analisi non copre l’intera app Signal, e la scalabilità della verifica formale a costi ragionevoli resta da dimostrare.
Il protocollo Signal garantisce la cifratura delle comunicazioni nell’app Signal, ma anche, secondo la fonte, in Google Messages e WhatsApp. Per l’articolo, questa dimostrazione costituisce una nuova validazione indipendente di questa crittografia, che protegge una quantità enorme di messaggi nel mondo. Illustra inoltre le capacità di verifica formale di Google DeepMind.
La verifica formale consiste nell’usare la matematica per controllare che un software funzioni come previsto, cioè che non presenti vulnerabilità critiche. I suoi sostenitori la considerano da tempo il Santo Graal della sicurezza software. Ma il suo utilizzo su larga scala rimane incerto, così come la sua efficacia di fronte a grandi quantità di codice.
Un’analisi mirata
Prima dell’era dell’IA, occorreva un tempo considerevole per descrivere le caratteristiche di un software, trasformare queste descrizioni in formule e poi elaborare la dimostrazione. Secondo la fonte, l’IA agentica può ridurre fortemente la durata di quest’ultima fase. La portata dell’analisi rimane tuttavia limitata: non ha, ad esempio, verificato formalmente l’intera applicazione mobile Signal.
Nelle parti del protocollo esaminate, i ricercatori non hanno trovato nuove vulnerabilità. Al contrario, quando hanno applicato AlphaProof Code a vecchie versioni di Signal contenenti falle note e corrette da tempo, lo strumento le ha correttamente identificate e ha mostrato che il protocollo non poteva essere verificato formalmente in quelle versioni. I ricercatori pubblicano la specifica e la dimostrazione elaborate per l’analisi del protocollo Signal, per facilitare altri lavori di verifica formale.
La rapidità del progetto è in parte dovuta a lavori precedenti della Signal Foundation in questo campo, come sottolineano i ricercatori di DeepMind. «Mentre la verifica formale precedente riguardava porzioni più ridotte del codice, l’approccio di Google DeepMind permette un’estensione significativa», dichiara Ehren Kret, direttore tecnico di Signal, in un comunicato. «Mentre le minacce alla sicurezza legate all’IA si moltiplicano, verificare rigorosamente l’implementazione del protocollo Signal ci dà una fiducia ancora maggiore nelle garanzie di riservatezza del nostro codice.»
Una questione di costo e di scala
Per i servizi critici utilizzati in contesti ad alto rischio, poter verificare formalmente ogni base di codice e l’intera catena di approvvigionamento software sarebbe, secondo Pushmeet Kohli, direttore scientifico di Google Cloud e vicepresidente della ricerca di DeepMind, un progresso significativo. «Se ora si può verificare la correttezza di queste implementazioni, si può stare tranquilli. Immaginate le banche, e tutte le altre aziende che si affidano a garanzie e che si preoccupano dei bug, poter ora affermare: « posso provare queste proprietà »», afferma.
Resta la questione, aperta per l’intero settore tecnologico, della capacità della verifica formale automatizzata dall’IA di scalare realmente, e a un costo ragionevole. DeepMind ha realizzato l’analisi di Signal gratuitamente, nell’ambito di un progetto di ricerca, e Google non ha voluto comunicarne il costo. L’azienda non ha nemmeno specificato se prevede di commercializzare un prodotto o un servizio di verifica formale.
I ricercatori ritengono che alcuni dei loro progressi cruciali riguardino un «processo di collaborazione umano-IA», secondo l’espressione di Swarat Chaudhuri, ricercatore scientifico di DeepMind. Questo processo permette agli agenti di contribuire e di correggersi a quasi ogni fase, pur sollecitando il parere e la validazione umani in momenti chiave. «Non vogliamo questo mondo dell’ambientazione, dove l’IA fissa gli obiettivi, dove l’IA produce le prove, e dove si superano i test che ha scritto lei stessa. Esiste una via di mezzo.»
