La compañía desarrolló AlphaProof Code, un marco de IA capaz de demostrar matemáticamente algunas de las principales garantías criptográficas del protocolo. El proyecto demandó cuatro semanas y abre nuevas posibilidades para detectar vulnerabilidades en sistemas críticos.
Google DeepMind dio un nuevo paso en la aplicación de inteligencia artificial a la seguridad informática. Sus investigadores utilizaron un sistema de IA con capacidades de gestión de agentes para verificar formalmente varias de las principales garantías criptográficas del protocolo Signal, una tecnología de cifrado utilizada también en servicios como WhatsApp y Google Messages.
El trabajo, desarrollado en apenas cuatro semanas como una prueba de concepto, representa un avance tanto para la criptografía como para la inteligencia artificial. Por un lado, aporta una validación independiente adicional sobre los mecanismos que protegen las comunicaciones privadas. Por otro, demuestra que los agentes de IA pueden acelerar considerablemente un procedimiento técnico que hasta ahora requería grandes cantidades de trabajo especializado.
La herramienta utilizada por los investigadores es AlphaProof Code, un nuevo marco de inteligencia artificial desarrollado por Google DeepMind. Su objetivo es facilitar la verificación formal de software: un proceso que utiliza métodos matemáticos para demostrar que un programa cumple determinadas propiedades y funciona de acuerdo con lo previsto.
La importancia de esta tecnología radica en que permite comprobar rigurosamente aspectos de seguridad de un sistema, en lugar de depender exclusivamente de pruebas convencionales o revisiones realizadas por especialistas. Durante años, la verificación formal fue considerada una de las herramientas más prometedoras para reducir vulnerabilidades críticas, aunque su aplicación resultaba extremadamente laboriosa.
Antes de la llegada de la IA, los investigadores debían describir las propiedades del software que querían comprobar, traducir esas descripciones a fórmulas matemáticas y desarrollar las demostraciones correspondientes. La intervención de agentes inteligentes puede reducir significativamente el tiempo necesario para completar esas etapas.
Qué logró demostrar Google DeepMind con Signal
El análisis no encontró nuevas vulnerabilidades en las partes del protocolo Signal que fueron examinadas. Sin embargo, uno de los resultados más relevantes fue la capacidad de AlphaProof Code para trabajar con versiones anteriores del protocolo que contenían fallas de seguridad conocidas y corregidas tiempo atrás.
Al analizar esas implementaciones, el sistema identificó correctamente las vulnerabilidades y demostró que el protocolo no podía superar la verificación formal. Es decir, no solo permitió comprobar determinadas propiedades de una versión del sistema, sino que también pudo reconocer situaciones en las que esas garantías no se cumplían.
El alcance del trabajo, de todos modos, tiene límites importantes. Los investigadores no verificaron formalmente toda la aplicación móvil de Signal ni todos los componentes de su infraestructura. El proyecto se concentró en determinadas garantías criptográficas del protocolo.
Además, Google DeepMind pudo avanzar con rapidez gracias a trabajos anteriores de verificación formal realizados por la Signal Foundation. La compañía publicó la especificación y la demostración matemática desarrolladas durante la investigación para facilitar nuevas iniciativas en este campo.
Ehren Kret, director de tecnología de Signal, destacó la importancia del avance. “Si bien la verificación formal previa se centraba en porciones más pequeñas del código, el enfoque de Google DeepMind permite una expansión significativa”, afirmó en un comunicado.
El ejecutivo también vinculó el desarrollo con el crecimiento de las amenazas de seguridad impulsadas por inteligencia artificial. “La verificación rigurosa de la implementación del protocolo Signal nos brinda aún mayor confianza en las garantías de privacidad de nuestro código”, agregó.
El desafío de verificar todo el software
La ambición de Google DeepMind va mucho más allá de Signal. Swarat Chaudhuri, científico investigador de la compañía, reconoció que todavía existe un largo camino antes de que esta tecnología pueda aplicarse a una escala mucho mayor.
“Estamos muy entusiasmados con este resultado, pero aún queda mucho camino por recorrer antes de poder aplicarlo a todo el software del mundo, y queremos lograrlo”, declaró a WIRED.
Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind, planteó algunas de las posibles aplicaciones en sectores donde los errores informáticos pueden tener consecuencias especialmente graves.
“Si ahora se puede verificar la corrección de estas implementaciones, se puede estar tranquilo”, sostuvo. Y mencionó a los bancos y otras empresas que dependen de garantías técnicas para operar: “Imaginen a todas esas empresas que se preocupan por los errores y que ahora podrían decir: ‘Puedo demostrar estas propiedades’”.
Sin embargo, todavía hay una pregunta central para la industria tecnológica: si la verificación formal asistida por inteligencia artificial puede extenderse a grandes cantidades de software y hacerlo a un costo económicamente viable.
En este caso, Google DeepMind realizó el análisis de Signal de manera gratuita como parte de un proyecto de investigación. Google no reveló cuánto habría costado el trabajo ni confirmó si tiene previsto lanzar un producto o servicio comercial basado en esta tecnología.
Chaudhuri también explicó que uno de los avances más importantes fue desarrollar un proceso de colaboración entre personas y sistemas de inteligencia artificial. Los agentes pueden intervenir en distintas etapas, revisar sus propios resultados y corregirse, pero los investigadores mantienen instancias de supervisión humana.
“No queremos un mundo donde la IA genere los objetivos y las pruebas, y básicamente realice pruebas autoinformadas”, explicó. “Hay un punto intermedio”.
La experiencia con Signal muestra una posible dirección para la seguridad informática: utilizar inteligencia artificial no solamente para escribir código o detectar errores, sino también para producir demostraciones matemáticas sobre el comportamiento de los sistemas. El desafío ahora será trasladar ese resultado, todavía acotado, a infraestructuras mucho más grandes y complejas.
