Google DeepMind afferma di aver usato AlphaProof Code per verificare matematicamente alcune proprietà di sicurezza fondamentali di libsignal, l’implementazione di riferimento del protocollo di messaggistica Signal. Il lavoro è durato quattro settimane. DeepMind sostiene che in passato verifiche simili avrebbero richiesto anni di lavoro a gruppi di esperti.
Il sistema ha affiancato ricercatori umani ad agenti di IA. Ricercatori e IA hanno contribuito a tradurre gli obiettivi di sicurezza di Signal in specifiche matematiche, poi esaminate da persone. Gli agenti basati su Gemini Carbon hanno quindi generato circa 6.5 milioni di righe di codice di dimostrazione in Lean. Lean è un linguaggio di programmazione il cui verificatore può controllare se una dimostrazione matematica rispetta le regole. Gli agenti hanno segnalato circa l’uno per cento della base di codice per una revisione umana.
Che cosa copre la dimostrazione?
I ricercatori hanno verificato il codice macchina compilato per l’handshake post-quantistico PQXDH di libsignal e per il Triple Ratchet. Hanno dimostrato proprietà specifiche, tra cui la segretezza in avanti, l’autenticazione e la protezione successiva alla compromissione di un dispositivo. Secondo il documento di ricerca, il codice è stato compilato da Rust non modificato con un compilatore standard e poi verificato come codice macchina AArch64.
Questo va oltre la dimostrazione della sicurezza di un progetto astratto: collega garanzie di sicurezza specificate al codice compilato. DeepMind la definisce la prima verifica formale, a questo livello di profondità, dell’implementazione di un protocollo crittografico ampiamente usato. Il gruppo ha anche reinserito in una versione isolata del codice due bug già corretti; il sistema ha prodotto dimostrazioni che mostravano come le versioni difettose non rispettassero le proprietà di sicurezza dichiarate.
I limiti della dimostrazione
Non si tratta di una garanzia matematica che ogni componente di Signal, o ogni app che usa il protocollo, sia privo di problemi di sicurezza. La dimostrazione riguarda proprietà selezionate di libsignal, non l’intera app. Inoltre, si basa su specifiche approvate, sul verificatore di Lean e sui contratti relativi alle routine crittografiche di basso livello. The Register osserva che il risultato non dimostra la segretezza computazionale dei byte dei messaggi reali; il documento di DeepMind descrive dimostrazioni sia in modelli simbolici sia computazionali, che dipendono da ipotesi sulle primitive crittografiche sottostanti.
DeepMind afferma di rendere disponibili i materiali di verifica perché altri possano usarli. L’azienda spera di applicare questo approccio, tra gli altri ambiti, al firmware dei dispositivi medici e ai software delle reti elettriche, ma sottolinea che per estendere il metodo serviranno ulteriori ricerche. Il lavoro è un passo verso la verifica di una quantità maggiore di codice usato nel mondo reale, non la prova che questi altri sistemi siano stati verificati.
Perché conta
Per chi usa Signal, il lavoro aggiunge una dimostrazione verificata da una macchina di specifiche proprietà di sicurezza nell’implementazione del protocollo di base. Non dimostra che l’intera app sia priva di bug e si basa su ipotesi relative ai componenti crittografici.
