E se vi dicessi che il codice che protegge i vostri messaggi privati non è solo ‘testato’, ma è stato dimostrato matematicamente per essere corretto?
Sì, avete letto bene. Non parlo di quel test pigro che facciamo noi prima di pushare su GitHub sperando che non esploda tutto in produzione. Parlo di verifica formale, il gold standard della sicurezza, roba che di solito richiede team di accademici chiusi in una stanza per anni a scrivere teoremi infiniti. Ma Google DeepMind ha deciso di scombinare le carte con AlphaProof Code.
Il succo della storia è questo: hanno usato un framework di agenti AI (basati su Gemini) per analizzare il protocollo crittografico di Signal. E non si sono fermati alla teoria o al design, che è dove di solito si fermano tutti i paper accademici che leggiamo. Sono andati a scavare nel codice compilato, quello che gira davvero sui vostri smartphone, per provare che le proprietà di sicurezza siano rispettate pezzetto per pezzetto.
Il processo è una figata tecnica che farebbe piangere di gioia un ingegnere del software: gli agenti AI hanno tradotto gli obiettivi di sicurezza in specifiche matematiche e hanno generato oltre sei milioni di righe di codice in Lean, un linguaggio per la verifica formale. Il bello? L’AI ha fatto il lavoro sporco e pesante, lasciando agli umani solo l’1% del codice da revisionare. In pratica, hanno ridotto un lavoro che richiederebbe anni a sole quattro settimane.
Per non farci scivolare nella trappola del ‘eh, ma è solo marketing’, hanno anche fatto una prova di fuoco: hanno reintrodotto intenzionalmente due bug reali (già risolti in passato) nel codice di Signal e il sistema è stato in grado di dichiarare immediatamente: «Ehi, questo codice è insicuro!». Niente allucinazioni da chatbot, solo pura logica matematica verificata da Lean.
Certo, c’è da essere un po’ cinici e chiedersi quanto potremo fidarci di sistemi così centralizzati, ma se l’obiettivo è rendere la difesa cibernetica veloce quanto gli attacchi, questa tecnologia è una lama affilatissima. Vedere l’AI che non scrive solo codice che ‘sembra’ funzionante, ma codice che ‘deve’ funzionare per legge matematica, è il salto di qualità che stavamo aspettando.
서서 (per i colleghi che masticano un po’ di coreano o seguono i paper): l’open source degli artefatti di verifica è disponibile. Quindi, se avete voglia di sporcarvi le mani e vedere come questi agenti hanno smontato Signal, andate a leggervi il paper. È il momento di smettere di sperare che i bug non ci trovino e iniziare a pretendere prove matematiche.
Source: AlphaProof Code