Investigadores de Google DeepMind usaron IA agéntica para probar matemáticamente, o "verificar formalmente", varias de las garantías criptográficas clave del protocolo de Signal, informó Wired el 10 de noviembre. Es un resultado que importa tanto para esa criptografía, de uso masivo, como para la propia IA.
El trabajo se hizo en solo cuatro semanas, como una especie de prueba de concepto, y tiene dos lecturas. Es una validación independiente más de la criptografía que protege enormes cantidades de comunicaciones en plataformas como la app Signal, Google Messages y WhatsApp. Y muestra la capacidad de verificación formal de Google DeepMind con un nuevo marco de IA llamado AlphaProof Code.
La verificación formal asistida por IA está en auge, pero no está claro cuán práctica será para un uso amplio ni cuán eficaz puede ser para asegurar grandes volúmenes de código. Sus defensores la llaman desde hace años una especie de santo grial de la seguridad de software, porque usa matemáticas para comprobar que el software funciona como debe, es decir, que no tiene vulnerabilidades críticas.
¿Qué verificó exactamente DeepMind?
Antes de la IA, el proceso consumía muchísimo tiempo. Había que describir las propiedades del software que se querían probar, convertir esas descripciones en fórmulas y después desarrollar la prueba. La IA agéntica acorta bastante esa última etapa, y eso hizo posible un análisis como el de DeepMind sobre Signal. Aun así el alcance fue limitado. No verificó formalmente la app móvil completa de Signal, por ejemplo, y los investigadores insisten en que el resultado es solo un hito dentro de un proceso más largo.
"Estamos muy entusiasmados con este resultado, pero queda un largo camino antes de poder escalarlo a todo el software del mundo, y queremos hacerlo", dijo a Wired Swarat Chaudhuri, científico investigador de DeepMind.
El análisis no encontró vulnerabilidades nuevas en las partes del protocolo que revisó. Cuando los investigadores aplicaron AlphaProof Code a versiones antiguas de Signal con fallas conocidas y corregidas hace tiempo, la herramienta las identificó y mostró que en esos casos el protocolo no podía verificarse formalmente. DeepMind va a publicar la especificación y la prueba que desarrolló para Signal, de modo que sirvan a otros trabajos de verificación formal.
Por qué fue tan rápido
Los investigadores reconocen que partieron con ventaja gracias a trabajos de verificación formal que la Signal Foundation ya había hecho antes.
"Mientras la verificación formal previa se concentró en porciones más pequeñas del código, el enfoque de Google DeepMind permite una expansión significativa", dijo en un comunicado Ehren Kret, director de tecnología de Signal. "A medida que crecen las amenazas de seguridad impulsadas por IA, verificar rigurosamente la implementación del protocolo de Signal nos da todavía más confianza en las garantías de privacidad de nuestro código".
Para servicios críticos usados en contextos de alto riesgo, poder verificar formalmente cada base de código y cadenas de suministro de software completas sería un sueño. "Si ahora puedes verificar que estas implementaciones son correctas, puedes quedarte tranquilo", dijo Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind. "Imagina los bancos, imagina todas esas otras empresas que dependen de garantías y que se preocupan por los bugs, y que ahora podrían decir 'puedo probar estas propiedades'".
¿Cuánto cuesta y puede escalar?
La pregunta abierta en la industria es si la verificación formal automatizada con IA puede escalar de verdad, y si puede hacerlo a un costo razonable. DeepMind hizo el análisis de Signal gratis, como proyecto de investigación, y Google no quiso revelar cuánto costó. Tampoco quiso decir si planea lanzar un producto o servicio comercial de verificación formal.
Según los investigadores, parte de sus avances está en desarrollar un "proceso de colaboración entre humanos e IA", como lo llama Chaudhuri. En ese proceso los agentes aportan y se autocorrigen en casi todas las etapas, pero piden revisión humana en los momentos clave.
"No queremos este tipo de mundo vibe donde la IA genera los objetivos y la IA genera las pruebas y básicamente rinde exámenes que ella misma escribió", dijo Chaudhuri. "Hay un punto intermedio".
