Google DeepMind ha presentato AlphaProof Code, un framework basato su agenti di intelligenza artificiale progettato per affrontare un compito che, nel software di sicurezza, resta fra i più difficili: dimostrare matematicamente che un programma possiede determinate proprietà e non soltanto verificarne il comportamento attraverso test ed esecuzioni controllate.
Il caso scelto per l’annuncio è tutt’altro che marginale. I ricercatori dichiarano di aver verificato proprietà di sicurezza fondamentali nel codice che implementa il protocollo Signal, la tecnologia crittografica usata dall’app Signal e da Google Messages. Il lavoro ha prodotto circa tre milioni di righe di prove nel linguaggio Lean, secondo la sintesi diffusa da DeepMind.
La distinzione importante è quella fra il protocollo descritto sulla carta e il software che lo realizza. Un protocollo può essere studiato e analizzato a livello teorico, ma l’implementazione concreta introduce strutture dati, condizioni, eccezioni, conversioni e scelte di programmazione che possono trasformarsi in punti deboli. Portare una verifica formale fino al codice è quindi un obiettivo molto più ambizioso che analizzare soltanto gli algoritmi crittografici astratti.
Dai test a una dimostrazione verificabile
Il testing tradizionale resta indispensabile, ma ha un limite strutturale: prova scenari selezionati. Anche una suite molto ampia può individuare errori rilevanti senza poter affermare di aver coperto ogni percorso possibile del programma. La verifica formale adotta un approccio differente. Si definiscono con precisione le proprietà che il sistema deve rispettare, si traduce il comportamento del codice in una forma adatta al ragionamento matematico e si costruisce una prova controllata da un sistema automatico.
In questo contesto Lean non è semplicemente un linguaggio di programmazione. È un proof assistant, cioè un ambiente capace di controllare passo per passo che una dimostrazione sia valida rispetto alle regole formali adottate. Le prove possono essere molto lunghe perché devono rendere espliciti passaggi che, in una spiegazione umana, verrebbero dati per scontati. La cifra di tre milioni di righe dà quindi un’indicazione della scala documentale e tecnica del progetto, non della quantità di codice del protocollo Signal.
La verifica formale non autorizza però una conclusione assoluta del tipo “Signal è inviolabile”. Una prova garantisce ciò che è stato espresso nelle specifiche e nel modello esaminato. Se un requisito non è stato formalizzato, se una componente esterna non rientra nell’analisi o se le ipotesi alla base del modello non corrispondono alla realtà operativa, quella garanzia non si estende automaticamente a tali aspetti. È una precisazione essenziale, soprattutto quando si parla di sistemi che proteggono comunicazioni private.
Il valore dell’annuncio sta proprio nell’avanzamento dichiarato sul piano dell’applicabilità. La verifica formale è da tempo considerata uno standard particolarmente solido per l’affidabilità del software, ma richiede competenze specialistiche, tempo e una disciplina di sviluppo difficile da adottare su larga scala. Per progetti complessi, il costo di tradurre codice e requisiti in oggetti verificabili può diventare proibitivo.
Il ruolo degli agenti: ampliare il lavoro degli specialisti
DeepMind descrive AlphaProof Code come un sistema agentico che combina competenza umana e agenti AI. L’idea non è ridurre l’intera verifica a una generazione automatica di testo o di codice: il risultato utile deve poter essere controllato da Lean. Questo introduce una differenza netta rispetto a un assistente di programmazione che suggerisce una soluzione plausibile. Nel caso delle prove formali, una proposta che non rispetta i vincoli del verificatore viene respinta.
Gli agenti possono essere impiegati per scomporre un obiettivo in sotto-problemi, cercare lemmi intermedi, tentare strategie di dimostrazione e correggere passaggi che non vengono accettati dal sistema. Il controllo finale resta legato al verificatore formale, mentre il contributo dell’AI riguarda l’esplorazione di uno spazio di possibilità che per un team umano può essere estremamente oneroso.
Questo è il punto che rende il progetto interessante anche oltre Signal. La sicurezza del software non dipende soltanto dalla qualità degli algoritmi: dipende dalla capacità di mantenere corretta l’implementazione mentre il codice cambia, viene ottimizzato, integrato con altre librerie e distribuito su piattaforme diverse. Se gli strumenti agentici riducono il costo della produzione e della manutenzione delle prove, la verifica formale può uscire più spesso dai contesti altamente specializzati in cui è stata finora confinata.
Il passaggio, tuttavia, non sarà immediato. Perché una prova sia significativa, gli ingegneri devono anzitutto decidere cosa dimostrare. Le proprietà di sicurezza vanno formulate con precisione, e questa fase richiede conoscenza del dominio, del modello delle minacce e delle assunzioni tecniche. Un agente può aiutare a costruire il percorso formale, ma non elimina la responsabilità di scegliere requisiti corretti e sufficientemente completi.
Perché il protocollo Signal è un banco di prova rilevante
Il protocollo Signal è impiegato per proteggere conversazioni private su servizi usati da un numero molto elevato di persone. Google DeepMind lo indica come la tecnologia alla base delle comunicazioni in Signal e Google Messages. L’adozione estesa fa sì che ogni miglioramento metodologico nella sua analisi interessi un caso reale, non un esercizio accademico costruito appositamente per un benchmark.
La crittografia delle comunicazioni è inoltre un settore in cui un dettaglio implementativo può avere conseguenze sproporzionate. Le funzioni da preservare includono, in termini generali, la riservatezza delle conversazioni e l’integrità dei meccanismi che regolano gli scambi tra partecipanti. DeepMind parla di “proprietà chiave” del codice del protocollo; senza ulteriori dettagli pubblici sulla portata precisa della verifica, è corretto attenersi a questa formulazione e non estendere il risultato a ogni parte dell’ecosistema delle app.
Per utenti e sviluppatori il messaggio più concreto è che la sicurezza può essere trattata anche come un problema di dimostrazione, oltre che di revisione, test e risposta agli incidenti. I diversi livelli non si sostituiscono. Una prova formale non rileva da sola una configurazione errata del dispositivo, un problema nell’interfaccia che induce l’utente a compiere un’azione rischiosa, una vulnerabilità in un componente non incluso nell’analisi o una compromissione dell’endpoint. Può però rendere più forte una specifica porzione della catena, purché l’ambito sia dichiarato e mantenuto nel tempo.
Le prossime verifiche saranno sulla ripetibilità
L’annuncio di DeepMind è una dichiarazione di ricerca dell’azienda e va letto anche con questa cornice. Il risultato sarà valutato dalla comunità tecnica attraverso il paper dedicato, i dettagli metodologici, l’esame delle assunzioni e, soprattutto, la possibilità di riprodurre o applicare l’approccio a basi di codice diverse. In un ambito come la verifica formale, la qualità non dipende soltanto dalla dimensione della prova, ma da quali proprietà sono state coperte, da come sono state modellate e da quanto il lavoro può essere aggiornato quando il software evolve.
Un altro elemento da osservare sarà il rapporto fra automazione e revisione umana. Un sistema capace di generare molte prove può accelerare il lavoro, ma aumenta anche l’esigenza di organizzare librerie, specifiche e processi di controllo comprensibili ai team che dovranno gestirli nel lungo periodo. La manutenzione è decisiva: una verifica che non riesce a seguire le modifiche del codice rischia di perdere rapidamente valore operativo.
AlphaProof Code non cambia quindi, da solo, le garanzie offerte oggi dalle applicazioni di messaggistica. Segnala però una direzione concreta: usare agenti AI non solo per scrivere software più velocemente, ma per produrre artefatti formali che un verificatore può controllare. Nel caso di Signal, DeepMind sostiene di aver portato questa impostazione sul codice di un protocollo crittografico utilizzato nel mondo reale. La rilevanza della notizia dipenderà ora dalla profondità tecnica del risultato e dalla sua capacità di diventare un metodo praticabile anche in altri software ad alta criticità.
