Seguridad de la IA
Anthropic y Theorem presentan pruebas escritas por IA para objetivos de fuzzing abiertos
Claude generó pruebas verificadas por máquina para 239 puntos de entrada de 123 bibliotecas, con límites explícitos de binarios, entradas, memoria y comportamiento.
Anthropic publicó el 22 de octubre una investigación con Theorem que afirma que Claude produjo pruebas formales de seguridad para 239 puntos de entrada de pruebas de fuzzing en 123 bibliotecas de código abierto. El trabajo convierte pruebas existentes en enunciados matemáticos sobre programas compilados y utiliza un comprobador independiente para validar los argumentos generados. Durante el proceso, el modelo también encontró y corrigió errores que impedían que esos enunciados se cumplieran.
Las garantías se aplican dentro de un entorno definido: binarios RISC-V estáticos y de un solo hilo, enlazados con musl, ejecutados en un modelo de procesos Linux con presupuestos de memoria fijos. El apéndice técnico especifica entradas menores de 64 MiB, y la documentación del controlador de Theorem indica que se rechazan archivos de ese tamaño o mayores. Las premisas del teorema también determinan qué respuestas del sistema operativo, distribuciones de memoria y condiciones de recursos quedan cubiertas.
El proceso utiliza el arnés de fuzzing existente de cada biblioteca, cuyas aserciones pueden expresar propiedades como la compresión y descompresión correctas. Compara binarios ordinarios con versiones que contienen comprobaciones de sanitizadores y razona sobre su comportamiento observable. El apéndice incluye entre los fallos las excepciones de ejecución, las terminaciones por aborto y el comportamiento ausente del modelo de procesos. Claude construye los argumentos en Rocq y su núcleo comprueba si establecen los enunciados requeridos.
La frontera de confianza sigue concentrada en los modelos formales de máquina y procesos, los enunciados exactos y el propio comprobador, incluidas las herramientas auxiliares y el entorno necesarios para comprobar cada binario. La cobertura sigue el código alcanzado desde el punto de entrada elegido y las comprobaciones presentes en el binario. Las propiedades ajenas a esas comprobaciones, y las diferencias entre el modelo y el hardware o los sistemas operativos desplegados, siguen siendo pertinentes al aplicar un resultado a software en producción.
La aplicación de parches introdujo otro reto: un agente podía facilitar una afirmación de ausencia de fallos eliminando comportamiento significativo del programa. Anthropic señala que el experimento penalizaba cada parche y otorgaba crédito adicional por demostrar qué entradas modificaba y lo reducido de ese conjunto. Los investigadores también registraron y auditaron los parches para detectar esos atajos. Tras una modificación, se regeneraba la especificación y el modelo intentaba demostrar el enunciado del programa revisado.
El material público es una parte de los resultados. En el momento de la revisión, el repositorio de Theorem enumeraba 60 puntos de entrada de 25 bibliotecas, con pruebas comprobadas mediante Rocq 9.2.0. Fija los binarios compilados y registra los enunciados y supuestos asociados. La versión publicada contiene pruebas de concordancia, que comparan comportamientos y excluyen errores especificados; aun así, pueden permitir una ejecución que nunca termina. La terminación exige un teorema separado.
El análisis experto del apéndice describe pruebas mucho más prolijas que las que escribiría normalmente un especialista humano. Los agentes detallaban repetidamente registros, direcciones de memoria y ramas de ejecución, aunque también desarrollaban algunas abstracciones conocidas. El análisis considera que mejorar la estructura modular sigue siendo una cuestión abierta para extender el método a programas más complejos. Separa la validez matemática de una prueba de la eficiencia y organización necesarias para producirla.
Theorem también ofrece su proceso OSS Verify sin coste a proyectos de código abierto que cumplan los requisitos. La elegibilidad se revisa individualmente según mantenimiento, uso, licencia y posición del proyecto en fronteras de seguridad o como base de otro software. El programa prioriza infraestructura ampliamente utilizada y comunica los errores descubiertos de forma privada a sus mantenedores. Su documentación indica que producir las pruebas puede llevar días y que pueden actualizarse después, vinculando cada resultado con compilaciones concretas del programa.