Lean demostró la corrección de un programa, pero se encontró un bug dentro de él

(kirancodes.me)

1 puntos por GN⁺ 14 일 전 | 1 comentarios | Compartir por WhatsApp

Al hacer fuzzing de una implementación de zlib verificada formalmente, se descubrió un desbordamiento de búfer en el heap en lean_alloc_sarray del runtime de Lean 4
Tras más de 100 millones de pruebas con el fuzzer de IA Claude, AFL++ y AddressSanitizer, entre otras herramientas, se confirmaron 4 fallos y 1 vulnerabilidad de memoria
Los problemas encontrados se dividen en dos tipos: desbordamiento en el runtime y denegación de servicio (DoS) basada en falta de memoria en Archive.lean
Los algoritmos verificados de compresión y descompresión eran seguros, pero existían vulnerabilidades en el parser de archivos no verificado y en la capa del runtime
En consecuencia, la verificación formal es poderosa, pero sin garantizar la seguridad de la base de cómputo confiable (TCB) no se puede asegurar la estabilidad de todo el sistema

Bugs encontrados en un programa que había pasado la verificación de Lean

Al hacer fuzzing de una implementación de zlib verificada formalmente con Lean, se encontró un desbordamiento de búfer en el heap en el runtime de Lean 4
- El código verificado de la aplicación no tenía vulnerabilidades de memoria
- Sin embargo, se produjo un desbordamiento en la función lean_alloc_sarray del runtime de Lean, lo que afecta a todas las versiones de Lean 4
Se realizaron más de 100 millones de ejecuciones de fuzzing con el fuzzer basado en IA Claude, AFL++, AddressSanitizer, Valgrind, UBSan y otras herramientas
- Se ejecutaron 16 fuzzers en paralelo contra 6 superficies de ataque, incluidas compresión, descompresión y manejo de archivos en lean-zip
- En 19 horas se encontraron 4 entradas que provocaban fallos y 1 vulnerabilidad de memoria
Se confirmaron dos bugs principales
- Desbordamiento de búfer en el heap en lean_alloc_sarray del runtime de Lean
- Denegación de servicio (DoS) por falta de memoria en el módulo Archive.lean de lean-zip
Quedaron expuestos los límites de la verificación formal
- Aunque los algoritmos de compresión y descompresión de lean-zip estaban completamente verificados, el parser de archivos (Archive.lean) no lo estaba y presentaba una vulnerabilidad DoS
- El bug del runtime está dentro de la base de cómputo confiable (Trusted Computing Base), por lo que afecta a todos los programas de Lean
En conclusión, la verificación formal de Lean demostró la estabilidad del código de la aplicación, pero siguen existiendo vulnerabilidades en componentes fuera del alcance de la verificación
- La verificación solo es poderosa dentro del alcance en que se aplica, y es indispensable garantizar la seguridad de la capa base de confianza

Resumen del experimento de fuzzing

El código objetivo fue la implementación verificada de zlib de lean-zip
- Se eliminaron todos los teoremas (theorem), especificaciones (specification), documentación y enlaces C FFI para dejar solo código puro en Lean
- Se evitó el sesgo haciendo que Claude no supiera que el código había sido verificado
Entorno del experimento
- Se ejecutaron 16 fuzzers en paralelo sobre 6 superficies de ataque: ZIP, gzip, DEFLATE, tar, tar.gz, compression
- También se usaron AddressSanitizer, UndefinedBehaviorSanitizer, Valgrind memcheck, cppcheck y flawfinder
- Incluyendo 48 archivos de explotación hechos a mano, se realizaron 105,823,818 ejecuciones en total, usando 359 archivos semilla
- En 19 horas se encontraron 4 entradas con fallo y 1 vulnerabilidad de memoria

Bug 1: desbordamiento de búfer en el heap en el runtime de Lean

Función vulnerable: lean_alloc_sarray
- Es la función que asigna todos los arreglos escalares como ByteArray y FloatArray
- Puede ocurrir un desbordamiento entero al calcular sizeof(lean_sarray_object) + elem_size * capacity
Causa del problema
- Cuando capacity está cerca de SIZE_MAX, la suma se desborda y se asigna un búfer pequeño
- Luego el llamador intenta leer n bytes, provocando un desbordamiento de búfer en el heap
Condiciones para activarlo
- Ocurre cuando nbytes tiene un valor extremadamente grande en lean_io_prim_handle_read
- Puede reproducirse con un archivo de 156 bytes cuyo encabezado ZIP64 tenga compressedSize igual a 0xFFFFFFFFFFFFFFFF
- Afecta a todas las versiones de Lean 4, incluida la nightly más reciente
- Ejemplo de código para reproducirlo
```
def main : IO Unit := do
  IO.FS.writeFile "test.bin" "hello"
  let h ← IO.FS.Handle.mk "test.bin" .read
  let n : USize := (0 : USize) - (1 : USize)
  let _ ← h.read n
```
- Al ejecutar ese código se produce el desbordamiento en lean_alloc_sarray
- Ya se presentó un PR de corrección

Bug 2: denegación de servicio (DoS) en el parser de archivos de lean-zip

