Notizia · · Per tutti
Google DeepMind: agenti IA dimostrano in modo formale la sicurezza del codice di Signal
Il 10 novembre Google DeepMind ha presentato AlphaProof Code, un sistema di agenti che scrive dimostrazioni matematiche controllate dal programma Lean. Lo ha applicato al codice macchina compilato della libreria di Signal per le chat a due, dimostrando proprietà come la segretezza dei messaggi passati e l'autenticazione.
Fonte: Google DeepMind ↗
Perché conta
La verifica formale, cioè la prova matematica che un programma fa ciò che promette, richiede di solito molto lavoro specialistico. Qui, secondo The Register, cinque persone hanno ottenuto in circa quattro settimane 6,5 milioni di righe di dimostrazione controllate dalla macchina, partendo dal codice già compilato: così non serve fidarsi del compilatore.
I limiti sono dichiarati: restano fuori le chat di gruppo, l'uso su più dispositivi e alcuni scenari con computer quantistici. Specifiche e dimostrazioni sono pubbliche su GitHub, mentre gli agenti di DeepMind non risultano disponibili. Per chi sviluppa è un segnale: gli agenti iniziano a controllare il codice, non solo a scriverlo.
Commento della redazione di Radar IA