📻 Versión en audio: si prefieres escuchar en vez de leer, el resumen del artículo está justo aquí arriba.
El hueco entre el diseño y el binario
Llevo años leyendo papers de criptografía que terminan igual: «el protocolo es seguro, con pruebas formales». Todo bonito en la pizarra. El problema es que tú no ejecutas el paper, ejecutas el binario compilado, y ahí es donde históricamente aparecen los bugs. La brecha entre el diseño verificado y el código corriendo en tu teléfono es el clásico escondite de las vulnerabilidades reales. Esta semana esa brecha se cerró de forma concreta para el caso más rutilante posible: Google DeepMind anunció AlphaProof Code, un framework de agentes que verificó matemáticamente el código real del protocolo de Signal, el mismo que protege conversaciones en Signal y en Google Messages.
Qué hicieron de verdad, sin marketing
La parte que me agrada es que no es una demo con datos juguetes. Investigadores humanos y modelos tradujeron las metas de seguridad de Signal a especificaciones formales, y luego agentes impulsados por Gemini Carbon las demostraron generando más de seis millones de líneas de Lean, el lenguaje de pruebas que un verificador automático sí puede chequear línea por línea. Los mismos agentes auditaron su trabajo y marcaron para revisión humana apenas un 1% del código; el resto lo respalda el verificador de Lean, que no se cansa y no se distrae. Lo que antes tomaba a un equipo de expertos años, acá tomó cuatro semanas.
Y el detalle fino: no se conformaron con el nivel de diseño, que es donde casi siempre se queda la verificación formal. Probaron que el código compilado cumple las propiedades clave, como mantener los mensajes protegidos antes y después de que un dispositivo sufra un compromiso temporal, hasta las instrucciones exactas que corren en los dispositivos.
El test que me convenció
Me da lata creerle a un anuncio corporativo por arte de magia, así que lo que me terminó de convencer fue el control negativo. Reintrodujeron a mano dos bugs reales, ya corregidos, en una versión aislada del código de Signal. En ambos casos el sistema produjo una prueba verificada por máquina de que esa versión era insegura. O sea: no le pasaron código bueno esperando que dijera que es bueno, le pasaron código envenenado esperando que lo cachara, y lo cachó. Es la misma lógica con la que yo confío en un pipeline de CI: no me impresiona que pase el test, me impresiona que falle cuando debe fallar.
Qué cambia para el resto de nosotros
Para el usuario promedio, la noticia es tranquila: tus mensajes de Signal siguen funcionando igual, ahora con garantía matemática. El cambio de fondo es más lateral. DeepMind liberó los artefactos de verificación, y esa clase de evidencia emigra rápido de los labs a las exigencias de compra de gobiernos e infraestructura crítica. Si contratas software para algo serio, el día en que te pidan no un pentest sino un proof artifact chequeable está más cerca de lo que parece. El mismo enfoque apunta ahora a firmware de dispositivos médicos y software de redes eléctricas, donde una vulnerabilidad no te roba un chat, te apaga un hospital.
Mi opinión: esto no mata el pentesting ni el bug bounty, para nada. Lo que hace es mover la línea. Cuando tener una prueba formal del código de producción pase de proeza de laboratorio a opción razonable, los atacantes van a quedarse con los sistemas que no la tengan. Y ese es exactamente el tipo de asimetría que a los de abajo nos conviene vigilar de cerca.
Fuente de inspiración: Google DeepMind: AI agents formally verify the Signal protocol implementation
