Agentes de IA verifican el código de Signal

Un equipo de Google DeepMind asegura haber demostrado matemáticamente que el código que implementa el protocolo de Signal cumple sus principales garantías de seguridad. Es el protocolo que cifra las conversaciones de Signal y, en distintas versiones, las de WhatsApp y Google Messages. Para hacerlo ha usado agentes de inteligencia artificial que han generado, según la propia DeepMind, más de seis millones de líneas de pruebas en Lean, un lenguaje con el que un ordenador comprueba demostraciones matemáticas. SecurityWeek habla de unos 6,5 millones.

Es un uso de la IA que va a favor del cifrado y no en su contra. Antes de celebrarlo conviene leer qué se ha demostrado y qué se ha quedado fuera.

Qué se ha verificado

La verificación formal consiste en probar con matemáticas que un programa hace exactamente lo que se le exige. Hasta ahora, la mayoría de los análisis de protocolos criptográficos se quedaban en el diseño. DeepMind afirma que esta vez la prueba llega al código compilado. Según SecurityWeek, las garantías demostradas son tres:

• Secreto hacia adelante: si hoy se compromete una clave, los mensajes antiguos siguen protegidos.
• Seguridad tras un compromiso: el sistema recupera la protección después de que un dispositivo haya estado comprometido temporalmente.
• Autenticación: cada parte habla con quien cree hablar.

El trabajo se ha hecho sobre libsignal, la implementación de referencia del protocolo. El método, que DeepMind llama AlphaProof Code, reparte las tareas. Varias personas expertas, ayudadas por modelos de lenguaje (SecurityWeek menciona Gemini 4 Carbon y Claude Opus 5.5), tradujeron los objetivos de seguridad a especificaciones formales, y DeepMind afirma que cada una pasó revisión humana. Después, agentes basados en Carbon escribieron las pruebas. Lean rechaza automáticamente las que no son válidas, y los propios agentes marcaron para revisión humana alrededor del 1 % del código.

Para comprobar que el sistema distingue el código correcto del defectuoso, el equipo volvió a introducir dos fallos reales que ya estaban corregidos. En ambos casos obtuvo una prueba verificada por máquina de que esa versión era insegura. Según SecurityWeek, cinco personas completaron el trabajo en cuatro semanas.

Qué no garantiza

La propia documentación marca los límites, aunque el anuncio no los destaque:

• Los resultados se aplican a la compilación del código que hizo Google, ejecutada con un pequeño programa de línea de comandos, y «no a las aplicaciones de Signal», según recoge SecurityWeek. Que el núcleo esté verificado no dice nada del resto de la app ni del sistema en el que corre.
• En partes del análisis se dejaron fuera los canales laterales, es decir, las fugas de información por tiempos de ejecución, consumo y otros efectos físicos.
• Una prueba formal solo garantiza lo que dice la especificación. Si a una especificación le falta una propiedad o la formula mal, el código puede ser «correcto» y aun así inseguro. Por eso la revisión humana de esas especificaciones es la parte crítica.

Como punto a favor, DeepMind dice que publicará las especificaciones y las pruebas para que cualquiera pueda revisarlas. También agradece a Rolfe Schmidt, Michael Rosenberg y Ehren Kret, de Signal, sus comentarios sobre la metodología.

El escaparate de Gemini

El anuncio coincide con el negocio. El mismo día, según SecurityWeek, Google amplió el acceso a Gemini 4 Carbon a desarrolladores de pago, empresas y suscriptores de Google AI Ultra. Hasta el 30 de noviembre tiene un precio introductorio de 2 dólares por millón de tokens de entrada y 10 por millón de salida, y después se duplica. La versión especializada en ciberseguridad sigue reservada a los miembros de su programa Fairwind.

DeepMind presenta la verificación de Signal como la base para proteger desde el firmware de dispositivos médicos hasta la red eléctrica. Puede que lo sea, pero el material publicado por ahora solo respalda lo que se ha medido: un núcleo criptográfico concreto, compilado de una forma concreta y frente a unas propiedades concretas.

Fuentes: Google DeepMind, SecurityWeek