Google DeepMind ha annunciato un risultato di verifica formale per l'implementazione crittografica di produzione di Signal, sostenendo che l'IA può ora colmare un pericoloso divario tra la progettazione di un protocollo e il codice macchina che effettivamente viene eseguito sui dispositivi. L'azienda afferma che AlphaProof Code, utilizzando agenti basati su Gemini Carbon sotto revisione umana, ha dimostrato proprietà di sicurezza selezionate del codice principale in quattro settimane, un processo che, secondo l'azienda, storicamente avrebbe richiesto anni a team di esperti.¹

La tempistica è importante perché i protocolli crittografici proteggono tutto, dai messaggi privati alle transazioni bancarie, e le debolezze emergono spesso durante l'implementazione piuttosto che nella progettazione astratta. Nel suo annuncio, DeepMind ha dichiarato che gli agenti hanno generato oltre sei milioni di righe di codice di prova Lean, mentre esperti umani hanno fissato gli obiettivi e revisionato i risultati. Ha inoltre reintrodotto due vecchi bug di Signal già corretti; il sistema ha mostrato correttamente che entrambe le versioni modificate erano insicure.¹

Signal ha accolto il risultato come qualcosa di più di un esercizio di laboratorio. Il direttore tecnologico Ehren Kret ha affermato che l'approccio consente una “significativa espansione” oltre i precedenti sforzi di verifica, più limitati, e offre all'organizzazione una “fiducia ancora maggiore” nelle garanzie di privacy di Signal.² L'amministratore delegato di DeepMind Demis Hassabis ha rilanciato il traguardo su X, descrivendolo come una prova di proprietà di sicurezza fondamentali nel codice macchina alla base del protocollo di messaggistica di Signal.Demis Hassabis (demishassabis)³

Il CEO di Google Sundar Pichai ha sottolineato che il lavoro ha verificato il protocollo fino al codice compilato del dispositivo, dove le garanzie teoriche altrimenti potrebbero non resistere al contatto con il software reale.Sundar Pichai (sundarpichai)⁴

Ma il passo avanti non equivale a dichiarare invulnerabile Signal, o il software in generale. Le notizie sul progetto osservano che DeepMind non ha verificato formalmente l'intera app mobile di Signal e che la questione centrale è se la verifica assistita dall'IA possa essere estesa a vaste basi di codice a un costo sostenibile. Lo scienziato ricercatore Swarat Chaudhuri ha espresso chiaramente il limite: “c'è ancora molta strada da fare prima di riuscire a estendere questo approccio a tutto il software del mondo.”²

Per ora, la prova è una dimostrazione netta di ciò che la revisione della sicurezza assistita dall'IA può fare, non ancora la prova universale che ogni programma sia sicuro.