Google DeepMind afirma que usó AlphaProof Code para comprobar matemáticamente propiedades de seguridad clave en libsignal, la implementación de referencia del protocolo de mensajería Signal. El trabajo llevó cuatro semanas. Según DeepMind, equipos de expertos han tardado años en realizar verificaciones similares.
El sistema combinó investigadores humanos con agentes de IA. Los investigadores y la IA ayudaron a convertir los objetivos de seguridad de Signal en especificaciones matemáticas, que luego revisaron personas. Después, agentes basados en Gemini Carbon generaron unos 6,5 millones de líneas de código de prueba en Lean. Lean es un lenguaje de programación cuyo verificador puede comprobar si una demostración matemática sigue sus reglas. Los agentes señalaron cerca del uno por ciento del código para que lo revisaran personas.
¿Qué abarcó la prueba?
Los investigadores comprobaron el código máquina compilado del protocolo de enlace postcuántico PQXDH de libsignal y de Triple Ratchet. Demostraron propiedades específicas, entre ellas el secreto hacia adelante, la autenticación y la protección tras el compromiso de un dispositivo. El artículo de investigación señala que el código se compiló a partir de Rust sin modificar, con un compilador estándar, y luego se comprobó como código máquina AArch64.
Esto va más allá de demostrar que un diseño abstracto es seguro: vincula garantías de seguridad especificadas con el código compilado. DeepMind lo considera la primera verificación formal, con este nivel de profundidad, de la implementación de un protocolo criptográfico ampliamente utilizado. El equipo también volvió a introducir dos errores que ya se habían corregido en una versión aislada del código; el sistema generó pruebas que demostraban que las versiones con errores no cumplían las propiedades de seguridad especificadas.
La prueba tiene límites
Esto no constituye una garantía matemática de que todos los componentes de Signal, o todas las aplicaciones que usan el protocolo, estén libres de problemas de seguridad. La prueba abarca propiedades seleccionadas de libsignal, no la aplicación entera. También depende de especificaciones aprobadas, del verificador de Lean y de contratos para rutinas criptográficas de bajo nivel. The Register señala que el resultado no demuestra el secreto computacional de los bytes de mensajes reales; el artículo de DeepMind describe pruebas tanto en modelos simbólicos como computacionales, que dependen de supuestos sobre las primitivas criptográficas subyacentes.
DeepMind afirma que pondrá los materiales de verificación a disposición de otras personas. Espera aplicar el método a ámbitos como el firmware de dispositivos médicos y el software de redes eléctricas, pero señala que ampliarlo requerirá más investigación. El trabajo supone un paso hacia la comprobación de más código del mundo real, no demuestra que esos otros sistemas hayan sido verificados.
Por qué importa
Para quienes usan Signal, el trabajo añade una prueba verificada por máquina de propiedades de seguridad específicas en la implementación de su protocolo central. No demuestra que toda la aplicación esté libre de errores, y la prueba depende de supuestos sobre componentes criptográficos.
