Un experimento de seguridad automatizado, realizado con agentes de la IA Claude, ha revelado un desbordamiento de búfer de montón (heap buffer overflow) en el runtime de Lean 4, exponiendo una vulnerabilidad que afecta a todas las versiones del lenguaje publicadas hasta la fecha.
El investigador Kiran Anand utilizó el agente de IA para llevar a cabo más de 105 millones de ejecuciones de fuzzing contra `lean-zip`, una implementación nativa de zlib que había sido declarada matemáticamente correcta mediante procesos de verificación formal.
Aunque el código de la aplicación `lean-zip` no presentó vulnerabilidades de memoria, el experimento identificó un fallo crítico en la función subyacente `lean_alloc_sarray` del propio runtime de Lean.
Un fallo en el runtime
La vulnerabilidad se produce durante la asignación de arreglos escalares, como `ByteArray`. Cuando el tamaño de la asignación se aproxima al valor máximo permitido en un sistema de 64 bits, un desbordamiento de enteros (integer overflow) provoca que el runtime asigne un búfer minúsculo, mientras el sistema intenta escribir una cantidad masiva de datos en él.
Antes de realizar la prueba, Anand eliminó todos los teoremas, especificaciones y documentación de la base de código de `lean-zip`. Esta configuración garantizó que el agente de Claude operara sin saber que el código contaba con verificación formal, evitando así cualquier sesgo algorítmico.
Para localizar el error, el agente de IA puso en marcha 16 fuzzers en paralelo cubriendo seis superficies de ataque distintas, incluyendo la extracción de archivos ZIP y la descompresión de gzip. El agente empleó un conjunto de herramientas de seguridad que incluía AddressSanitizer, Valgrind y diversos motores de análisis estático.
Además del desbordamiento en el runtime, el experimento identificó una vulnerabilidad de denegación de servicio (DoS) en el analizador (parser) de archivos de `lean-zip`. Este componente específico no estaba incluido en el proceso de verificación formal.
Se ha enviado un informe de error a los desarrolladores de Lean, y actualmente se está trabajando en una solución que se encuentra pendiente en el repositorio de Lean 4.
