Verificación Formal a Escala con LLMs: Un Deep Dive en la Seguridad de Binarios RISC-V

La seguridad del software en la era de la IA generativa enfrenta un desafío fundamental: mientras los LLMs se vuelven expertos en encontrar y explotar vulnerabilidades, las defensas tradicionales basadas en pruebas heurísticas son insuficientes. La tesis central es que la verificación formal, históricamente costosa y reservada para sistemas de misión crítica, puede ahora ser escalada masivamente mediante el uso de LLMs. Esto resuelve el problema de la intratabilidad de la verificación manual, permitiendo la generación autónoma de pruebas de corrección a nivel de binario y ofreciendo garantías de seguridad sin precedentes para el software de producción. El contexto histórico muestra que la verificación formal, aunque teóricamente superior, siempre ha chocado con la barrera del esfuerzo humano, una barrera que los LLMs están derribando ahora.

Arquitectura del Sistema

El sistema propuesto integra LLMs en un pipeline de verificación formal para binarios RISC-V. El flujo comienza con la conversión de suites de fuzz tests existentes (ej. de OSS-Fuzz) en especificaciones formales. Estas especificaciones, que definen propiedades como la ausencia de crashes o errores de seguridad de memoria para inputs de hasta 64 MB, se expresan sobre el comportamiento de binarios RISC-V compilados en un entorno Linux modelado. El LLM (Claude en este caso) toma el código ensamblador RISC-V y las semánticas formales del conjunto de instrucciones RISC-V y del proceso Linux (proporcionadas por Theorem), y genera una prueba formal en Rocq. Esta prueba, que puede alcanzar cientos de millones de líneas, demuestra que el binario cumple la especificación. Un verificador de pruebas (Rocq proof checker) valida la corrección de la prueba. Si el LLM encuentra un bug durante el intento de prueba, lo corrige en el código fuente, regenera la especificación y procede a probar la nueva versión. Este proceso se repite hasta que se obtiene una prueba exitosa. La reusabilidad de las pruebas es un factor clave, ya que gran parte de ellas se superponen para componentes comunes como la inicialización del runtime C o AddressSanitizer.

Fundamentos Teóricos

Este trabajo se conecta directamente con los fundamentos de la lógica y la teoría de la computación, particularmente con el campo de la verificación formal de programas. Conceptos como la corrección de programas, la completitud y la consistencia, explorados por pioneros como Alan Turing y C.A.R. Hoare (con su lógica de Hoare para la verificación de programas), son centrales. La dificultad inherente de probar la corrección de programas se remonta al problema de la parada (Halting Problem) de Turing (1936), que establece límites fundamentales a lo que se puede probar algorítmicamente. Sin embargo, la verificación formal busca probar propiedades específicas de programas finitos. El uso de modelos matemáticos para representar el comportamiento del software y la aplicación de lógicas formales para derivar pruebas de propiedades de seguridad se basa en décadas de investigación académica. La contribución de los LLMs es automatizar la generación de estas pruebas, que tradicionalmente requerían un alto grado de experiencia humana, como se ejemplifica en la verificación del kernel seL4 (Klein et al., 2009).