Google DeepMind logró un avance significativo al utilizar inteligencia artificial agéntica para verificar matemáticamente las garantías criptográficas clave del protocolo Signal. Este protocolo es la base de la seguridad en aplicaciones de mensajería masiva como Signal, Google Messages y WhatsApp, que protegen las comunicaciones de millones de personas en todo el mundo, incluidos usuarios de México y América Latina.
¿Qué significa verificar formalmente un protocolo criptográfico?
La verificación formal es un proceso que utiliza matemáticas para comprobar que un software funciona según lo previsto y carece de vulnerabilidades críticas. Durante décadas, se ha considerado una especie de santo grial de la seguridad informática, pero resultaba extremadamente lenta y costosa porque requería que expertos humanos describieran las propiedades del software, las convirtieran en fórmulas y desarrollaran pruebas rigurosas.
Con la llegada de la IA agéntica, ese proceso puede acelerarse drásticamente. DeepMind empleó un nuevo marco de trabajo llamado AlphaProof Code para generar las pruebas matemáticas que demuestran que ciertas partes del protocolo Signal cumplen con sus garantías de seguridad. El proyecto se completó en solo cuatro semanas y se considera una prueba de concepto.
Implicaciones para la seguridad de las comunicaciones
Este trabajo tiene una doble relevancia. Por un lado, proporciona una validación independiente de la criptografía que protege una cantidad enorme de comunicaciones globales. Por otro, demuestra la capacidad de DeepMind para aplicar verificación formal asistida por IA a problemas del mundo real.
Los investigadores no encontraron nuevas vulnerabilidades en las porciones del protocolo Signal que analizaron. Sin embargo, al aplicar AlphaProof Code a versiones antiguas de Signal que contenían fallos conocidos y ya corregidos, el sistema identificó correctamente esas vulnerabilidades y demostró que el protocolo no podía verificarse formalmente. Esto sugiere que la herramienta podría ser útil para auditar la seguridad de software heredado.
“Estamos muy entusiasmados con este resultado, pero queda un largo camino antes de poder escalarlo a todo el software del mundo, y queremos hacerlo”, señaló Swarat Chaudhuri, científico investigador de DeepMind, en declaraciones a WIRED.
El auge de la verificación formal asistida por IA
La verificación formal con ayuda de IA está teniendo un momento destacado, aunque aún no está claro qué tan práctica resultará para un uso generalizado ni cuán efectiva será para asegurar grandes cantidades de código. Este proyecto de DeepMind es un paso importante, pero sus propios autores reconocen que se trata de un hito dentro de un proceso mucho más amplio.
El análisis no verificó formalmente toda la aplicación celular de Signal, sino solo componentes específicos del protocolo. Aun así, los investigadores liberaron la especificación y las pruebas desarrolladas para que otros equipos puedan continuar con este tipo de verificaciones.
Impacto para desarrolladores y usuarios en Latinoamérica
Para los desarrolladores de la región que trabajan en aplicaciones de mensajería segura, este avance representa una señal alentadora: la IA podría reducir drásticamente el tiempo y el costo de auditar criptografía. Para los usuarios, implica una capa adicional de confianza en las herramientas que usan a diario para comunicarse.
Si bien la verificación formal aún no es ubicua, casos como el de Signal muestran que la combinación de IA y matemáticas puede fortalecer la seguridad del software que sostiene la vida digital moderna. El siguiente paso será escalar estas técnicas a otros protocolos y aplicaciones, un desafío que DeepMind ya ha declarado querer abordar.