Investigadores de Google DeepMind han usado inteligencia artificial para «verificar formalmente» —demostrar matemáticamente— varias de las garantías criptográficas clave del protocolo de Signal, el cifrado que protege las comunicaciones de Signal, Google Messages y WhatsApp. Lo hicieron como prueba de concepto en apenas cuatro semanas, con una nueva herramienta llamada AlphaProof Code. Lo cuenta Wired.
La verificación formal lleva años considerándose una especie de santo grial de la seguridad: usar las matemáticas para probar que un programa hace exactamente lo que debe y no esconde vulnerabilidades críticas.
¿Qué ha demostrado exactamente la IA de DeepMind?
Que las garantías criptográficas analizadas del protocolo de Signal se cumplen, con una prueba matemática en vez de con confianza. Según Wired, el trabajo es significativo por dos motivos: valida de forma independiente la criptografía que protege enormes cantidades de comunicaciones en plataformas como Signal, Google Messages o WhatsApp, y demuestra la capacidad de DeepMind en verificación formal con su nuevo marco de IA. El análisis no encontró vulnerabilidades nuevas en las partes revisadas; y cuando los investigadores aplicaron AlphaProof Code a versiones antiguas de Signal con fallos ya conocidos y corregidos, la herramienta los identificó correctamente y mostró que el protocolo no podía verificarse.
Conviene entender su alcance real, porque los propios investigadores insisten en que es un hito, no el final. El análisis fue limitado: no verificó, por ejemplo, toda la aplicación móvil de Signal. Es la misma frontera de «demostrar» en lugar de «confiar» que exploran otros laboratorios, como Anthropic con su herramienta FlashProve para verificar modelos, en un campo donde la IA está acelerando tareas antes lentísimas, como la formalización de pruebas matemáticas en lenguajes como Lean.
¿Por qué importa y qué dudas deja?
Porque abre la puerta a verificar código crítico que hoy solo se audita de forma parcial, aunque queda por ver si escala y a qué coste. Antes de la IA, describir las características de un programa, traducirlas a fórmulas y desarrollar la demostración era lentísimo; los agentes pueden recortar mucho ese trabajo. Ehren Kret, director de tecnología de Signal, lo valora en un comunicado: «mientras la verificación formal previa se centraba en porciones más pequeñas del código, el enfoque de Google DeepMind permite una expansión significativa», y añade que verificar con rigor la implementación del protocolo les da «mayor confianza en las garantías de privacidad».
La gran incógnita es si esto funcionará a gran escala y a un precio razonable. Swarat Chaudhuri, científico investigador de DeepMind, es franco: «estamos muy entusiasmados con este resultado, pero hay una larga distancia que recorrer antes de poder escalarlo a todo el software del mundo, y queremos hacerlo». DeepMind hizo el análisis gratis como proyecto de investigación, Google declinó revelar su coste y no quiso comentar si lanzará un producto comercial. Que sea precisamente Signal el protocolo elegido no es casual: es el referente de la mensajería cifrada, la misma empresa cuya responsable advierte de que los chatbots de IA no son tus amigos cuando hablamos de privacidad. Chaudhuri subraya además que buscan un proceso de «colaboración humano-IA», no un mundo donde la IA se marque sus propios objetivos y se corrija sus propios exámenes.
Mi lectura es que esto es más importante de lo que su tono prudente sugiere, aunque no por lo que parece. Que una IA confirme que Signal es seguro no cambia nada para Signal, cuya criptografía ya era de las más auditadas del mundo; el valor está en la demostración de que la verificación formal, el santo grial inalcanzable por su coste en horas humanas, podría volverse viable cuando una IA hace el trabajo pesado. Si eso se cumple, el impacto va mucho más allá de la mensajería: bancos, infraestructuras y cadenas de suministro de software podrían pasar de «creemos que es correcto» a «está probado que lo es». La cautela es obligada —fueron cuatro semanas, un alcance limitado y un coste que Google no quiere contar—, y el propio equipo evita vender humo. Pero si la verificación formal deja de ser un lujo de laboratorio, habremos ganado una de las herramientas más potentes que existen para fiarnos del software. Y eso, en un mundo que corre a delegarlo todo en código, no es poca cosa.