Investigadores de Google DeepMind han utilizado una IA agentica para demostrar matemáticamente varias garantías criptográficas clave del protocolo Signal. Realizados en cuatro semanas como un proyecto de prueba de concepto, estos trabajos se basan en un nuevo marco de IA llamado AlphaProof Code.
- Google DeepMind usa IA agéntica para demostrar matemáticamente garantías criptográficas del protocolo Signal.
- No encuentra vulnerabilidades nuevas, pero detecta fallos antiguos en versiones previas de Signal.
- El análisis no cubre toda la aplicación Signal, y su coste sigue sin conocerse.
- Los investigadores defienden un proceso de colaboración humano-IA para la verificación formal.
El protocolo Signal asegura el cifrado de las comunicaciones de la aplicación Signal, pero también, según la fuente, de Google Messages y de WhatsApp. Para el artículo, esta demostración constituye una nueva validación independiente de esta criptografía, que protege una cantidad enorme de mensajes en el mundo. También ilustra las capacidades de verificación formal de Google DeepMind.
La verificación formal consiste en usar las matemáticas para controlar que un software funciona como se espera, es decir, que no contiene fallos críticos. Sus partidarios la consideran desde hace tiempo como el Grial de la seguridad del software. Pero su uso a gran escala sigue siendo incierto, al igual que su eficacia frente a grandes cantidades de código.
Un análisis dirigido
Antes de la era de la IA, se necesitaba un tiempo considerable para describir las características de un software, transformar estas descripciones en fórmulas y luego elaborar la prueba. Según la fuente, la IA agentica puede reducir fuertemente la duración de esta última etapa. El alcance del análisis sigue siendo, sin embargo, limitado: no ha verificado formalmente, por ejemplo, la totalidad de la aplicación móvil Signal.
En las partes del protocolo examinadas, los investigadores no encontraron ninguna nueva vulnerabilidad. En cambio, cuando aplicaron AlphaProof Code a versiones antiguas de Signal que contenían fallos conocidos y corregidos hace tiempo, la herramienta los identificó correctamente y mostró que el protocolo no podía ser verificado formalmente en esas versiones. Los investigadores publican la especificación y la prueba elaboradas para el análisis del protocolo Signal, para facilitar otros trabajos de verificación formal.
La rapidez del proyecto se debe en parte a trabajos anteriores de la Signal Foundation en este ámbito, como destacan los investigadores de DeepMind. «Mientras que la verificación formal anterior se centraba en porciones más reducidas del código, el enfoque de Google DeepMind permite una extensión significativa», declara Ehren Kret, director técnico de Signal, en un comunicado. «Mientras las amenazas de seguridad relacionadas con la IA se multiplican, verificar rigurosamente la implementación del protocolo Signal nos da una confianza aún mayor en las garantías de confidencialidad de nuestro código.»
Una cuestión de coste y escala
Para los servicios críticos utilizados en contextos de alto riesgo, poder verificar formalmente cada base de código y la totalidad de las cadenas de suministro de software sería, según Pushmeet Kohli, director científico de Google Cloud y vicepresidente de investigación en DeepMind, un avance mayor. «Si ahora se puede verificar la corrección de estas implementaciones, uno puede estar tranquilo. Imaginen a los bancos, y todas las demás empresas que dependen de garantías y que se preocupan por los errores, pudiendo ahora afirmar: « puedo probar estas propiedades »», afirma.
Queda la cuestión, abierta para todo el sector tecnológico, de la capacidad de la verificación formal automatizada por IA para escalar realmente, y a un coste razonable. DeepMind realizó el análisis de Signal de forma gratuita, como parte de un proyecto de investigación, y Google no quiso comunicar su coste. La empresa tampoco precisó si planea comercializar un producto o servicio de verificación formal.
Los investigadores estiman que algunos de sus avances cruciales se centran en un «proceso de colaboración humano-IA», según la expresión de Swarat Chaudhuri, investigador científico en DeepMind. Este proceso permite a los agentes contribuir y corregirse en casi cada etapa, mientras solicitan la opinión y validación humanas en momentos clave. «No queremos ese mundo de la ambientación, donde la IA fija los objetivos, donde la IA produce las pruebas, y donde se pasan las pruebas que ella misma ha escrito. Existe un término medio.»
