Google DeepMind usó IA para verificar con matemáticas garantías del cifrado de Signal, sin hallar vulnerabilidades nuevas en cuatro semanas de trabajo.
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 el reporte de Wired, el proyecto duró cuatro semanas y no encontró vulnerabilidades nuevas en las partes analizadas. Para el análisis se usó un sistema nuevo de la compañía llamado AlphaProof Code, que los investigadores 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 conoce como 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. Según Wired, esta es una meta largamente buscada por quienes trabajan en seguridad informática, porque describir esas propiedades y armar la demostración consumía mucho tiempo de especialistas. Un agente de IA, es decir, un asistente que ejecuta tareas por su cuenta, acorta sobre todo la construcción de la prueba.
El análisis no abarcó 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 del proyecto público Signal Shot, lanzado el 20 de abril de 2026 por la Beneficial AI Foundation, Signal y el grupo Lean FRO, cuyo 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. 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, y que verificar la implementación da «aún más confianza» en las garantías de privacidad del código. Swarat Chaudhuri, investigador de DeepMind, dijo a Wired: «Falta mucho para poder escalar esto a todo el software del mundo, y queremos hacerlo». Explicó que el método combina agentes y revisión humana en los momentos clave. Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind, planteó que bancos y otras empresas que dependen de la ausencia de errores podrían demostrar que pueden probar ciertas propiedades de su software.
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.
Foto: Photographer.JuliaMustard / Wikimedia Commons (CC BY-SA 4.0).