Anthropic utiliza Claude para verificar la seguridad de 123 bibliotecas de código abierto
La empresa Anthropic presentó una investigación que muestra cómo la inteligencia artificial puede ayudar a comprobar propiedades de seguridad del software mediante pruebas matemáticas formales. En colaboración con Theorem, el equipo utilizó Claude para analizar 123 bibliotecas de código abierto y generar pruebas sobre determinados comportamientos de sus programas compilados.
El trabajo cubrió 239 puntos de entrada utilizados en pruebas de software. Según Anthropic, el proceso permitió demostrar que esos componentes no se bloqueaban bajo determinadas condiciones y encontrar cientos de errores durante la elaboración de las pruebas.
De encontrar errores a demostrar propiedades
Muchas herramientas de seguridad ejecutan un programa con diferentes entradas para intentar provocar fallos. La verificación formal sigue otro camino: define una propiedad concreta y utiliza una prueba matemática que un verificador independiente puede comprobar.
En este proyecto, Claude generó pruebas sobre código compilado para la arquitectura RISC-V, mientras que el verificador Rocq comprobó los resultados. Este enfoque puede aportar garantías más precisas que una colección de pruebas tradicionales, siempre que se respeten las condiciones y supuestos definidos.
Un avance importante, pero con límites
La investigación no demuestra que las 123 bibliotecas estén completamente libres de vulnerabilidades. Las pruebas se concentraron en determinadas funciones y propiedades, bajo condiciones específicas de ejecución. Otros errores, usos incorrectos o componentes no cubiertos todavía pueden representar riesgos.
Aun con esas limitaciones, el enfoque podría ayudar a los desarrolladores a revisar componentes críticos, detectar fallas difíciles de reproducir y mejorar la seguridad de proyectos de código abierto utilizados por empresas y servicios digitales.
Comentarios
Publicar un comentario