endrazine/lean-cve-pocCVE-2026-72844 : Ejemplo de demostración de "0 = 1" utilizando una vulnerabilidad en el kernel de Lean 4.
Demostrando 0 = 1 sin axiomas mediante la evasión de la validación de proyecciones inductivas anidadas.
| Campo | Valor |
|---|
| CVE | CVE-2026-72844 |
| Aviso | VulnCheck VCSA |
| Informe de error | leanprover/lean4#14576 |
| Corrección | leanprover/lean4#14577 |
| Afectados | Lean 4 ≤ v4.31.0 / nightly ≤ 2026-07-27 |
| Corregido en | nightly 2026-07-29+ / v4.32.2 |
| CVSS 4.0 | AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 MEDIUM |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 6.3 MEDIUM |
| CWE | CWE-843 (Confusión de tipos) |
El kernel de Lean 4 no verifica que la estructura nombrada en una expresión de proyección coincida con el tipo del valor que se proyecta, y environment::add_inductive en src/kernel/inductive.cpp no comprobaba los tipos de las aplicaciones inductivas anidadas que son reemplazadas por tipos auxiliares, por lo que sus argumentos paramétricos escapaban a la comprobación.
Un metaprograma que se ejecuta en el proceso de Lean puede registrar un inductivo anidado mal tipado cuyo constructor aplica una proyección .proj C 0 a un valor del tipo no relacionado W, y el kernel admite la declaración a través de la ruta addDecl verificada ordinaria con la comprobación máxima del kernel. El resultado es una confusión de tipos que produce una prueba de False sin axiomas, de la que se puede derivar cualquier proposición, incluida 0 = 1.
El exploit:
addDecl del kernel--trust=0 (comprobación máxima)#print axiomssorry, unsafeCast, debug.skipKernelTC, FFI ni manipulación de .oleandocker build -t lean-cve-poc .
docker run --rm lean-cve-poc
Salida esperada en una versión vulnerable de Lean:
[*] Running ZeroEqOne.lean with --trust=0 ...
'bad' does not depend on any axioms
'boom' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
zero_eq_one : 0 = 1
[!] VULNERABILITY CONFIRMED — CVE-2026-72844
zero_eq_one : 0 = 1
Depends on: no axioms
En una versión de Lean parcheada, el kernel rechaza el inductivo mal tipado y el script informa que la versión no es vulnerable.
Cualquier sistema que confíe en las pruebas verificadas por el kernel de Lean como verdad fundamental está afectado. Esto incluye:
La causa raíz está en el manejo que hace el kernel de los tipos inductivos anidados. Al eliminar una ocurrencia anidada I Ds is, el kernel debe verificar que los argumentos paramétricos Ds coincidan con los parámetros declarados del inductivo. El código vulnerable no comprueba que las expresiones de proyección (.proj) en Ds hagan referencia al nombre de estructura correcto: se acepta un .proj C 0 w incluso cuando w : W y W ≠ C.
Combinado con una colisión de hash (el kernel usa comparaciones Expr.hash en su comprobación de igualdad definicional), esto permite a un atacante registrar declaraciones donde la asignación de tipos interna del kernel discrepa de la semántica real del término, lo que conduce a una confusión de tipos y a una prueba de False.