IA en un minutoNoticiasSeguridad
Anthropic usa Claude, su modelo de IA, para demostrar propiedades de seguridad en 123 bibliotecas de código abierto
Redacción de IA en un minuto · Editor: Jon Elgezabal
En 30 segundos
Claude, el modelo de Anthropic, ha comprobado con matemáticas que parte del código de 123 bibliotecas abiertas no se cae por errores de memoria. El trabajo, hecho con Theorem sobre las instrucciones RISC-V del procesador, vale mientras la entrada no pase de 64 MB y se cumplan ciertas condiciones. Mientras trabajaba, salieron a la luz fallos que llevaban años escondidos, y parte de las demostraciones se publica para que otros las revisen.
Anthropic publicó el jueves 22 de octubre, junto a Theorem, una investigación en la que Claude, su modelo de IA, aplicó verificación formal (demostrar matemáticamente que un programa cumple unas reglas) a 123 bibliotecas de código abierto. Según la empresa, es el primer esfuerzo a gran escala de usar IA para hacerlo con software de producción a nivel de código ensamblador RISC-V (las instrucciones que ejecuta el procesador).
El punto de partida fueron las pruebas de fuzzing (las que bombardean un programa con entradas alteradas para hacerlo fallar) que esas bibliotecas tienen en OSS-Fuzz, de Google. Claude demostró que algunos de sus programas siempre terminan con normalidad, sin errores de seguridad de memoria, con cualquier entrada de menos de 64 MB y bajo ciertas condiciones: que corran en un solo hilo, en un procesador RISC-V con Linux y con un límite fijo de memoria. En unas semanas lo consiguió en 239 puntos de entrada de esas pruebas, con demostraciones que suman unos 180 millones de líneas en Rocq, la herramienta que las comprueba.
Mientras escribía las demostraciones, Claude encontró y corrigió errores que llevaban años sin detectarse pese a billones de ejecuciones de prueba. Uno, en un descompresor, solo aparecía con entradas de unos 20 MB y una disposición concreta, un tamaño que los fuzzers no suelen probar porque normalmente no pasan de 1 MB. También volvió a dar con una vulnerabilidad ya catalogada de libexpat.
Hasta ahora, esta técnica exigía años de trabajo de expertos y solo compensaba en sistemas críticos, como el software de aviónica de Airbus: programar seL4, un núcleo de sistema operativo, costó dos años-persona, y verificarlo, 20.
Anthropic publica parte de las demostraciones, junto con los modelos de RISC-V y de Linux en los que se apoyan, para que cualquiera pueda verificarlas; no publica las que podrían revelar fallos aún sin corregir. Theorem se ofrece a aplicar el mismo proceso a otros proyectos de código abierto y ha publicado una skill de Claude para empezar a verificar código propio.
La empresa reconoce que aún está lejos de corregir todos los fallos posibles. Las demostraciones no cubren todos los puntos de entrada de cada biblioteca, y la mayoría de la gente usa estas bibliotecas en procesadores x86 o ARM, no en RISC-V. El coste es otro límite: producir las demostraciones puede consumir cientos de millones de tokens, aunque, según Anthropic, su modelo Opus 5.5 gasta aproximadamente un 40 % menos de tokens que Opus 5 para resolver la mitad de 36 tareas de prueba.
Por qué importa · análisis y opinión
Demostrar que un programa está libre de cierto tipo de fallo era, hasta ahora, un lujo reservado a la aviónica y a otros sistemas críticos. Que una IA lo haga en serie cambia la conversación sobre seguridad: de buscar errores probando una y otra vez a poder garantizar por escrito que ciertos errores no existen. El paso al uso diario todavía no está dado. Las demostraciones valen para un procesador y una configuración que no son los habituales, consumen muchísimo cómputo y no cubren bibliotecas enteras. Para quien desarrolla o compra software, el beneficio inmediato es otro: el simple intento de demostrar destapa fallos que las pruebas de siempre no ven. Lo que hay que vigilar es si el método llega a los procesadores más comunes y si el coste baja lo bastante como para salir de los grandes proyectos de código abierto.
Fuente oficial: Anthropic · Redactada con ayuda de IA: cómo hacemos las noticias
