Cuatro semanas bastaron para que Google DeepMind aplicara AlphaProof Code a propiedades de seguridad del código de libsignal, la implementación de referencia del protocolo de Signal. El resultado va más allá de comprobar un diseño criptográfico abstracto: las pruebas se refieren al binario compilado para AArch64. La diferencia importa porque una especificación correcta no garantiza, por sí sola, que el programa que llega a los dispositivos conserve las mismas propiedades.
El trabajo no demuestra que toda la aplicación Signal esté libre de fallos, ni cubre cada pieza del protocolo. Se concentra en propiedades clave de su núcleo criptográfico y en una versión concreta compilada para el análisis. Su interés está tanto en ese alcance como en el método: un sistema de agentes de IA generó millones de líneas de pruebas formales, mientras las decisiones que determinan qué significa «seguro» siguieron bajo revisión humana.
Del modelo del protocolo al ejecutable
La verificación formal expresa propiedades de un programa mediante especificaciones matemáticas y demuestra que el código las satisface. En este caso, el equipo abordó libsignal, la implementación de referencia del protocolo Signal. El trabajo de Google DeepMind cubrió el protocolo de establecimiento de sesión PQXDH y Triple Ratchet, con propiedades como secreto hacia delante, seguridad tras una vulneración y secreto del intercambio inicial. El artículo técnico también distingue entre el modelo simbólico y el computacional, dos formas de razonar sobre las garantías criptográficas.
El salto respecto a buena parte de la verificación previa está en el nivel examinado. Según los investigadores, los esfuerzos anteriores se habían centrado en modelos abstractos, reimplementaciones adaptadas a la verificación o propiedades más acotadas. AlphaProof Code, en cambio, conectó garantías del protocolo con el código sin modificar de libsignal, compilado con el compilador estándar de Rust a código máquina AArch64. El equipo describe el resultado como las primeras pruebas de propiedades de seguridad de protocolo para una implementación ampliamente desplegada y sin modificar.
El proceso combina cuatro piezas: personas y agentes redactan y revisan la especificación Lean; el código Rust se compila a un ejecutable; Lean representa la semántica del código máquina; y agentes probadores intentan demostrar los teoremas acordados. Un componente de control acepta una prueba solo si el kernel de Lean la verifica y confirma que se refiere a la especificación aprobada.
flowchart TD A["Expertos y agentes redactan la especificación"] --> B["Revisión y aprobación humana"] B --> C["Rust se compila a AArch64"] C --> D["Lean representa el ejecutable"] D --> E["Agentes generan pruebas"] E --> F["Kernel de Lean comprueba la prueba"] B --> G["Supuestos y contratos revisados"] G --> F
La escala del resultado es llamativa: el artículo técnico contabiliza alrededor de 6,5 millones de líneas Lean generadas por los agentes. Pero ese volumen no equivale a millones de líneas que una persona deba aceptar por confianza. Lean verifica las pruebas con su kernel; si una demostración contiene un error lógico, no debería superar ese control. La publicación de Google DeepMind resume la producción como más de seis millones de líneas y afirma que los agentes señalaron para revisión humana solo el uno por ciento de la base examinada.
La especificación sigue siendo el punto crítico
El verificador puede confirmar que una implementación satisface un teorema; no puede decidir si ese teorema expresa la garantía que realmente necesita una organización. La especificación define las propiedades, las condiciones de entrada y los supuestos sobre el entorno. Una hipótesis demasiado restrictiva o una propiedad formulada con poca fuerza puede permitir que el código «demuestre» algo insuficiente. Google DeepMind reconoce que elaborar y validar esa especificación requiere juicio experto, iteración y revisión.
En el caso de Signal, los agentes ayudaron a adaptar modelos formales existentes, pero no bastó con trasladarlos literalmente: los modelos previos trataban por separado el intercambio inicial y el ratchet, y no incluían el ratchet poscuántico desplegado. El equipo tuvo que componer y ampliar esas especificaciones con guía humana. Los agentes revisores buscaron debilidades, y los investigadores probaron que las hipótesis fueran satisfacibles y que los teoremas se cumplieran en ejecuciones concretas, para reducir el riesgo de una prueba vacía.
También importa qué queda dentro de la base de confianza. El trabajo formaliza una semántica de AArch64 y hace que Lean compruebe que los bytes representados corresponden al ejecutable, pero los investigadores explican que no pueden demostrar que el hardware y el sistema operativo reales se comporten exactamente como esa semántica. Además, el análisis depende de contratos para algunas rutinas externas y de supuestos sobre las primitivas criptográficas. La prueba es rigurosa dentro de esos límites; no elimina los límites.
Las pruebas producidas por los agentes son, en ese sentido, menos delicadas que las afirmaciones que se les pide demostrar. Lean puede rechazar una demostración defectuosa, pero no detecta por sí solo una especificación que omita una amenaza relevante o dé por sentado demasiado sobre el entorno. Ese reparto explica por qué el sistema no convierte la verificación en una tarea enteramente autónoma: automatiza la búsqueda de pruebas, no la responsabilidad de definir el objetivo.
Qué revelan los fallos reintroducidos
Para probar que el método podía distinguir código correcto de código vulnerable, el equipo reintrodujo dos errores previamente corregidos en versiones aisladas de libsignal. AlphaProof Code demostró que las variantes defectuosas no satisfacían los teoremas de seguridad. WIRED informa además de que el análisis del código actual no encontró vulnerabilidades nuevas en las partes examinadas. El resultado valida la capacidad del proceso para detectar esos fallos conocidos, pero no permite concluir que cualquier error, en cualquier parte de la aplicación, vaya a ser encontrado.
El alcance concreto es una diferencia decisiva para empresas que quieran interpretar estas pruebas. No se verificó toda la aplicación móvil de Signal ni la totalidad de sus componentes; se examinó el núcleo criptográfico definido por el proyecto, con un ejecutable vinculado a un pequeño programa de prueba. Tampoco se convierte la demostración en una garantía universal contra ataques: las propiedades probadas y los modelos empleados establecen qué ataques quedan excluidos bajo los supuestos declarados.
“We are very excited by this result, but there is a long distance to go before we are able to scale this to all the software of the world, and we want to do that,”
— Swarat Chaudhuri, investigador de Google DeepMind
La cautela es pertinente también para el calendario. El proyecto duró cuatro semanas, frente a años de trabajo experto que, según DeepMind, habría requerido una verificación de esta complejidad con métodos anteriores. Pero WIRED señala que el equipo partió de trabajo previo de verificación formal realizado por Signal. No es una medición del coste de aplicar el sistema desde cero a cualquier producto: Google DeepMind llevó a cabo este análisis como proyecto de investigación sin cobrar y no reveló su coste. Google tampoco comentó si planea ofrecer un producto o servicio comercial de verificación formal.
La oportunidad —y la factura pendiente— para las empresas
Para los equipos que mantienen software crítico, el cambio potencial está en el coste de producir pruebas profundas sobre código ya existente. El artículo técnico recuerda que proyectos anteriores de verificación formal de sistemas importantes exigieron años-persona; cita veinte para el microkernel seL4 y seis para el compilador CompCert. Aquellos sistemas, además, se escribieron teniendo en cuenta la verificación. libsignal representa un reto distinto: analizar código de producción preexistente, compilado sin modificar, y llevar las propiedades hasta el ejecutable.
La reducción de tiempo podría ampliar qué componentes justifican un esfuerzo formal, en lugar de reservarlo únicamente para sistemas diseñados desde el inicio alrededor de pruebas matemáticas. Google DeepMind plantea extender el enfoque a firmware de dispositivos médicos y software de redes eléctricas, y menciona combinarlo con sistemas como CodeMender. Para una empresa, eso abre una vía de evaluación; no prueba aún que el proceso sea asequible o reproducible en cualquier base de código.
Ese es el principal intercambio: menos trabajo manual en la construcción de demostraciones, a cambio de una inversión sostenida en especificaciones, revisión de supuestos y comprensión del entorno de ejecución. Los millones de líneas generadas reducen la carga de escribir pruebas, pero no sustituyen a especialistas capaces de decidir si las propiedades son adecuadas, ni a responsables que delimiten los componentes externos confiables. El porcentaje que requiere revisión humana tampoco significa que el 99 % del sistema haya quedado fuera de toda supervisión: significa que, según DeepMind, los agentes concentraron la revisión manual en una fracción del código analizado.
Google DeepMind ha publicado las especificaciones y las pruebas para que otros puedan examinarlas y reutilizarlas. La apertura permite estudiar el método y sus decisiones formales; el siguiente reto práctico será comprobar cuánto de ese trabajo puede trasladarse a otros sistemas y con qué coste. En el caso de Signal, la prueba alcanza el código criptográfico compilado, pero no toda la aplicación que lo rodea.
Fuentes: The Decoder, Google DeepMind, Google DeepMind researchers, WIRED
