Anthropic anunció que su modelo de inteligencia artificial Claude logró escribir pruebas matemáticas verificadas automáticamente que demuestran que el código compilado de unas 123 bibliotecas de código abierto no puede colapsar bajo condiciones específicas, descubriendo cientos de vulnerabilidades de software que eludieron billones de pruebas tradicionales durante años.
Un logro sin precedentes en la verificación formal a nivel de lenguaje ensamblador
De las pruebas de fuzzing aleatorias a las demostraciones matemáticas en lenguaje Lean
El descubrimiento de cientos de vulnerabilidades pasadas por alto por las herramientas de escaneo tradicionales
Los límites de las garantías de seguridad y la evolución en la economía de la ingeniería de software
Preguntas frecuentes
Un logro sin precedentes en la verificación formal a nivel de lenguaje ensamblador
La empresa de desarrollo de inteligencia artificial Anthropic anunció que su modelo de lenguaje Claude ha logrado redactar y escribir pruebas matemáticas verificadas automáticamente que demuestran de manera categórica que el código compilado de 123 bibliotecas de software de código abierto no puede sufrir colapsos o interrupciones repentinas bajo condiciones operativas estrictamente definidas. Además de probar la confiabilidad del software, el modelo logró identificar y detectar fallas y vulnerabilidades profundas de programación que habían permanecido ocultas durante muchos años sin que nadie las notara, a pesar de que dichas bibliotecas habían sido sometidas a billones de ejecuciones y pruebas automatizadas continuas.
Estos resultados se presentaron en una investigación científica y técnica publicada el 22 de octubre, elaborada por el equipo de ruptura de fronteras (Frontier Red Team) de Anthropic en estrecha colaboración con Theorem, una empresa especializada en métodos matemáticos formales. Anthropic describió este proyecto como lo que considera “el primer esfuerzo a gran escala para utilizar la inteligencia artificial en la aplicación de la verificación formal al software de producción real a nivel de código ensamblador”. La empresa explicó en su documento de investigación que los sistemas de inteligencia artificial hoy en día son capaces de encontrar y explotar vulnerabilidades de software con extrema facilidad, por lo que depender exclusivamente de las pruebas de software tradicionales ya no es suficiente para defender los sistemas y protegerlos contra ciberataques avanzados.
De las pruebas de fuzzing aleatorias a las demostraciones matemáticas en lenguaje Lean
El equipo de investigación comenzó su misión a partir de pruebas aleatorias conocidas como fuzz testing, derivadas del programa OSS-Fuzz de Google, convirtiendo cada una de estas pruebas en una especificación matemática formal precisa. La estricta regla adoptada en estas especificaciones consistió en garantizar que la prueba nunca colapse al procesar cualquier entrada de datos de un tamaño inferior a 64 megabytes, tras compilar el código fuente al lenguaje de máquina de la arquitectura de procesadores de código abierto RISC-V.
A lo largo de varias semanas de trabajo continuo, el modelo Claude logró demostrar esta rigurosa regla para unos 239 puntos de entrada de software distribuidos en 123 bibliotecas de código abierto. Según los datos de Anthropic, el volumen total combinado de estas pruebas matemáticas alcanza unos 180 millones de líneas de código escritas en el lenguaje de demostración matemática Lean, mientras que una prueba típica individual abarca cerca de 600 000 líneas de código. El medio de noticias Interesting Engineering informó que el verificador de pruebas en el lenguaje Lean comprueba automáticamente que cada prueba cumpla con sus especificaciones matemáticas, lo que libera a los desarrolladores humanos de la necesidad de revisar millones de líneas generadas línea por línea.
Anthropic confirmó que actualmente está trabajando en la publicación de un subconjunto de estas pruebas para el público, junto con los modelos semánticos de la arquitectura RISC-V y el sistema operativo Linux en los que se basaron dichas demostraciones. En el mismo contexto, el medio Unite.AI informó que Theorem ofrece la ejecución del mismo proceso de canalización y verificación para proyectos de software de código abierto elegibles de manera totalmente gratuita a través de su nuevo programa llamado OSS Verify, y la empresa también ha lanzado una habilidad dedicada dentro del modelo Claude para ayudar a los mantenedores en el desarrollo de bibliotecas de software a registrarse y unirse al programa con facilidad.
El descubrimiento de cientos de vulnerabilidades pasadas por alto por las herramientas de escaneo tradicionales
Durante el proceso de formulación y redacción de las pruebas matemáticas, Claude reveló cientos de errores y vulnerabilidades de software ocultas. El modelo procedió a escribir parches de software para corregirlas antes de comenzar a demostrar formalmente la seguridad del código modificado. Entre los casos destacados documentados por la investigación, el modelo encontró en una herramienta de descompresión de datos un error derivado de una desalineación en un contador numérico, lo que provocaba la escritura de datos fuera de los límites de memoria permitidos; sin embargo, esta falla solo se manifestaba al introducir archivos de un tamaño cercano a los 20 megabytes que además poseían una estructura de diseño sumamente inusual.
En un segundo caso dentro de un programa de decodificación de imágenes, el modelo detectó una vulnerabilidad de lectura fuera de los límites de memoria, pero su activación requería entradas de 64 megabytes y el consumo de más de 2 gigabytes de memoria RAM, lo que explica la incapacidad de las herramientas de escaneo tradicionales para detectarla. Asimismo, Claude redescubrió una vulnerabilidad de seguridad conocida en la popular biblioteca libexpat y también identificó un grave defecto lógico en el que una característica diseñada para restringir los archivos permitidos para su carga por una aplicación fallaba y no se aplicaba en todas las circunstancias, según indicó el documento de investigación.
Los límites de las garantías de seguridad y la evolución en la economía de la ingeniería de software
A pesar de la importancia de este avance técnico, Anthropic advirtió claramente que estas pruebas matemáticas no significan que las bibliotecas de software estudiadas estén completamente libres de todos los errores posibles bajo cualquier circunstancia. Las pruebas completadas presuponen la existencia de un archivo ejecutable estático de un solo hilo que opera dentro de un presupuesto de memoria predefinido en una unidad central de procesamiento con arquitectura RISC-V bajo el entorno del sistema operativo Linux.
La empresa explicó en su informe que cualquier error de software restante se encuentra fuera del ámbito específico de estas pruebas o bien permanece latente en los componentes confiables en los que se basó el estudio, refiriéndose a los modelos matemáticos del hardware y del sistema operativo, la formulación de las propias teorías y la herramienta de verificación del lenguaje Lean en sí misma. Interesting Engineering señaló que la gran mayoría de los sistemas de software implementados en el mundo real dependen de otras arquitecturas de procesadores o configuraciones operativas multihilo que difieren del entorno virtual de la investigación.
No obstante, Anthropic considera que la viabilidad económica de la verificación formal de software está experimentando una transformación radical gracias a la inteligencia artificial. El equipo de investigación escribió al final de su informe un mensaje directo dirigido a los programadores: «Alentamos a todos los desarrolladores a explorar la verificación formal utilizando modelos de lenguaje grandes, en particular a aquellos que han probado este enfoque anteriormente con modelos menos capaces y descubrieron que no funcionó en su momento».
Preguntas frecuentes
Pregunta: ¿Qué demostró el modelo Claude en la nueva investigación de Anthropic?
Respuesta: El modelo Claude logró redactar pruebas matemáticas verificadas automáticamente que demuestran que el código compilado de unas 123 bibliotecas de código abierto no puede colapsar al procesar entradas de menos de 64 megabytes dentro de un entorno específico.
Pregunta: ¿Cuál es el volumen de las pruebas matemáticas escritas por el modelo Claude?
Respuesta: El volumen total de las pruebas alcanzó unos 180 millones de líneas de código escritas en lenguaje Lean a través de 239 puntos de entrada, con un promedio de cerca de 600 000 líneas por cada prueba.
Pregunta: ¿Cómo ayudó el proceso de verificación formal a descubrir nuevas vulnerabilidades?
Respuesta: Mientras intentaba probar la seguridad del código, Claude descubrió cientos de vulnerabilidades complejas que las pruebas de fuzzing pasaron por alto durante años, tales como fallas de desbordamiento de memoria en programas de descompresión y decodificación de imágenes y en la biblioteca libexpat, aplicando parches antes de probar su validez.
Pregunta: ¿Cuáles son las limitaciones técnicas de las garantías proporcionadas por estas pruebas?
Respuesta: Las pruebas asumen la ejecución de un archivo ejecutable estático de un solo hilo con un presupuesto de memoria determinado en un procesador RISC-V y Linux, y no cubren errores fuera de este alcance o latentes en los modelos de hardware y en el propio verificador de Lean.
