De tests a demostraciones: verificación formal con LLM en 123 bibliotecas open source

Llevamos unas semanas en las que casi cada día hay una noticia de fallos de seguridad encontrados con IA, y esta misma semana hemos tenido PHP2Shell, descubierto con ayuda de modelos. Si encontrar fallos se ha vuelto barato, la pregunta es cuál es la defensa. Anthropic ha publicado LLMs are making formal software verification feasible at a much larger scale, en colaboración con Theorem, y su respuesta es ambiciosa: demostrar que el código no tiene ciertos fallos, en lugar de buscarlos uno a uno.

Qué es la verificación formal y por qué casi nadie la usa

Verificar formalmente un programa consiste en traducirlo a un modelo matemático y demostrar que siempre cumple unas reglas, por ejemplo, que nunca accede a memoria fuera de sus límites. Si la demostración falla, el punto donde falla indica dónde puede haber un fallo. Se corrige y se vuelve a intentar, hasta que la demostración sale.

El problema es el coste. Las demostraciones pueden ser muchas veces más grandes que el código, y escribirlas exige una especialización muy poco común. El ejemplo clásico es seL4, un núcleo de sistema operativo: escribirlo costó dos años-persona y verificarlo formalmente, veinte. Por eso la verificación formal se ha quedado en nichos como la aviónica.

Convertir los tests de fuzzing en especificaciones

El primer obstáculo es decidir qué significa “correcto”. Para un decodificador PNG hay una especificación clara, el RFC, pero para la mayoría de programas no. El truco del proyecto es aprovechar algo que ya existe: los tests de fuzzing.

Un fuzzer genera millones de entradas semialeatorias contra un punto de entrada del código, y cualquier entrada que provoque un fallo es un error que interesa a los autores. Pero es fuerza bruta: por mucho que se ejecute, nunca garantiza haber probado todos los caminos. La idea es convertir ese test en una especificación: “este test no falla con ninguna entrada de menos de 64 MB”. Si se demuestra, el fuzzer ya no tiene nada que encontrar en ese punto de entrada.

flowchart LR
    A["Biblioteca y su test de fuzzing"] --> B["Binario RISC-V"]
    B --> C["Especificación · no falla con ninguna entrada"]
    D["Semántica de RISC-V y Linux"] --> C
    C --> E["Claude escribe la demostración"]
    E --> F["Rocq comprueba la demostración"]
    E -->|"fallo encontrado"| G["Parche y nueva especificación"]
    G --> C

Lo hicieron con proyectos de OSS-Fuzz, el programa de Google de fuzzing continuo para proyectos open source, que además compila el código C y C++ con AddressSanitizer para que cualquier acceso incorrecto a memoria provoque un fallo. Así, demostrar que el test no falla es demostrar también una forma de seguridad de memoria.

Y lo hicieron sobre el binario compilado, no sobre el código fuente: las demostraciones razonan sobre las instrucciones RISC-V, usando un modelo formal de esa arquitectura y de los procesos de Linux.

Los números

Son cifras enormes, pero lo interesante es que casi nada de eso necesita revisión humana. El comprobador de demostraciones de Rocq garantiza que la demostración cumple la especificación. Lo único en lo que hay que confiar es en los modelos formales de RISC-V y de Linux, en el enunciado exacto de lo que se ha demostrado y en el propio Rocq. Es el mismo principio que comentaba con las semillas de las curvas NIST o con la ingeniería inversa de hardware: cuando el resultado se puede comprobar de forma objetiva, da igual cuántas líneas haya escrito el modelo.

Los fallos que aparecieron por el camino

Intentar las demostraciones sacó a la luz cientos de fallos, muchos de los que un fuzzer difícilmente encontraría, porque los fuzzers suelen trabajar con entradas pequeñas, normalmente de hasta 1 MB:

• Un desbordamiento por debajo de un contador en un descompresor que provocaba una escritura fuera de límites, pero sólo con entradas de unos 20 MB con una estructura concreta y poco habitual.
• Una lectura fuera de límites en un decodificador de imágenes que necesitaba una entrada de 64 MB y más de 2 GB de memoria.
• Una lectura fuera de límites que sólo aparecía con una secuencia concreta de llamadas sobre dos manejadores del mismo fichero.
• El redescubrimiento de un CVE de libexpat que necesitaba una entrada muy anidada.
• Fallos de lógica que nunca provocan un fallo de ejecución, como una función para restringir qué ficheros puede cargar una aplicación que no siempre se aplicaba.

