Google DeepMind Utiliza IA para Verificar el Código Criptográfico de Signal

El 10 de noviembre de 2026, Google DeepMind presentó los resultados de un estudio en el que agentes de IA ayudaron a verificar matemáticamente los mecanismos de seguridad clave del protocolo criptográfico Signal. Para este trabajo, los científicos desarrollaron el sistema AlphaProof Code, que combina modelos de lenguaje grandes, herramientas de verificación formal y supervisión por parte de especialistas. Según los investigadores, lograron por primera vez vincular las pruebas de seguridad de un protocolo criptográfico ampliamente utilizado con el código máquina de su implementación no modificada.

El proyecto duró cuatro semanas y requirió la participación de cinco investigadores. Durante este tiempo, los agentes basados en Gemini 4 Carbon crearon aproximadamente 6.5 millones de líneas de pruebas en el lenguaje Lean, que fueron verificadas por el núcleo matemático de este sistema. Los resultados se publicaron junto con documentación técnica y código fuente para que otros especialistas pudieran estudiar y reproducir la verificación.

Qué mecanismos de seguridad de Signal fueron verificados por los investigadores

El enfoque principal del estudio fue la biblioteca libsignal, que implementa el protocolo criptográfico Signal. Este protocolo se utiliza para el cifrado de mensajes de extremo a extremo no solo en el mensajero homónimo, sino también en otros servicios de comunicación, incluidos WhatsApp y Google Messages. Los investigadores examinaron dos mecanismos importantes: PQXDH, responsable del intercambio seguro de claves durante el establecimiento de la conexión, y Triple Ratchet, que actualiza las claves criptográficas a medida que avanza la conversación.

La verificación cubrió varias propiedades de seguridad. Entre ellas estaban la confidencialidad y autenticidad de los mensajes, la protección de la correspondencia anterior en caso de compromiso posterior de la clave, y la capacidad de restaurar la seguridad de intercambios futuros después de ciertos tipos de compromiso. Los investigadores también analizaron propiedades de seguridad específicas del procedimiento de establecimiento de conexión, considerando amenazas potenciales cuánticas.

A diferencia de la verificación tradicional de un modelo matemático de un protocolo, DeepMind estudió directamente la implementación compilada. Para esto, los investigadores utilizaron la versión 0.105.4 de libsignal y examinaron el código ejecutable para la arquitectura AArch64 utilizada en procesadores Arm. Este enfoque permite verificar no solo el esquema criptográfico, sino también cómo su implementación de software se adhiere a las propiedades de seguridad especificadas.

Cómo AlphaProof Code utiliza IA para verificar programas

La verificación formal difiere de las pruebas regulares en que, en lugar de verificar escenarios individuales, los desarrolladores prueban matemáticamente el cumplimiento de ciertos requisitos. Por ejemplo, se puede formular una condición donde un participante no autorizado no debería acceder al contenido de un mensaje, y luego se verifica si esta condición se cumple en todos los casos proporcionados por el modelo.

En AlphaProof Code, este proceso comienza con la creación de una especificación formal: una descripción matemática precisa de las propiedades a verificar. Los agentes de IA ayudan a traducir los requisitos de seguridad en expresiones en el lenguaje Lean, pero las formulaciones finales son verificadas y aprobadas por humanos. Después de esto, otro grupo de agentes genera pruebas, que el sistema Lean verifica independientemente de cómo fueron obtenidas.

Durante el estudio, se prepararon aproximadamente 6.5 millones de líneas de pruebas verificadas por máquina. Se basaron en aproximadamente 26,000 líneas de especificaciones confiables y descripciones del funcionamiento de la arquitectura del procesador. El sistema también destacó áreas que requerían verificación humana adicional, permitiendo a los investigadores enfocarse en las suposiciones más críticas.

Para probar la capacidad de AlphaProof Code para detectar problemas reales, el equipo reintrodujo dos vulnerabilidades previamente corregidas en versiones separadas del código. En ambos casos, el sistema pudo demostrar matemáticamente la violación de las propiedades de seguridad especificadas. Este experimento mostró que la herramienta es capaz no solo de confirmar la corrección de una implementación, sino también de identificar ciertos errores.

¿Significa esto que Signal es completamente seguro?

A pesar de los resultados, el estudio no cubre todo el sistema Signal. Los investigadores verificaron una implementación específica del protocolo criptográfico para el intercambio de mensajes entre dos participantes, no todas las funciones de la aplicación móvil. Los chats grupales, características específicas de las operaciones de dispositivos y servidores, así como algunos tipos de ataques de software, estaban fuera del alcance de este trabajo.

Además, las pruebas matemáticas son válidas bajo ciertas suposiciones sobre la seguridad de los algoritmos criptográficos utilizados. Los investigadores aplicaron dos modelos: uno simbólico, donde las operaciones criptográficas se consideran en una forma idealizada, y uno computacional, teniendo en cuenta las capacidades de los atacantes bajo condiciones dadas. Sin embargo, la prueba computacional no se extiende a adversarios cuánticos, y algunas propiedades post-cuánticas de Triple Ratchet aún requieren verificación separada.

Los investigadores no encontraron nuevas vulnerabilidades en los componentes verificados de la implementación actual. Sin embargo, esto no descarta problemas en otras partes de la aplicación y no garantiza la seguridad del sistema en todas las circunstancias.

Por qué el estudio es importante para el desarrollo de software

Según Google DeepMind, AlphaProof Code podría reducir significativamente el trabajo requerido para la verificación formal de software complejo. Anteriormente, tales proyectos tomaban años de trabajo por parte de especialistas: por ejemplo, la verificación formal del microkernel del sistema operativo seL4 requirió aproximadamente 20 años-persona, y el desarrollo del compilador C verificado CompCert tomó seis años.

La parte más laboriosa del nuevo enfoque no fue la generación de pruebas, sino determinar qué propiedades del software necesitaban ser verificadas. La colaboración humano-IA aceleró la preparación de pruebas pero no eliminó la necesidad de evaluación experta de modelos matemáticos y sus limitaciones.

En el futuro, Google DeepMind planea aplicar métodos similares a otros sistemas de software complejos, incluidos el software bancario y la infraestructura crítica. Sin embargo, la posibilidad de escalar la tecnología a bases de código más grandes, el costo de los cálculos y la cantidad de supervisión humana necesaria siguen siendo preguntas abiertas.