Google DeepMind usó IA para verificar matemáticamente la seguridad del cifrado de Signal

Investigadores de Google DeepMind usaron inteligencia artificial para demostrar con matemáticas varias garantías clave del protocolo criptográfico de Signal, la tecnología que protege los mensajes de esa aplicación. Según informó Wired, el proyecto duró cuatro semanas y no encontró vulnerabilidades nuevas en las partes analizadas.

El trabajo usó un sistema nuevo de la compañía llamado AlphaProof Code. Los investigadores lo describen como una prueba de concepto, es decir, un ensayo para mostrar que la idea funciona antes de aplicarla a gran escala.

La técnica se llama verificación formal: en lugar de probar un programa con ejemplos y esperar que no falle, se escribe en lenguaje matemático lo que el programa debe cumplir y se demuestra que lo cumple. Para quienes trabajan en seguridad informática, según Wired, es una meta largamente buscada.

Hasta ahora, describir esas propiedades y armar la demostración consumía mucho tiempo de especialistas. Un agente de IA, un asistente que ejecuta tareas por su cuenta, acorta sobre todo la segunda parte, la de construir la prueba.

Qué se comprobó y qué quedó fuera

El análisis no incluyó toda la aplicación móvil de Signal, sino ciertas garantías de su protocolo. Los investigadores también probaron la herramienta con versiones antiguas de Signal que tenían fallas conocidas y ya corregidas: el sistema las detectó y mostró que esas versiones no podían verificarse.

DeepMind publicará la especificación y la demostración que desarrolló, para que otros equipos las usen en trabajos similares. Los investigadores reconocieron que partieron con ventaja, porque la Signal Foundation ya había hecho verificaciones formales sobre porciones más pequeñas del código.

Ese trabajo previo forma parte de un proyecto público llamado Signal Shot, lanzado el 20 de abril de 2026 por la Beneficial AI Foundation, Signal y el grupo Lean FRO, según el sitio del proyecto. Su objetivo es verificar el protocolo y la aplicación completa con el asistente de demostraciones Lean.

El protocolo de Signal también sirve de base al cifrado de WhatsApp y de Google Messages. Por eso, según Wired, el resultado funciona como una validación independiente de la criptografía que protege una enorme cantidad de comunicaciones.

Las voces de DeepMind y de Signal

Ehren Kret, director de tecnología de Signal, afirmó en un comunicado que el enfoque de DeepMind permite una expansión significativa frente a los trabajos anteriores, centrados en partes más pequeñas. Dijo que verificar la implementación da “aún más confianza” en las garantías de privacidad del código, en un contexto de amenazas de seguridad impulsadas por IA.

Swarat Chaudhuri, investigador de DeepMind, fue prudente con el alcance. “Falta mucho para poder escalar esto a todo el software del mundo, y queremos hacerlo”, dijo a Wired. También explicó que el método combina agentes y revisión humana en los momentos clave, y que el equipo no quiere un esquema en el que la IA genere las metas y las pruebas sin control.

Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind, planteó un posible uso: bancos y otras empresas que dependen de la ausencia de errores podrían decir que pueden probar ciertas propiedades de su software.

La duda que queda abierta es el costo. DeepMind hizo el análisis de Signal sin cargo, como proyecto de investigación, y Google no quiso revelar cuánto costó. La compañía tampoco dijo si planea lanzar un producto o servicio comercial de verificación formal.