La IA de DeepMind verifica en un mes partes del código que protege Signal y WhatsApp
Google DeepMind asegura haber completado en cuatro semanas una tarea que hasta ahora podía exigir años de trabajo especializado: verificar matemáticamente partes clave de la implementación del protocolo de cifrado de Signal. Este sistema protege las conversaciones privadas de Signal y Google Messages, y también sirve de base para el cifrado de WhatsApp.
El resultado no significa que toda la aplicación de Signal haya sido revisada de forma exhaustiva ni que la inteligencia artificial pueda sustituir a los expertos en seguridad. Sin embargo, el proyecto representa un avance relevante en la verificación formal del software, una técnica diseñada para demostrar que un programa cumple unas propiedades concretas de seguridad.
Una garantía matemática para el cifrado
La verificación formal utiliza matemáticas y lógica para comprobar que el código se comporta como establecen sus especificaciones. A diferencia de las pruebas convencionales, que examinan distintos escenarios y buscan errores, este método intenta demostrar que determinadas propiedades se cumplen en todos los casos contemplados.
En los protocolos criptográficos, estas propiedades pueden incluir la protección de los mensajes frente a un atacante, la seguridad de las claves o la capacidad del sistema para recuperar sus garantías después de que un dispositivo haya sido comprometido temporalmente.
Hasta ahora, buena parte de los trabajos de verificación formal se centraba en el diseño teórico de los protocolos. DeepMind afirma que su sistema ha ido un paso más allá al analizar también la implementación real, es decir, el código que ejecutan los dispositivos y en el que pueden aparecer errores que no estaban presentes en el diseño original.
La compañía sostiene que es la primera vez que se verifica formalmente, mediante cualquier método, la implementación de un protocolo criptográfico tan extendido. Se trata de una afirmación de alcance limitado: el análisis cubre partes relevantes del código, pero no equivale a certificar toda la aplicación de mensajería.
Más de seis millones de líneas de pruebas
El proyecto se ha desarrollado con AlphaProof Code, un marco que combina varios modelos de inteligencia artificial con la supervisión de investigadores humanos. El sistema parte de los objetivos de seguridad del protocolo y los traduce a especificaciones formales, una descripción precisa de lo que el código debe garantizar.
Los expertos revisaron esas especificaciones antes de que los agentes de IA comenzaran a generar las demostraciones. Para ello utilizaron modelos basados en Gemini Carbon y el lenguaje Lean, una herramienta que permite a un ordenador comprobar automáticamente si una prueba matemática es válida.
El proceso produjo más de seis millones de líneas de código Lean. Después, los propios agentes revisaron el resultado y señalaron aproximadamente el 1% de la base analizada para una segunda comprobación humana. Esa revisión es especialmente importante porque una prueba puede estar correctamente construida y, aun así, demostrar una propiedad distinta de la que realmente interesa verificar.
Según DeepMind, el análisis cubrió garantías relacionadas con la confidencialidad de los mensajes antes y después de una intrusión temporal en un dispositivo. Este tipo de resistencia es fundamental en aplicaciones de mensajería segura, donde un atacante puede obtener acceso durante un periodo limitado y tratar de utilizarlo para acceder a conversaciones futuras.
El sistema también identificó código vulnerable
El análisis no detectó nuevas vulnerabilidades en las partes de Signal examinadas. Para comprobar si la herramienta sabía distinguir entre una implementación segura y otra defectuosa, los investigadores introdujeron de nuevo dos errores reales que ya habían sido corregidos en una versión aislada del código.
En ambos casos, el sistema generó una prueba verificada por máquina que demostraba que las versiones modificadas ya no cumplían las garantías de seguridad. Esta prueba de control es relevante porque muestra que el sistema no se limita a confirmar automáticamente que todo funciona, sino que puede señalar cuándo una modificación rompe una propiedad definida.
La supervisión humana sigue siendo imprescindible
Uno de los principales límites del enfoque está en la definición de los objetivos. Si la inteligencia artificial escribe tanto las especificaciones como las pruebas, podría acabar verificando un problema que ella misma ha formulado de manera incompleta.
Por este motivo, el equipo de DeepMind defiende un modelo intermedio en el que los investigadores humanos revisan qué se quiere demostrar y examinan las partes más delicadas del resultado. La máquina aporta velocidad y capacidad para explorar grandes cantidades de código, mientras que los expertos controlan el significado de las garantías.
Signal ya contaba con trabajos previos de verificación formal sobre fragmentos más pequeños de su código. La nueva investigación amplía el alcance de ese esfuerzo, aunque se apoya parcialmente en esa base anterior. La organización responsable de Signal considera que esta combinación permite reforzar la confianza en sus mecanismos de privacidad ante amenazas cada vez más sofisticadas.
Un método prometedor, pero todavía difícil de escalar
La gran incógnita es si este proceso puede aplicarse a sistemas mucho más amplios y a un coste asumible. DeepMind realizó el análisis como un proyecto de investigación y no ha detallado cuánto habría costado en condiciones comerciales ni si planea convertir la herramienta en un producto.
Verificar una aplicación completa implica analizar millones de componentes, dependencias externas, sistemas operativos y cambios constantes en el código. Además, cada nuevo objetivo de seguridad requiere especificaciones revisadas por especialistas, un recurso que sigue siendo escaso.
DeepMind prevé publicar los materiales de verificación para que la comunidad pueda examinarlos y reutilizarlos. A largo plazo, la misma tecnología podría aplicarse a sistemas críticos como el firmware de dispositivos médicos, el software industrial o las redes eléctricas.
El avance, por tanto, no convierte a la IA en una garantía automática de seguridad. Sí apunta a una nueva forma de trabajar: utilizar agentes capaces de generar y comprobar pruebas a gran escala, pero mantener a los humanos al frente de las decisiones sobre qué debe considerarse seguro.
