Anthropic: Claude escribió pruebas verificadas por máquina para el código compilado de 123 bibliotecas de código abierto
El Frontier Red Team de Anthropic y la empresa de métodos formales Theorem usaron Claude para demostrar que 239 puntos de entrada de pruebas de fuzzing en 123 bibliotecas de OSS-Fuzz no pueden fallar con entradas de menos de 64 MB en un entorno modelado. El trabajo halló errores que años de fuzzing no detectaron, aunque las pruebas tienen salvedades importantes.
Anthropic ha publicado una investigación en la que su Frontier Red Team, junto con la empresa de métodos formales Theorem, usó Claude para verificar formalmente propiedades de seguridad de 123 bibliotecas de código abierto del proyecto OSS-Fuzz de Google, con 239 puntos de entrada de fuzzing. Las pruebas trabajan sobre código máquina RISC-V compilado, no sobre el código fuente.
Cómo funcionó
Cada prueba de fuzzing existente se convirtió en una especificación formal: el test compilado no debe fallar (por ejemplo, por un error de memoria detectado por AddressSanitizer o una aserción fallida) con ninguna entrada de menos de 64 MB en un entorno modelado. Theorem aportó modelos formales del conjunto de instrucciones RISC-V y del comportamiento de procesos de Linux; Claude escribió las pruebas y el verificador Rocq las validó. Según DevOps.com, Claude generó unos 180 millones de líneas de pruebas en pocas semanas.
Errores que el fuzzing no vio
Claude podía parchear los errores que encontraba, y salieron a la luz cientos. Entre los ejemplos, un subdesbordamiento de contador en un descompresor que solo provocaba una escritura fuera de límites con entradas de unos 20 MB, y un error de lectura en un decodificador de imágenes que requería 64 MB. Anthropic dice que penalizó los parches grandes y los auditó para que el modelo no reescribiera programas que trivialmente nunca fallen.
Límites
Anthropic subraya que “verificado formalmente” no significa “sin errores”. Las pruebas suponen binarios RISC-V de un solo hilo, enlazados estáticamente con musl libc, mientras que la mayoría del software Linux corre en x86 o ARM con glibc; AddressSanitizer no detecta todos los errores de memoria y no se verificaron todos los puntos de entrada. El coste es otra limitación: las pruebas pueden consumir cientos de millones de tokens. Las mejoras de eficiencia de los nuevos modelos Claude proceden de pruebas internas de Anthropic. Parte de las pruebas se ha publicado en GitHub.
También disponible en: EnglishСаха тылаРусский中文Portuguêsالعربية