endrazine/lean-cve-poc-14484CVE-2026-72711 — Bug de solidez do kernel do Lean 4: Envenenamento do cache de inferência
Provando 0 = 1 sem axiomas via envenenamento do cache FVar de declarações opacas.
| Campo | Valor |
|---|---|
| Relatório do bug | leanprover/lean4#14484 |
| Correção | leanprover/lean4#14498 |
| Afetado | Lean 4 ≤ v4.31.0 / todas as versões anteriores |
| Corrigido em | nightly 2026-07-23+, backportado para v4.32.1 e 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 (Exposição de Elemento de Dados à Sessão Errada), CWE-20 (Validação de Entrada Imprópria) |
| CVE | CVE-2026-72711 |
O caminho environment::add_opaque do kernel do Lean 4 não chama
check_no_metavar_no_fvar no corpo da declaração — diferentemente de definições e
teoremas, que realizam essa verificação de fechamento antes de verificar o tipo do valor.
Um metaprograma adversário explora essa omissão por meio do envenenamento do cache de inferência:
Preparação — Uma expressão de tipo elaborada (cachePrimingType) é uma
beta-redex fechada, definitionalmente igual a False. Durante a verificação de seu tipo, o
kernel cria uma declaração local temporária _kernel_fresh.2 : False e
armazena em cache seu tipo inferido no cache de inferência da instância de type_checker.
Invalidação de contexto — O contexto local é restaurado (a variável
temporária é removida), mas o cache de inferência persiste na mesma
instância de type_checker. A entrada do cache agora está obsoleta — ela mapeia um
identificador que não se refere mais a nada no escopo.
Exploração — O valor da declaração opaca é um Expr.fvar
apontando para o identificador obsoleto. A consulta ao cache é disparada antes de
o ramo FVar verificar a pertinência ao contexto local, retornando False como o
tipo sem nunca detectar a variável não vinculada.
O resultado é uma constante opaca do tipo False aceita pelo kernel, da qual
0 = 1 decorre trivialmente.
O exploit:
addDecl do kernel--trust=0 (verificação máxima)#print axiomssorry, unsafeCast, debug.skipKernelTC, FFI ou adulteração de .oleanleanchecker --freshdocker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484
Saída esperada numa versão vulnerável do 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
Em uma versão corrigida do Lean, o kernel rejeita a declaração opaca mal tipada e o script relata que a versão não é vulnerável.
Qualquer sistema que confia nas provas verificadas pelo kernel do Lean como verdade absoluta é afetado. Isso inclui:
leanchecker --fresh
também aceita o exploit. O formato de exportação comparator não consegue expressar um
FVar, portanto esse caminho de validação não é afetado.Em src/kernel/environment.cpp, a função add_opaque verifica o tipo do valor
opaco, mas não realiza a verificação de fechamento:
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 quanto add_theorem chamam check_no_metavar_no_fvar sobre seus valores antes de fazer a verificação de tipos. A omissão em add_opaque é o ponto de entrada.
O cache de inferência em type_checker mapeia expressões para seus tipos inferidos. Em infer_type_core, a consulta ao cache:
auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
return it->second;
dispara antes de o ramo FVar validar a associação ao 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();
}
O atacante controla o preenchimento do cache por meio da expressão de tipo, tornando o nome da entrada obsoleta (_kernel_fresh.2) previsível e direcionável.
| Aspecto | #14484 (este bug) | #14576 |
|---|---|---|
| Classe do bug | Envenenamento de cache | Confusão de tipos via validação de projeção |
| Ponto de entrada | add_opaque sem verificação de closure | Parâmetros fantasma indutivos aninhados |
| Cache envolvido | Sim — cache de inferência | Sim — comparação de hash de expr |
| Afeta o leanchecker | Sim | Sim |
| Afeta o comparator | Não (FVar não é expressável) | Sim |