endrazine/lean-cve-poc-14484CVE-2026-72711 — Error de solidez del kernel de Lean 4: envenenamiento de la caché de inferencia
Demostración de 0 = 1 sin axiomas mediante el envenenamiento de la caché FVar de una declaración opaca.
| Campo | Valor |
|---|---|
| Informe de error | leanprover/lean4#14484 |
| Corrección | leanprover/lean4#14498 |
| Afectado | Lean 4 ≤ v4.31.0 / todas las versiones anteriores |
| Corregido en | nightly 2026-07-23+, retroportado a v4.32.1 y v4.33.0 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-488 (Exposición de un elemento de datos a una sesión incorrecta), CWE-20 (Validación de entrada incorrecta) |
| CVE | CVE-2026-72711 |
La ruta environment::add_opaque del kernel de Lean 4 no llama a
check_no_metavar_no_fvar sobre el cuerpo de la declaración — a diferencia de las definiciones y
los teoremas, que realizan esta comprobación de cierre antes de verificar el tipo del valor.
Un metaprograma malicioso explota esta omisión mediante el envenenamiento de la caché de inferencia:
Cebado — Una expresión de tipo manipulada (cachePrimingType) es una beta-redex cerrada
definicionalmente igual a False. Mientras se verifica su tipo, el
kernel crea una declaración local temporal _kernel_fresh.2 : False y
almacena en caché su tipo inferido en la caché de inferencia de la instancia de type_checker.
Invalidación del contexto — El contexto local se restaura (la variable temporal
se elimina), pero la caché de inferencia persiste en la misma
instancia de type_checker. La entrada de la caché ahora está obsoleta — asigna un
identificador que ya no hace referencia a nada en el ámbito.
Explotación — El valor de la declaración opaca es un Expr.fvar
que apunta al identificador obsoleto. La consulta a la caché se dispara antes de que
la rama FVar compruebe la pertenencia al contexto local, devolviendo False como
tipo sin llegar a detectar nunca la variable no ligada.
El resultado es una constante opaca de tipo False aceptada por el kernel, de la cual
0 = 1 se deduce trivialmente.
El exploit:
addDecl del kernel--trust=0 (verificación máxima)#print axiomssorry, unsafeCast, debug.skipKernelTC, FFI ni manipulación de .oleanleanchecker --freshdocker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484
Salida esperada en una versión vulnerable de Lean:
[*] Running CachePoisonFalse.lean with --trust=0 ...
kernel accepted bad : False
'bad' does not depend on any axioms
'assumptionFreeFalse' does not depend on any axioms
'zero_eq_one' does not depend on any axioms
[!] VULNERABILITY CONFIRMED
zero_eq_one : 0 = 1
Depends on: no axioms
Bug class: Inference cache poisoning (CWE-488)
Root cause: missing check_no_metavar_no_fvar in add_opaque
Bug report: https://github.com/leanprover/lean4/issues/14484
Fix: https://github.com/leanprover/lean4/pull/14498
En una versión de Lean parcheada, el kernel rechaza la declaración opaca mal tipada 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 absoluta se ve afectado. Esto incluye:
leanchecker --fresh también acepta el exploit. El formato de exportación de comparator no puede expresar un FVar, por lo que esa ruta de validación no se ve afectada.En src/kernel/environment.cpp, la función add_opaque verifica el tipo del valor opaco pero no realiza la comprobación de cierre:
environment environment::add_opaque(declaration const & d, bool check) const {
scoped_diagnostics diag(*this, check);
opaque_val const & v = d.to_opaque_val();
if (check) {
type_checker checker(*this, diag.get());
check_constant_val(*this, v.to_constant_val(), checker);
// ← MISSING: check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
expr val_type = checker.check(v.get_value(), v.get_lparams());
// ...
}
}
Tanto add_definition como add_theorem llaman a check_no_metavar_no_fvar sobre sus valores antes de verificar sus tipos. La omisión en add_opaque es el punto de entrada.
La caché de inferencia en type_checker asigna expresiones a sus tipos inferidos. En infer_type_core, la búsqueda en la caché:
auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
return it->second;
se activa antes de que la rama FVar valide la pertenencia al contexto local:
case expr_kind::FVar: {
optional<local_decl> d = m_lctx.find_local_decl(e);
if (!d) throw_kernel_exception(...);
return d->get_type();
}
El atacante controla la población de la caché mediante la expresión de tipo, lo que hace que el nombre de la entrada obsoleta (_kernel_fresh.2) sea predecible y atacable.
| Aspecto | #14484 (este bug) | #14576 |
|---|---|---|
| Clase de bug | Envenenamiento de caché | Confusión de tipos mediante validación de proyección |
| Punto de entrada | add_opaque sin comprobación de cierre | Parámetros fantasma inductivos anidados |
| Caché implicada | Sí — caché de inferencia | Sí — comparación de hash de expr |
| Afecta a leanchecker | Sí | Sí |
| Afecta a comparator | No (FVar no expresable) | Sí |