Claude corregía el fallo, se regeneraba la especificación con el código corregido y seguía con la demostración. Hay un riesgo evidente, que el propio informe reconoce: el modelo podría “hacer trampa” reescribiendo el programa para que nunca falle de forma trivial. Para evitarlo, penalizaron los parches, premiaron demostrar qué entradas cambiaba cada parche y revisaron todos los cambios.

Un detalle que me ha gustado: demostrar que un test no falla a veces obliga a demostrar mucho más. Para cpp-httplib, había que descartar un desbordamiento de pila por recursión en el destructor de std::set, así que Claude tuvo que demostrar, sobre código máquina, que el árbol rojo-negro de libc++ mantiene su profundidad acotada de forma logarítmica.

Otros experimentos

El informe cuenta otras pruebas con verificación formal:

• zlib en el kernel de Linux: Claude escribió una especificación formal del RFC 1950 y demostró, sobre el binario x86, que la implementación la cumple. Para eso generó también la semántica formal de x86, tan completa que permite arrancar un userspace de Ubuntu, y que de paso encontró cientos de errores en la documentación oficial de referencia.
• Un intérprete de Python en Rust, demostrado con Verus contra la semántica de CPython. En 1,7 millones de programas aleatorios, se comportó igual que CPython en el 99,95% de los casos.
• Un lector de PDF muy usado, en el que encontraron en una semana tantos fallos de seguridad como los que se suelen reportar en un año.

El coste, y por qué va a bajar

La gran limitación es el precio: una demostración puede costar cientos de millones de tokens. Pero hay dos tendencias a favor:

• Los modelos nuevos necesitan menos tokens. En 36 tareas de verificación sacadas de OSS-Fuzz, Opus 5.5 demuestra la mitad usando un 40% menos de tokens que Opus 5.
• Las demostraciones se reutilizan. Gran parte de cada demostración trata de código que tienen todos los programas, como la inicialización del runtime de C. Cuando los agentes podían copiar las demostraciones de otros, necesitaban un 17% menos de tokens, y algunos lograron demostraciones en las que habían fallado trabajando solos.

La reutilización es la clave a largo plazo. Igual que Mathlib, la biblioteca de matemáticas formales de Lean, ha crecido hasta casi 300.000 teoremas apoyándose unos en otros, cada dependencia de software sólo tendría que verificarse una vez. Theorem tiene incluso una hoja de ruta para verificar todo el ecosistema de Nix, incluidos glibc, OpenSSL y cURL.

Los límites

El informe es honesto con lo que no significa todo esto: “verificado formalmente” no quiere decir “sin fallos”. Una demostración garantiza que el programa cumple la especificación en el modelo de máquina que se ha usado, y la realidad puede ser distinta:

• El modelo no es la máquina real. Las demostraciones son sobre binarios RISC-V estáticos, de un solo hilo y enlazados con musl. La mayoría de la gente usa estas bibliotecas en x86 o ARM, enlazadas dinámicamente con glibc.
• La especificación no cubre todo. AddressSanitizer no detecta todos los problemas de memoria, no se verificaron todos los puntos de entrada de cada biblioteca, y un programa puede usar mal una biblioteca correcta.

La ventaja es que se sabe exactamente dónde buscar: los fallos que queden estarán en los modelos de confianza o fuera de lo que se ha demostrado.

Lo que me llevo

Me parece de los trabajos más interesantes que he leído sobre IA y seguridad, precisamente porque no va de encontrar más fallos, sino de poder dejar de buscarlos. Y la idea de partir de los tests de fuzzing es muy inteligente: no hay que escribir especificaciones nuevas, se aprovecha lo que los propios desarrolladores ya habían decidido que era un error.

La conclusión del informe es que la verificación formal pronto será tan práctica como el fuzzing hoy. Con el coste actual, todavía es para bibliotecas críticas y equipos con recursos. Pero si los tokens necesarios siguen bajando y las demostraciones se reutilizan entre proyectos, verificar las dependencias más usadas una sola vez puede cambiar mucho la seguridad del software que todos usamos. Han publicado parte de las demostraciones y los modelos formales para que cualquiera pueda comprobarlos, y Theorem ofrece aplicar el mismo proceso a otros proyectos open source.

Fuente: LLMs are making formal software verification feasible at a much larger scale, Anthropic y Theorem.