Una IA de Google DeepMind verifica matemáticamente garantías clave del protocolo de Signal
Investigadores de Google DeepMind han utilizado inteligencia artificial para verificar formalmente varias garantías criptográficas esenciales del protocolo de Signal, la tecnología que protege las comunicaciones de aplicaciones como Signal, Google Messages y WhatsApp. El análisis se completó en apenas cuatro semanas mediante una herramienta experimental denominada AlphaProof Code.
El resultado no demuestra que toda la aplicación de Signal sea completamente invulnerable, pero sí supone un avance relevante en un campo que aspira a sustituir parte de la confianza en las auditorías por pruebas matemáticas verificables. El equipo no encontró vulnerabilidades nuevas en los componentes analizados y confirmó que la herramienta detectaba errores ya conocidos en versiones antiguas del protocolo.
Qué significa verificar formalmente un protocolo
La verificación formal consiste en describir con precisión qué debe hacer un programa y demostrar, mediante lógica y matemáticas, que cumple esas propiedades. En seguridad informática, este método permite comprobar que determinadas operaciones criptográficas respetan las condiciones necesarias para proteger los mensajes y las claves.
El procedimiento es mucho más exigente que una revisión convencional del código. Una auditoría puede localizar errores, comportamientos inesperados o patrones sospechosos, pero no garantiza que se hayan cubierto todos los casos posibles. La verificación formal intenta demostrar que, bajo unas condiciones definidas, el sistema se comporta exactamente como se espera.
Estas pruebas suelen escribirse en lenguajes especializados, como Lean, que permiten expresar teoremas y comprobar que cada paso de una demostración es válido. El problema es que traducir un protocolo complejo a fórmulas y construir después la prueba requiere normalmente una enorme cantidad de trabajo humano.
La IA acelera una tarea tradicionalmente lenta
AlphaProof Code está diseñada para ayudar a los investigadores a formalizar programas y desarrollar las demostraciones necesarias. En este caso, la inteligencia artificial se encargó de buena parte del trabajo pesado: transformar las propiedades de seguridad del protocolo en afirmaciones formales y encontrar los pasos que permitían probarlas.
El proceso se planteó como una colaboración entre personas y máquinas. Los investigadores definen el alcance, las propiedades que quieren analizar y las condiciones del modelo, mientras la IA propone estructuras, completa partes de las pruebas y ayuda a localizar inconsistencias.
Esta distinción es importante. La herramienta no establece por sí misma qué significa que un sistema sea seguro ni decide de manera autónoma cuáles son sus objetivos. Su función es ayudar a demostrar propiedades previamente definidas por especialistas.
Un análisis limitado, no una revisión completa de Signal
El trabajo se centró en varias garantías criptográficas del protocolo de Signal, no en el conjunto de la aplicación. Eso significa que no se verificaron todos los componentes del programa, como la interfaz, el sistema operativo del teléfono, las bibliotecas externas, los servidores o la protección física del dispositivo.
La seguridad de una aplicación de mensajería depende de muchos elementos adicionales. Un protocolo puede estar correctamente diseñado y, aun así, una vulnerabilidad en su implementación, en el almacenamiento de las claves o en el propio terminal podría comprometer la privacidad de un usuario.
Por ello, el resultado debe interpretarse como una prueba de concepto y no como un certificado absoluto de seguridad. La contribución principal está en demostrar que una IA puede ayudar a verificar una parte significativa de un protocolo utilizado a gran escala.
La herramienta también identificó fallos conocidos
Para comprobar la utilidad del sistema, los investigadores aplicaron AlphaProof Code a versiones anteriores del protocolo que contenían vulnerabilidades ya documentadas y posteriormente corregidas. En esos casos, la herramienta detectó que las propiedades de seguridad no podían demostrarse.
Este comportamiento resulta especialmente relevante porque muestra que el sistema no se limita a completar pruebas cuando todo está diseñado correctamente. También puede señalar que una afirmación de seguridad es falsa o que el modelo contiene un fallo que impide verificarla.
La capacidad de distinguir entre una implementación verificable y otra con errores podría ayudar a revisar cambios futuros en protocolos de comunicación, especialmente cuando se incorporan nuevas funciones o se modifican los mecanismos de gestión de claves.
El reto: ampliar el método sin disparar los costes
La verificación formal lleva décadas considerándose una de las vías más sólidas para aumentar la fiabilidad del software crítico. Sin embargo, su elevado coste y la complejidad de formalizar sistemas grandes han limitado su uso a componentes concretos, como determinados módulos de seguridad, procesadores o sistemas de control.
La inteligencia artificial puede reducir el número de horas necesarias para construir las pruebas, pero todavía no está claro hasta dónde puede escalar este enfoque. DeepMind realizó el análisis como proyecto de investigación y no ha detallado cuánto habría costado el trabajo en condiciones comerciales.
También queda por determinar si AlphaProof Code podrá aplicarse a aplicaciones completas, con millones de líneas de código, dependencias externas y cambios constantes. Verificar un protocolo aislado es una tarea muy distinta de demostrar la corrección de todo un servicio digital.
Una posible transformación para el software crítico
El interés del proyecto va más allá de las aplicaciones de mensajería. Si estas técnicas maduran, podrían utilizarse para revisar componentes de bancos, infraestructuras energéticas, sistemas sanitarios, redes de telecomunicaciones o cadenas de suministro de software.
En todos esos ámbitos, la seguridad suele depender de auditorías periódicas, pruebas automatizadas y la experiencia de los equipos de desarrollo. La verificación formal asistida por IA podría añadir una capa capaz de demostrar matemáticamente que ciertas propiedades se cumplen, en lugar de limitarse a buscar indicios de que el sistema funciona bien.
El resultado de DeepMind no convierte a Signal en una aplicación perfecta ni elimina la necesidad de auditorías independientes. Sí muestra, en cambio, que la IA puede acercar la verificación formal a sistemas más complejos y reducir una de sus principales barreras: el tiempo necesario para construir las pruebas.
La pregunta decisiva será si ese avance puede mantenerse cuando aumenten el tamaño del código, el número de condiciones y el coste de supervisión. Por ahora, el experimento ofrece una señal prometedora: pasar de confiar en que una parte del software es correcta a disponer de una demostración matemática de sus garantías puede empezar a ser una posibilidad práctica.