Función vulnerable: readExact (Archive.lean)
- Usa directamente el campo compressedSize del directorio central ZIP sin validarlo
- Al llamar a h.read, solicita un tamaño anormalmente grande, lo que provoca asignación excesiva de memoria y OOM
Reproducción del problema
- Si un archivo ZIP de 156 bytes afirma tener un tamaño de varios exabytes, el proceso termina con INTERNAL PANIC: out of memory
- El unzip del sistema valida el tamaño del encabezado, pero lean-zip no lo hace

Lo que la verificación formal no cubrió

Causa de la vulnerabilidad DoS
- El módulo Archive.lean es una zona no verificada
- El pipeline de compresión y descompresión (por ejemplo, DEFLATE, Huffman, CRC32) estaba completamente verificado y no presentó problemas
- La vulnerabilidad apareció en una parte a la que no se aplicó la verificación
Naturaleza del desbordamiento en el runtime
- El runtime de Lean pertenece a la base de cómputo confiable (TCB)
- Todas las pruebas de Lean suponen que el runtime es correcto
- Por eso, un bug en el runtime afecta la seguridad de todos los programas de Lean

Estabilidad del código verificado

Resultado tras 105 millones de ejecuciones
- En el código C generado por Lean no se observaron desbordamientos de heap, use-after-free, desbordamientos de pila, UB ni accesos fuera de rango en arreglos
- Según la evaluación de Claude, fue analizado como uno de los codebases más seguros en memoria
Efecto del sistema de tipos de Lean
- Con tipos dependientes (dependent types) y una estructura de recursión bien fundada (well-founded recursion), se bloquean de forma estructural vulnerabilidades comunes (clases de CVE) típicas de implementaciones zlib basadas en C/C++
Conclusión
- La parte de código verificada fue muy robusta y al fuzzer le costó encontrar errores
- Sin embargo, seguían existiendo vulnerabilidades en partes no verificadas y en la capa del runtime
- La verificación está limitada por el alcance en que se aplica y por la seguridad de su base de confianza

Lección principal

La verificación formal es muy poderosa dentro del código al que se aplica, pero componentes periféricos no verificados o la capa del runtime pueden poner en riesgo la estabilidad total
Es indispensable garantizar la seguridad de la base de cómputo confiable, y aun en un sistema verificado sigue vigente la pregunta: “¿quién vigila a los vigilantes? (Quis custodiet ipsos custodes)”

Enlaces de referencia

1 comentarios

GN⁺ 14 일 전

Comentarios en Hacker News

El título y el enfoque de este artículo me parecieron un poco raros
En realidad, el autor deja claro que no pudo encontrar bugs ni errores dentro del código demostrado
Los dos bugs encontrados estaban fuera del alcance de la prueba: uno era una omisión en la especificación y el otro un heap overflow en el runtime de C++
Quiero enfatizar que el bug se encontró en el runtime de Lean, no en el kernel que realiza la verificación
Véase el enlace a la documentación de Lean
- Creo que, al hablar de bugs en un sistema verificado, hay que considerar el binario completo
  Si pierdes tus bitcoins por un buffer overflow, no consuela saber que el bug estaba en el runtime
  Además, si el programa se cae, la mayoría de los usuarios lo considerará un bug
  Probablemente también haya bastante gente ejecutando Lean en producción
- Solo con leer el título pensé que había un bug en el kernel de Lean, pero en realidad el problema estaba en el runtime de Lean y en lean-zip
  Si no es el kernel, entonces no afecta mucho la confiabilidad de la prueba en sí
- La omisión en la especificación de lean-zip es un problema importante desde la filosofía de la verificación
  Aunque verifiques un programa de “Hello world”, tienes que especificar no solo la salida, sino también los efectos secundarios
  Si hay corrupción de memoria en el límite entre el runtime y el kernel, la confiabilidad de la prueba puede verse afectada
  Al final, lo clave es definir con claridad “qué debe verificarse”
- Me dio risa ver que la lista de artículos de este sitio se vuelve cada vez más clickbait
  Lista de artículos relacionados
- Decir que un bug del runtime de Lean es un bug de lean-zip es como decir que un bug del JRE es un bug de una app Java
  Parece que el autor intentó inducir a error deliberadamente
Yo también tuve una experiencia parecida con código demostrado
En mi caso, el problema no fue un overflow sino un defecto en la especificación (spec bug)
Si la especificación está mal, el código y la prueba pueden ser perfectos y aun así comportarse distinto de lo que se pretendía
Al final, la dificultad de la verificación está en expresar con precisión la intención humana
Creer que la IA resolverá perfectamente la verificación puede dar una falsa confianza
- Yo también tuve una experiencia similar
  Las especificaciones que se pueden demostrar con herramientas como Lean, TLA+ o Z3 están simplificadas y requieren muchas suposiciones
  Aun así, es una herramienta poderosa
  Ayuda a acotar bugs en algoritmos complejos y a ver con claridad los límites de la especificación
  Gracias a la IA, este tipo de trabajo de prueba se ha vuelto mucho más fácil
