Google DeepMind logró un avance significativo al utilizar inteligencia artificial agéntica para verificar formalmente, es decir, demostrar matemáticamente, varias de las garantías criptográficas clave del protocolo Signal. Este trabajo, realizado como una prueba de concepto en solo cuatro semanas, representa un hito tanto para la criptografía de uso masivo como para el desarrollo de la propia IA.
La relevancia es doble. Por un lado, constituye una validación independiente adicional de la criptografía que protege una cantidad enorme de comunicaciones a nivel mundial en plataformas como la aplicación Signal, Google Messages y WhatsApp. Por otro, demuestra las capacidades de verificación formal de Google DeepMind mediante un nuevo marco de IA llamado AlphaProof Code.
¿Qué es la verificación formal y por qué importa?
La verificación formal es considerada desde hace tiempo una especie de santo grial en la seguridad del software. Consiste en utilizar matemáticas para comprobar y validar que un programa funciona según lo previsto, es decir, que no contiene vulnerabilidades críticas. Antes de la era de la IA, el proceso era extremadamente laborioso: los expertos debían describir las propiedades que querían demostrar, traducirlas a fórmulas y luego desarrollar la prueba correspondiente.
La IA agéntica puede reducir drásticamente el tiempo necesario para esta última etapa, permitiendo análisis como el de DeepMind sobre Signal. Sin embargo, incluso este análisis tuvo un alcance limitado: no verificó formalmente toda la aplicación celular de Signal, y los investigadores enfatizan que sus hallazgos son solo un hito en un proceso mayor.
“Estamos muy entusiasmados con este resultado, pero queda un largo camino por recorrer antes de que podamos escalar esto a todo el software del mundo, y queremos hacerlo”, declaró Swarat Chaudhuri, científico investigador de DeepMind, a WIRED.
Alcance y resultados del análisis
El análisis de DeepMind no encontró nuevas vulnerabilidades en las porciones del protocolo Signal que examinó. No obstante, cuando los investigadores aplicaron AlphaProof Code a versiones antiguas de Signal que contienen vulnerabilidades conocidas y corregidas hace tiempo, la herramienta las identificó correctamente y demostró que el protocolo no podía verificarse formalmente. Esto valida la eficacia del enfoque para detectar fallos.
Los investigadores están publicando la especificación y la prueba que desarrollaron para el análisis del protocolo Signal, con el fin de contribuir a otros trabajos de verificación formal.
Implicaciones para la seguridad del software
Más allá de Signal, la verificación formal asistida por IA está teniendo un momento destacado, aunque aún no está claro cuán práctica resultará para un uso generalizado ni cuán efectiva puede ser para asegurar grandes cantidades de código. Este trabajo de DeepMind es una muestra del potencial, pero también evidencia sus limitaciones actuales.
Para el público de México y Latinoamérica, este avance es relevante porque las aplicaciones de mensajería cifrada son herramientas cotidianas. La confirmación matemática de las garantías de seguridad de Signal refuerza la confianza en estas plataformas, al tiempo que abre la puerta a que en el futuro se puedan verificar otros sistemas críticos.
- Validación independiente: El estudio respalda la solidez criptográfica del protocolo Signal.
- Nuevo marco de IA: AlphaProof Code demuestra capacidades de verificación formal.
- Detección de fallos: La herramienta identificó correctamente vulnerabilidades en versiones antiguas.
- Publicación abierta: Los investigadores liberan la especificación y la prueba para futuros trabajos.
El camino hacia la verificación formal masiva del software aún es largo, pero este paso de DeepMind marca un precedente importante en la intersección de la inteligencia artificial y la ciberseguridad.