AlphaProof Code: la seguretat de Signal, demostrada instrucció a instrucció

Una demostració matemàtica, no una bateria de proves

Google DeepMind va presentar el 10 de novembre AlphaProof Code, un marc de treball amb agents d'IA (AI agents) per a la verificació formal de programari. Segons la nota del laboratori, signada per Pushmeet Kohli i Swarat Chaudhuri, el va fer servir per demostrar propietats de seguretat clau del codi real del protocol de Signal.

Signal és l'aplicació de missatgeria xifrada que manté la Signal Technology Foundation, una fundació estatunidenca sense ànim de lucre creada el 2018, amb Brian Acton, cofundador de WhatsApp, al patronat.

Segons DeepMind, és la primera vegada que la implementació d'un protocol així es verifica formalment per qualsevol mètode, amb IA o sense. Segons el seu article tècnic, els treballs anteriors sobre Signal analitzaven models abstractes, versions reescrites o propietats més restringides.

Les persones trien què cal demostrar i els agents ho demostren

Segons DeepMind, les persones decideixen què cal demostrar i aproven les especificacions, i els agents d'IA (AI agents) fan les demostracions. Les especificacions, segons l'article tècnic, van sortir d'un treball d'anada i tornada amb agents basats en Gemini 4 Carbon, de Google, i Claude Opus 5.5, d'Anthropic.

Les demostracions les van escriure íntegrament equips d'agents amb Gemini 4 Carbon: segons l'article, cap autor no va escriure codi de les demostracions. Un agent «guardià» només acceptava una prova que el nucli de Lean hagués comprovat.

Segons DeepMind, els agents van marcar per a revisió humana només l'1 % del codi i la resta la va comprovar Lean. L'article compara l'esforç amb altres verificacions, amb una advertència: aquells sistemes es van escriure per ser verificats, i libsignal no.

La demostració arriba fins al codi màquina

Segons l'article tècnic, el que s'ha verificat és libsignal-cli, un executable per a Linux en processadors AArch64, l'arquitectura ARM de 64 bits, compilat amb el compilador estàndard de Rust a partir de libsignal v0.105.4 sense modificar.

Els teoremes s'enuncien sobre el codi màquina, de manera que no cal refiar-se del compilador: un error seu faria fallar la prova. Cobreixen PQXDH, un intercanvi inicial de claus amb criptografia postquàntica (PQC, post-quantum cryptography), i el Triple Ratchet, i demostren el secret cap endavant (forward secrecy), la seguretat després que es filtri una clau (post-compromise security) i la confidencialitat i l'autenticitat dels missatges.

Segons l'article, les aplicacions de Signal per a Android i iOS executen el mateix codi Rust, de manera que els teoremes es traslladen als mòbils sempre que la compilació, l'enllaçament i el sistema operatiu no alterin el comportament del protocol.

Dos errors antics, caçats de nou

Els investigadors van reintroduir en una còpia aïllada dos errors reals de libsignal ja corregits, que havien descobert Cheval, Jacomme i Richards. Segons DeepMind, en tots dos casos el sistema va produir una demostració, comprovada per Lean, que aquella versió era insegura.

Segons l'article tècnic, en un d'ells, quan es desxifrava un missatge amb una sessió arxivada, la sessió nova desava una còpia de la clau secreta signada; en l'altre, el receptor no comprovava la clau base de l'emissor. De passada, els autors diuen que han catalogat 15 buits o errors en una anàlisi acadèmica anterior d'una part del protocol.

El que la demostració no cobreix

Segons l'article tècnic, la prova simbòlica suposa una criptografia perfecta, les primitives criptogràfiques s'especifiquen per contracte i els canals laterals (side channels) queden fora. La part computacional no dona garanties davant d'un adversari quàntic.

L'escenari, a més, és més limitat que el real: un dispositiu per persona, claus d'identitat ja fixades i converses de només dues parts. Google, per la seva banda, fa servir una variant del protocol a Google Messages, i les demostracions les va escriure el seu propi model.

L'única veu externa és la de Signal, el codi de la qual surt aprovat. Segons la nota de DeepMind, Ehren Kret, director tècnic (CTO) de Signal, afirma que fer servir agents d'IA per traduir automàticament el codi real en teoremes vàlids de Lean «és un gran avenç». A 11 de novembre, Signal no havia publicat res pel seu compte sobre el treball.