DeepMind prueba con IA que el cifrado de Signal es seguro

DeepMind demostró con IA que el protocolo de Signal es seguro

Cuatro semanas de trabajo con agentes de inteligencia artificial bastaron para demostrar matemáticamente lo que la industria venía auditando a mano durante años: que el protocolo de cifrado de Signal cumple sus garantías criptográficas. Lo hicieron investigadores de Google DeepMind con AlphaProof Code, un nuevo marco de verificación formal, y el resultado le importa a cualquier founder que construya sobre software de terceros: abre la puerta a probar que el código crítico hace lo que promete, en lugar de confiar en que lo hace.

ZDNET lo resume con una comparación útil: el equipo hizo en un mes lo que normalmente les llevaría años a expertos humanos. Y la criptografía en juego no es menor, porque protege las comunicaciones de la app de Signal, Google Messages y WhatsApp.

Qué demostró exactamente la IA de DeepMind

El análisis se centró en dos piezas centrales del protocolo: PQXDH, que negocia las claves iniciales de cifrado, y Triple Ratchet, que renueva esas claves a medida que avanza la conversación. Sobre ellas, los investigadores verificaron la confidencialidad hacia adelante (que los mensajes pasados sigan protegidos aunque una clave se filtre), la autenticación de mensajes y las condiciones para recuperar la seguridad después de una filtración de claves.

Leíste lo que hace la IA. ¿Y en tu negocio?

Un agente de IA puede quedarse con parte de tu día: ordenar lo pendiente y pedirte el OK antes de actuar. El Kit «tu mano derecha con IA» trae un video de 11 minutos y una ficha para dejar al tuyo trabajando. CAR está cerrada por ahora; al anotarte, te avisamos cuando abra.

👥 Quiero el Kit →

El resultado tiene dos lecturas. La primera: no aparecieron vulnerabilidades nuevas en las porciones revisadas. La segunda, más interesante para cualquiera que evalúe herramientas de IA: cuando aplicaron AlphaProof Code a versiones antiguas de Signal que contenían fallos ya conocidos y corregidos, la herramienta los identificó correctamente y demostró que el protocolo no podía verificarse. Es decir, la IA no solo dijo ‘todo bien’: también supo decir ‘aquí no se puede probar’.

DeepMind publicó la especificación y las pruebas que desarrolló para que otros equipos las reutilicen, y realizó el análisis gratis como proyecto de investigación. Google declinó revelar cuánto costó y no comentó si lanzará un producto comercial de verificación formal.

Cómo lo hicieron: agentes, Lean y millones de líneas de prueba

El reparto de trabajo es la parte que más debería interesar a un equipo de producto. Según ZDNET, los humanos trabajaron junto a los agentes para definir qué había que probar, y varios agentes corriendo Gemini Carbon, el modelo más reciente de la compañía, ejecutaron las demostraciones. Después, los propios agentes auditaron la prueba y marcaron las zonas que necesitaban una segunda mirada humana: apenas el 1% del código, lo que en la práctica significa un ahorro enorme de horas de especialista.

El detalle técnico, reportado por el medio coreano Digital Today, es que el trabajo no se quedó en el diseño teórico del protocolo. El equipo tomó libsignal, la librería central escrita en Rust, la compiló a código máquina AArch64 para Linux y analizó matemáticamente el comportamiento del binario resultante. En total, unos 6,5 millones de líneas de código de prueba en Lean, el lenguaje de verificación formal que también usa Anthropic en sus proyectos.

Ese punto es clave: verificar el binario compilado, y no solo el código fuente, cierra la brecha donde suelen esconderse los errores que introduce el compilador.

Qué alcance real tiene y qué quedó afuera

Los propios investigadores insisten en que esto es un hito, no la meta. El análisis no verificó toda la aplicación móvil de Signal y dejó fuera de su alcance los chats grupales, los entornos multidispositivo y la totalidad de los ataques con computación cuántica. Parte de la seguridad de ciertas operaciones criptográficas sigue apoyada en supuestos, no en pruebas.

Swarat Chaudhuri, científico investigador de DeepMind, lo dice sin adornos: ‘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’. Pushmeet Kohli, científico jefe de Google Cloud y vicepresidente de investigación de DeepMind, apunta al caso de uso que mueve el mercado: ‘puedes imaginar bancos, imaginar a todas esas otras compañías que dependen de garantías y que se preocupan por los bugs, que ahora podrían decir: puedo probar estas propiedades’.

Ehren Kret, director de tecnología de Signal, valora el enfoque en un comunicado: mientras la verificación formal previa se centraba en porciones más pequeñas del código, el abordaje de DeepMind ‘permite una expansión significativa’, y verificar con rigor la implementación del protocolo les da ‘mayor confianza en las garantías de privacidad’.

