Ing. Calogero Bono
Google DeepMind ha annunciato di aver dimostrato matematicamente alcune proprietà di sicurezza del codice reale del protocollo Signal, lo stesso usato da WhatsApp e Google Messages. L'ha fatto con AlphaProof Code, un sistema di agenti IA guidati da esperti umani. Secondo i ricercatori è la prima volta che l'implementazione di un protocollo cifrato così diffuso viene verificata formalmente, con o senza IA. Per chi costruisce software conta il metodo, oltre al risultato.
Qualche termine, prima di entrare nei fatti. Verifica formale è la dimostrazione matematica che un codice fa ciò che deve, senza errori. Lean è un linguaggio che controlla in automatico la correttezza di una dimostrazione. Protocollo sono le regole con cui due dispositivi si scambiano messaggi cifrati. Post-compromise security significa che i messaggi restano protetti anche dopo che un dispositivo è stato compromesso per un certo tempo. Agente IA è un modello che porta avanti un lavoro in più passaggi, quasi da solo.
Che cosa ha dimostrato DeepMind su Signal?
Stando al blog ufficiale di Google DeepMind, gli agenti hanno provato proprietà chiave del codice compilato, come la protezione dei messaggi prima e dopo una compromissione temporanea del dispositivo. Il livello è quello del codice che gira davvero sui dispositivi, non solo del progetto teorico.
Secondo The Register, sono stati verificati l'handshake post-quantistico PQXDH e il Triple Ratchet della libreria libsignal. Le proprietà coperte sono forward secrecy, autenticazione, post-compromise security e segretezza dell'handshake.
Come funziona AlphaProof Code?
È un framework con più modelli che divide il lavoro come un gruppo di ricerca. Esperti umani e modelli decidono che cosa dimostrare, poi un gruppo di agenti lo dimostra.
I ricercatori hanno tradotto gli obiettivi di sicurezza di Signal in specifiche matematiche, tutte riviste da persone. Gli agenti, basati su Gemini Carbon, hanno generato oltre sei milioni di righe di Lean (6,5 milioni secondo The Register). Poi hanno controllato la dimostrazione e segnalato solo l'1% del codice per una seconda lettura umana. Sul modello abbiamo scritto in Gemini 4 Carbon, Google punta su sicurezza informatica e lavori lunghi.
Perché quattro settimane contano?
Perché la verifica formale è sempre stata lenta. Secondo il paper citato da The Register, la verifica del microkernel seL4 richiese 20 anni-persona e lo sviluppo del compilatore CompCert sei anni. Qui il lavoro è durato quattro settimane, con un team di cinque persone e «parecchi token».
Il costo in risorse di calcolo non è stato reso noto, come ricorda 9to5Mac. Il lavoro si è appoggiato anche a verifiche precedenti della Signal Foundation, fatte senza IA.
Il sistema riconosce davvero il codice sbagliato?
Per saperlo, i ricercatori hanno reintrodotto due bug reali, già corretti, in una versione isolata del codice di Signal. In entrambi i casi il sistema ha prodotto una prova verificata dalla macchina che quella versione non era sicura.
È un test utile, perché una verifica che approva tutto non servirebbe a niente. Resta un controllo su due casi, non una garanzia sull'intero software.
Limiti da conoscere
La verifica riguarda il protocollo e non l'app Signal nel suo insieme, precisa 9to5Mac. DeepMind non ha verificato tutto il codice. Secondo The Register il risultato è teorico, perché assume una crittografia perfetta e non garantisce la segretezza computazionale dei byte. Il costo di calcolo non è dichiarato e Google ha detto a Wired che non è chiaro quanto l'approccio sia praticabile su larga scala. Non ci sono piani per un prodotto commerciale.
Cosa cambia per chi lavora con il digitale
Per ora non cambia nulla nelle tue app di messaggistica. Cambia l'orizzonte per chi scrive codice sensibile. Se integri la cifratura nei tuoi prodotti, il protocollo Signal per la crittografia end-to-end resta una base solida da capire, e ora ha una garanzia in più. Il lavoro dei ricercatori sposta l'attenzione dalla dimostrazione alla specifica, cioè a scrivere con precisione che cosa il codice deve garantire. È una competenza che vale anche per i gestionali e le app su misura. Il codice verrà pubblicato in open source, quindi potrai studiarlo.
Il nostro parere
Il risultato è serio, ma va letto con misura. Il valore sta nel metodo. Gli agenti fanno le dimostrazioni e gli umani decidono che cosa vale la pena dimostrare, e lì sta la parte difficile. I toni da «traguardo storico» sono prematuri, perché si parla di un protocollo, di quattro settimane di lavoro e di costi non dichiarati. Colpisce però che l'IA, spesso citata per le vulnerabilità che trova, venga usata per provare che il codice regge. Se i costi scenderanno, la verifica potrebbe uscire dai laboratori. Ne riparleremo quando vedremo il codice aperto.
Domande frequenti
Signal è ora garantito al cento per cento sicuro?
No. È stato verificato il nucleo crittografico del protocollo, non l'app intera. Il risultato inoltre assume una crittografia perfetta.
Anche WhatsApp è coinvolto?
Indirettamente sì. WhatsApp e Google Messages usano lo stesso protocollo di cifratura, quindi la verifica riguarda la base che condividono.
Quanto è durata la verifica?
Quattro settimane, secondo DeepMind. Un lavoro simile richiede storicamente anni a team di esperti. Il team era di cinque persone.
Che cos'è Lean?
È un linguaggio che controlla in automatico le dimostrazioni matematiche. Gli agenti hanno generato milioni di righe di Lean, e solo l'1% è stato riletto da persone.
Posso usare AlphaProof Code?
Non come prodotto. DeepMind non ha annunciato piani commerciali, ma i ricercatori rendono open source il loro codice per aiutare altri progetti di verifica formale.
Cosa guardare dopo Signal, dalla specifica al codice aperto
La prova ora è sul tavolo. Nei prossimi mesi si capirà se il metodo esce dal caso singolo.
- Controlla quando DeepMind pubblica il codice open source e quali requisiti di calcolo dichiara.
- Segui se altri protocolli o librerie ottengono verifiche simili, magari con costi diversi.
- Allena il tuo team a scrivere requisiti di sicurezza precisi, perché la specifica sarà il collo di bottiglia.
