viernes, 30 de octubre de 202623°General Pico · 10° / 25°Dólar Oficial $1.560Dólar Blue $1.565Dólar MEP $1.568Dólar Tarjeta $2.028
Claude verifica formalmente la ausencia de fallos de memoria en 123 bibliotecas de código abierto
Según informó anthropic.com, el modelo Claude generó pruebas matemáticas sobre el código de 123 bibliotecas abiertas y detectó errores que habían pasado inadvertidos durante años. La compañía sostiene que este enfoque podría volverse una parte central del desarrollo seguro de software.
Redacción PicoTecno
2 min de lectura
(Claude Lorrain / Wikimedia Commons · Public domain)
Según informó anthropic.com, la empresa utilizó su modelo Claude, en colaboración con la firma Theorem, para aplicar verificación formal a más de 100 bibliotecas de software de código abierto. La verificación formal consiste en demostrar matemáticamente que un programa cumple ciertas reglas de seguridad, en lugar de confiar solo en pruebas que lo ejecutan con distintos datos. Hasta ahora, esta técnica se usaba casi exclusivamente en sistemas críticos, porque requería años de trabajo de especialistas.
Los modelos de lenguaje de gran escala (LLM, por sus siglas en inglés) son sistemas de inteligencia artificial entrenados con enormes volúmenes de texto y código. De acuerdo con la publicación, estos modelos ya pueden producir pruebas formales de software real de manera autónoma, algo que antes era impráctico para la mayoría de los proyectos.
El alcance del trabajo fue amplio. Claude analizó 123 bibliotecas y comprobó 239 puntos de entrada, es decir, las funciones que reciben datos externos y que suelen ser el blanco de pruebas automatizadas. Las pruebas se hicieron sobre el código ensamblador, el nivel más bajo en que se escribe un programa antes de convertirse en un ejecutable. Para eso se usó la arquitectura RISC-V, un conjunto de instrucciones de código abierto. Según el texto, las demostraciones se escribieron en Rocq, un asistente de pruebas formales, y ocupan en total unos 180 millones de líneas.
Las pruebas tienen condiciones concretas. Cubren entradas de hasta 64 MB y asumen, entre otros supuestos, que cada programa corre como un binario de un solo hilo, con una cantidad fija de memoria y sobre Linux. Por eso la propia publicación aclara que todavía está lejos de eliminar todos los errores posibles, aunque la considera un avance importante. Durante el proceso, Claude también corrigió los fallos que encontró y detectó errores que no habían sido identificados en años, pese a haber pasado por billones de ejecuciones de prueba.
La empresa indicó que publicará un subconjunto de las demostraciones, junto con la semántica de RISC-V y de Linux, para que cualquiera pueda verificarlas y reutilizarlas. Theorem, por su parte, ofrece aplicar el mismo proceso a otros proyectos de código abierto y publicará una habilidad de Claude pensada para ayudar a los desarrolladores a comenzar con sus propios códigos.
El punto de partida que plantea la publicación es la creciente cantidad de fallos que los modelos de IA pueden encontrar y encadenar en ataques. Como ejemplo, menciona que el kernel de Linux tuvo recientemente más de 1.000 vulnerabilidades divulgadas. Para la compañía, los métodos tradicionales de defensa ya no alcanzan, y la verificación formal podría ofrecer garantías más sólidas. Aun así, reconoce que escribir pruebas sigue siendo costoso, y sostiene que ese costo debería bajar a medida que los modelos mejoren y que las pruebas puedan reutilizarse entre distintos proyectos.
