La empresa Anthropic presentó los resultados de experimentos sobre el uso de modelos de IA para la verificación formal de la fiabilidad y seguridad de proyectos existentes. Durante el experimento, se generaron pruebas matemáticas de ausencia de errores en la gestión de memoria utilizando modelos de IA para 123 bibliotecas de código abierto, probadas en la infraestructura de OSS Fuzz.
La verificación se realizó a nivel de código ensamblador compilado para la arquitectura RISC-V. El volumen total de pruebas generadas ascendió a alrededor de 180 millones de líneas de código para el sistema de verificación Rocq Prover (aproximadamente 600 mil líneas para un archivo binario con 18 mil instrucciones RISC-V). Las pruebas se generaron a través de la conversión automática de pruebas de fuzzing existentes en especificaciones formales, tras lo cual el modelo de IA Claude demostró que, con cualquier entrada de hasta 64 MB, no se producen fallos en el programa.
En el proceso de construcción de las pruebas, el modelo de IA pudo identificar y preparar correcciones para cientos de errores que no habían sido detectados durante las pruebas de fuzzing. Entre otras cosas, se identificaron vulnerabilidades que provocan desbordamientos de búfer al procesar ciertos datos de entrada (por ejemplo, CVE-2026-56132 en libexpat), así como errores lógicos. Además, se utilizó el modelo de IA para probar la conformidad de la implementación del algoritmo zlib en el núcleo de Linux con la especificación RFC 1950.
También se generó un intérprete en Rust para un subconjunto del lenguaje Python, para el cual se preparó una prueba formal de conformidad con la semántica de CPython utilizando la herramienta Verus. Para comparar el comportamiento con CPython, se realizaron más de 1.7 millones de programas de Python generados aleatoriamente. En un 99.95% de los casos, los resultados de la ejecución de estos programas en la nueva implementación y en CPython coincidieron, y las discrepancias encontradas resultaron ser casos límite conocidos.
La verificación formal realizada garantiza el cumplimiento de las especificaciones, pero no elimina completamente la posibilidad de problemas de seguridad, ya que los riesgos relacionados con problemas de multihilo, enlace dinámico y comportamientos anómalos del hardware real no quedan formalizados. La principal ventaja del enfoque propuesto es trabajar directamente con archivos binarios, lo que permite prescindir de la necesidad de reescribir el código existente en lenguajes formalmente verificables.
Fuente: opennet.ru
