Signal: cosa ha realmente dimostrato l’IA sul suo codice

Google DeepMind afferma di aver usato AlphaProof Code per dimostrare alcune proprietà del codice compilato di libsignal. Il risultato mette in luce il potenziale dell’IA, ma anche i limiti precisi di una dimostrazione formale.

Per valutare se un software cifra correttamente i messaggi, non basta eseguire test e osservarne il comportamento in alcune situazioni. Occorre anche poter stabilire, attraverso un ragionamento verificabile, che determinate proprietà valgano in tutte le esecuzioni contemplate dal modello. Google DeepMind afferma di aver usato il proprio sistema AlphaProof Code per svolgere questo lavoro sul codice compilato del protocollo Signal, con agenti di IA e il verificatore di dimostrazioni Lean.

L’esperimento riguarda garanzie crittografiche precise, non la sicurezza assoluta dell’app Signal. Mostra soprattutto come l’IA possa partecipare a una verifica formale impegnativa, lasciando ai ricercatori importanti decisioni e affidando il controllo matematico finale a un software specializzato.

Dal modello crittografico al codice eseguito

Un protocollo di cifratura descrive le regole che permettono, per esempio, di proteggere uno scambio e autenticare gli interlocutori. Ma una progettazione corretta non basta: il programma che la implementa può contenere un errore. La verifica formale mira a stabilire matematicamente che il codice rispetti proprietà definite in anticipo, sulla base di ipotesi anch’esse esplicite.

DeepMind afferma di aver lavorato sul codice compilato di libsignal, la libreria che implementa il protocollo Signal. Questo passaggio è importante: il team non si è fermato a una descrizione teorica del protocollo, ma ha cercato di collegare le garanzie di sicurezza al codice prodotto dopo la compilazione.

Il sistema, battezzato AlphaProof Code, suddivide il lavoro tra diversi modelli e agenti. Secondo la descrizione pubblicata da Google DeepMind, alcuni ricercatori hanno prima tradotto gli obiettivi di sicurezza in specifiche matematiche; poi agenti basati su Gemini hanno costruito dimostrazioni formali. Il post di DeepMind menziona oltre sei milioni di righe prodotte nel linguaggio Lean. Questo volume non significa che l’IA abbia scritto sei milioni di righe di software: si tratta degli artefatti usati per formalizzare e verificare le dimostrazioni.

Cosa verifica Lean e cosa decidono i ricercatori

Lean è un assistente alla dimostrazione. Controlla che una dimostrazione rispetti le regole logiche del sistema e dimostri effettivamente il risultato formulato. Da solo, però, non decide se le proprietà scelte corrispondano a tutte le aspettative di un utente, né se le ipotesi iniziali descrivano correttamente il mondo reale.

Questa distinzione è centrale. Secondo DeepMind, gli esperti hanno partecipato alla definizione di ciò che andava dimostrato e hanno revisionato le specifiche. Gli agenti hanno poi esplorato possibili percorsi dimostrativi, mentre Lean ne verificava la validità formale. Il sistema può quindi ridurre una parte del lavoro necessario a trovare una dimostrazione, ma l’ambito di quest’ultima resta una scelta umana.

Una dimostrazione formale non è dunque un audit universale. Se una proprietà non è inclusa nelle specifiche, la dimostrazione non la copre. Se una funzione crittografica è considerata sicura senza che la sua implementazione venga verificata, questa ipotesi rimane un anello esterno al risultato. La conclusione corretta è condizionale: il codice soddisfa le proprietà formalizzate, nel quadro definito e sulla base delle ipotesi adottate.

Quattro settimane, due bug reintrodotti

DeepMind annuncia che l’esperimento è durato quattro settimane. Per verificare se il metodo fosse in grado di distinguere il codice conforme da una versione difettosa, il team ha anche reintrodotto due bug noti, corretti in precedenza, in una versione isolata del codice. Secondo l’azienda, il sistema ha quindi prodotto dimostrazioni verificate automaticamente, mostrando che queste varianti non rispettavano più le garanzie esaminate.

Questo test è utile perché mette alla prova il metodo con errori concreti, invece di misurare soltanto la sua capacità di produrre una dimostrazione su una versione corretta. Ma non costituisce un tasso di rilevamento generalizzabile: due difetti reintrodotti non rappresentano tutte le categorie di vulnerabilità, né tutti i software, né tutti i modi in cui un sistema potrebbe fallire.

I confini della dimostrazione restano precisi

Le garanzie esaminate riguardano il nucleo crittografico e gli scambi individuali. L’ambito descritto esclude l’applicazione nel suo complesso, le conversazioni di gruppo e l’uso su più dispositivi. Inoltre, non si tratta di una verifica di WhatsApp o Google Messages, anche se questi servizi utilizzano elementi del protocollo Signal. Una libreria o un protocollo condiviso non rende identiche le applicazioni che li integrano, le loro versioni e le loro configurazioni.

La verifica non significa nemmeno che non restino vulnerabilità sconosciute. Riduce l’incertezza su proprietà definite e sul codice incluso nell’analisi. Altri componenti, le interfacce, i sistemi operativi, la gestione delle chiavi o le funzioni escluse dall’ambito possono sollevare questioni distinte.

Per gli utenti, il vantaggio immediato consiste quindi meno in una nuova impostazione che in un metodo di controllo potenzialmente capace di rendere più difficile contestare determinate garanzie o violarle inavvertitamente. Per i team che progettano software critici, la questione è capire se gli agenti possano ridurre il costo umano di dimostrazioni che finora richiedevano un notevole lavoro specialistico. DeepMind cita possibili applicazioni ad altri software, ma resta da dimostrare che questo approccio possa essere esteso a sistemi più ampi.

Le specifiche e le dimostrazioni pubblicate da DeepMind offrono ad altri specialisti gli strumenti per esaminare e riprodurre il lavoro. È questa possibilità di controllo, insieme a un ambito chiaramente definito, a consentire di valutare il contributo dell’IA: non una certificazione generale di «sicurezza», ma un aiuto per stabilire determinate proprietà del codice, con esseri umani che scelgono ciò che conta e un verificatore formale che controlla la dimostrazione.