Investigadores de Google DeepMind aplicaron inteligencia artificial para demostrar con rigor matemático varias garantías esenciales del protocolo criptográfico que protege los mensajes en la aplicación Signal. Según información publicada por la revista especializada Wired, el proyecto se desarrolló en un lapso de cuatro semanas y no detectó fallos de seguridad inéditos en los segmentos analizados.
El trabajo empleó una herramienta novedosa de la compañía denominada AlphaProof Code. Los científicos la calificaron como una prueba de concepto, es decir, un ensayo orientado a validar la idea antes de expandirla a escalas mayores.
La metodología utilizada se conoce como verificación formal: en lugar de someter un programa a pruebas empíricas y confiar en que no falle, se traduce en lenguaje matemático lo que el programa debe cumplir y se demuestra que efectivamente lo cumple. Para los expertos en seguridad informática, según Wired, este enfoque representa una meta largamente perseguida.
Hasta ahora, describir esas propiedades y construir la demostración insumía mucho tiempo de especialistas humanos. Un agente de IA, un asistente que ejecuta tareas de forma autónoma, reduce sobre todo la segunda fase: la de elaborar la prueba formal.
Alcance del análisis y limitaciones
El estudio no abarcó la totalidad de la aplicación móvil de Signal, sino ciertas garantías de su protocolo. Los investigadores también probaron el sistema con versiones antiguas de Signal que contenían fallas conocidas y ya corregidas: el sistema las identificó y demostró que esas versiones no podían pasar la verificación.
DeepMind publicará la especificación y la demostración que desarrolló, para que otros equipos las utilicen en trabajos similares. Los investigadores reconocieron que partieron con ventaja, dado que la Signal Foundation ya había realizado 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 consta en 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 ello, según Wired, el resultado funciona como una validación independiente de la criptografía que protege una inmensa cantidad de comunicaciones.
Declaraciones de DeepMind y 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, que se centraban en partes más pequeñas. Señaló que verificar la implementación brinda 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, se mostró prudente respecto al alcance. “Falta mucho para poder escalar esto a todo el software del mundo, y queremos hacerlo”, declaró a Wired. También explicó que el método combina agentes y revisión humana en los momentos clave, y que el equipo no desea un esquema donde 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 incógnita que permanece abierta es el costo. DeepMind realizó el análisis de Signal sin cargo, como proyecto de investigación, y Google no quiso revelar cuánto costó. La compañía tampoco informó si planea lanzar un producto o servicio comercial de verificación formal.
Fuente: Infobae