Un equipo de investigadores ha descubierto una vulnerabilidad crítica en el entorno de desarrollo Lean 4, a pesar de que una implementación de zlib (lean-zip) había sido formalmente verificada como correcta por Lean. El hallazgo, realizado por Kiran Gopinathan utilizando un agente Claude y herramientas de fuzzing (AFL++, AddressSanitizer, Valgrind, UBSan), revela un desbordamiento de búfer en la memoria del propio runtime de Lean 4, afectando a todas las versiones hasta la fecha (v4.31.0-nightly-2026-04-11). Además, se identificó una denegación de servicio en el parser de archivos de lean-zip debido a la falta de validación del tamaño comprimido en los encabezados ZIP. Este incidente pone de relieve las limitaciones de la verificación formal, ya que solo cubre las áreas donde se aplican las pruebas, y subraya una creciente preocupación sobre la seguridad del software, especialmente a medida que la IA se vuelve más efectiva en la detección de vulnerabilidades. La experiencia demuestra que, aunque la verificación formal puede aumentar la confianza en el código, no es una garantía absoluta de ausencia de errores y requiere una cobertura exhaustiva.
Noticias agregadas con IA