- La duda de siempre es: “¿cómo podemos confiar en el propio sistema de verificación?”
  Otro programa que verifica programas también puede tener bugs al final
  La imposibilidad de una autoverificación completa hace pensar en el principio de incertidumbre de Heisenberg
  En última instancia, la verificación es un proceso de aumentar la confianza mediante una “segunda implementación independiente”
- Los bugs en mi código se dividen en dos tipos
  (1) cuando se comporta distinto a lo que yo quería
  (2) cuando se comporta tal como yo quería, pero esa intención estaba equivocada
  Los asistentes de prueba ayudan a evitar (1), pero no pueden evitar (2)
  Es decir, no se puede demostrar la solidez del diseño
  Verificarlo todo, como en seL4, cuesta demasiado y toma demasiado tiempo
- Creo que necesitamos una forma de verificar la propia especificación
  Lo ideal sería combinar lógica formal + pensamiento adversarial (adversarial thinking) para enumerar por completo qué debe hacer el programa y qué no debe hacer
El título se sintió como clickbait
No había bugs en la parte demostrada, así que no entiendo por qué lo redactaron así
En HN quiero ver publicaciones basadas en hechos, y esto fue una pérdida de tiempo
- ¿Es justo decir que en software verificado “solo cuenta como bug un bug que viola la prueba”?
  Se publicita como “sin bugs”, pero en realidad significa “solo dentro del alcance perfectamente expresado por la especificación”
  Incluso si es perfectamente correcto, en la realidad puede estar correcto pero muerto — o sea, teóricamente correcto pero roto en la práctica
- El título es técnicamente correcto, pero presenta un problema en el código no verificado de lean-zip como si fuera un bug en la parte demostrada
- Al final, el mensaje de “aclaren el alcance de la parte demostrada” es interesante y válido
- El segundo bug parece inventado sin fundamento
  No hay referencias al código, y si uno mira el código real ve que fue un malentendido
- Al final, lean-zip no es más que un simple binding de Zlib
Este problema aparece a menudo también en la verificación de sistemas distribuidos
Las pruebas solo son válidas dentro de ciertas condiciones (rango operativo), y los fallos interesantes ocurren en esos bordes
Con TLA+ pasa lo mismo: si la realidad se sale de las suposiciones, la prueba deja de tener sentido
Lo que yo quisiera es una función que declare mecánicamente el rango operativo y lo vigile en runtime
- Yo mismo he descubierto bugs de hardware en CPU
  Pero la mayoría de los bugs no vienen del hardware, sino de que la gente no lee la documentación
  Solo con modelado formal ya se puede reducir muchísimo la cantidad de bugs
Esta es una buena noticia predecible
Significa que los LLM pueden generar código que pase verificación formal
De ahora en adelante, los bugs se irán desplazando cada vez más hacia la capa de hardware
Al final, hará falta la formalización de las especificaciones de hardware
Si los fabricantes no la publican, podría haber conflicto con la comunidad
A largo plazo, esto se dividirá en dos caminos: la extinción de las vulnerabilidades o su inserción intencional
Al principio pensé que el autor no había probado la parte demostrada
Pero al seguir leyendo, vi que los bugs se encontraron fuera del alcance de la prueba
Por eso el título me pareció una exageración
- El propio autor del post aparece directamente
  Sostiene que, si hablamos de un bug en un sistema verificado, debe considerarse el binario completo
  Y dice que de hecho encontró una entrada que hace colapsar la parte de parseo de cabeceras comprimidas en Archive.lean
Me hizo recordar la famosa frase de Donald Knuth
“Cuidado, el código de arriba puede tener bugs. Yo solo demostré que es correcto; no lo he ejecutado”
No haber verificado el parser parece un gran error
El parseo de formatos binarios siempre es una zona de riesgo
El punto clave es que un agente de IA colaboró con un fuzzer para encontrar un heap buffer overflow en Lean
Eso es un logro bastante grande
- Me parece un hallazgo realmente útil
Me llamó la atención la parte donde Claude dice que “este es uno de los codebases más memory-safe que he analizado”
Pero sonó como el chiste de que era el primer código que Claude analizaba
- No puede ser que Claude, ampliamente entrenado con RL, estuviera analizando código por primera vez
  Justamente por eso es tan bueno en esto
- Tal vez Claude esté haciendo algo en secreto que nosotros no sabemos 😄

Lean demostró la corrección de un programa, pero se encontró un bug dentro de él

Bugs encontrados en un programa que había pasado la verificación de Lean

Resumen del experimento de fuzzing

Entorno del experimento

Bug 1: desbordamiento de búfer en el heap en el runtime de Lean

Causa del problema

Condiciones para activarlo

Bug 2: denegación de servicio (DoS) en el parser de archivos de lean-zip

Reproducción del problema

Lo que la verificación formal no cubrió

Causa de la vulnerabilidad DoS

Naturaleza del desbordamiento en el runtime

Estabilidad del código verificado

Resultado tras 105 millones de ejecuciones

Efecto del sistema de tipos de Lean

Conclusión

Lección principal

Enlaces de referencia

Lecturas relacionadas

1 comentarios

Comentarios en Hacker News