Verificación formal: de santo grial de laboratorio a mercado

La verificación formal lleva décadas siendo el santo grial de la seguridad del software: en lugar de hacer pruebas que detectan fallos conocidos, se demuestra lógicamente que el programa no contiene errores. El problema siempre fue el costo en horas humanas, que la limitó a sistemas de misión crítica como los de la NASA o ciertos componentes de Apple.

Según Noticias Neo, ese cuello de botella es justo lo que el capital de riesgo está apostando a romper. Investigadores de Stanford mostraron que una herramienta de IA puede completar un proyecto de ingeniería en menos de medio día, una tarea que tres expertos tardaron cinco meses en resolver de forma manual. La startup &Truth ha recaudado 70 millones de dólares para verificar código en cualquier lenguaje, y Harmonic, con 295 millones de dólares en financiamiento, anunció que su agente Aristotle ya soporta verificación de software escrito en C y diseños de hardware en Verilog, y está evaluando la tecnología con fabricantes de chips como Tensordyne y Nvidia, cuyo brazo de capital riesgo figura entre sus inversores. En el mismo movimiento, Anthropic y la startup Theorem reportaron haber usado IA para detectar errores en software de código abierto que las pruebas convencionales no habían logrado identificar.

El caso de Anthropic es el más cercano al de DeepMind. A comienzos de noviembre presentó FlashProve, un prototipo open source que prueba criptográficamente qué modelo generó una respuesta. Según eWeek, el sistema genera pruebas de unos 19 MB que se verifican en 17 segundos en un procesador común, aunque producirlas cuesta entre 70 y 95 veces el tiempo de GPU de una inferencia normal. Es la misma tensión que enfrenta DeepMind: la tecnología funciona, la pregunta es a qué precio.

Qué significa esto para tu startup

Para un founder, la noticia no es que Signal sea seguro, porque su criptografía ya era de las más auditadas del mundo. La noticia es que el costo de demostrar que el software hace lo que dice podría dejar de ser prohibitivo. Eso cambia el cálculo en cuatro frentes concretos.

Revisa qué dependencias críticas usas sin poder probarlas. Si tu producto maneja pagos, datos de salud o credenciales, hoy dependes de la reputación del proveedor, no de una prueba. Empieza por inventariar esas dependencias y documentar cuáles son realmente críticas: la verificación formal se aplica primero a módulos acotados, no a sistemas enteros.
Pregunta a tus proveedores por el alcance, no por el titular. Cuando un vendor diga que su código está ‘verificado formalmente’, la pregunta correcta es qué porciones, bajo qué supuestos y con qué versión. El propio caso de DeepMind lo demuestra: no cubrió la app completa ni los chats grupales. Un ‘verificado’ sin alcance declarado no es una garantía.
Prepara tu código para ser verificable. La IA acelera la parte pesada, que es traducir especificaciones a fórmulas y desarrollar la demostración, pero los humanos siguen definiendo qué hay que probar. Eso exige módulos con responsabilidades claras y especificaciones escritas. Un monolito sin documentación no se verifica, se reescribe.
Aprovecha la ventana de costos. DeepMind hizo el análisis gratis como investigación y Google no reveló el costo. Para startups de LATAM y España, con presupuestos de seguridad limitados, la oportunidad está en adoptar estas herramientas temprano sobre un módulo pequeño y medir cuánto tiempo de auditoría ahorra, antes de que se conviertan en producto comercial.

Hay un matiz que conviene no perder. Chaudhuri insiste en que buscan un proceso de ‘colaboración humano-IA’, no un mundo donde la IA se fije sus propios objetivos y se corrija sus propios exámenes. Traducido a tu equipo: la IA puede escribir la prueba, pero alguien tiene que decidir qué se está probando y revisar el resultado.

Conclusión

Que una IA confirme que Signal es seguro no cambia nada para Signal. Lo que cambia es la evidencia de que la verificación formal, atrapada durante décadas en el laboratorio por su costo en horas humanas, podría volverse viable cuando un agente hace el trabajo pesado. Fueron cuatro semanas, un alcance limitado y un costo que Google no quiso contar: la cautela es obligada.

Pero si la tendencia se sostiene, el impacto va mucho más allá de la mensajería. Bancos, firmware de dispositivos médicos, software de redes eléctricas y cadenas de suministro completas podrían pasar de ‘creemos que es correcto’ a ‘está probado que lo es’. Para un founder, la jugada sensata no es esperar el producto comercial terminado, sino empezar a ordenar hoy el código y las dependencias que algún día querrá verificar.