endrazine/lean-cve-poc-14484CVE-2026-72711 — Bug de solidité du noyau Lean 4 : empoisonnement du cache d'inférence
Prouver 0 = 1 sans axiome via l'empoisonnement du cache FVar d'une déclaration opaque.
| Champ | Valeur |
|---|---|
| Rapport de bug | leanprover/lean4#14484 |
| Correctif | leanprover/lean4#14498 |
| Affecté | Lean 4 ≤ v4.31.0 / toutes les versions antérieures |
| Corrigé dans | nightly 2026-07-23+, rétroporté vers v4.32.1 et 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 (Exposition d'un élément de données à une mauvaise session), CWE-20 (Validation d'entrée incorrecte) |
| CVE | CVE-2026-72711 |
Le chemin environment::add_opaque du noyau Lean 4 n'appelle pas
check_no_metavar_no_fvar sur le corps de la déclaration — contrairement aux définitions et
aux théorèmes, qui effectuent cette vérification de clôture avant de vérifier le type de la valeur.
Un métaprogramme malveillant exploite cette omission via l'empoisonnement du cache d'inférence :
Amorçage — Une expression de type forgée (cachePrimingType) est un beta-redex clos
définitionnellement égal à False. Pendant sa vérification de type, le
noyau crée une déclaration locale temporaire _kernel_fresh.2 : False et
met en cache son type inféré dans le cache d'inférence de l'instance type_checker.
Invalidation du contexte — Le contexte local est restauré (la variable temporaire
est supprimée), mais le cache d'inférence persiste sur la même
instance type_checker. L'entrée du cache est désormais obsolète — elle associe un
identifiant qui ne fait plus référence à rien dans la portée.
Exploitation — La valeur de la déclaration opaque est un Expr.fvar
pointant vers l'identifiant obsolète. La consultation du cache se déclenche avant que
la branche FVar ne vérifie l'appartenance au contexte local, renvoyant False comme
type sans jamais détecter la variable non liée.
Le résultat est une constante opaque de type False acceptée par le noyau, à partir de laquelle
0 = 1 découle trivialement.
L'exploit :
addDecl vérifié du noyau--trust=0 (vérification maximale)#print axiomssorry, ni unsafeCast, ni debug.skipKernelTC, ni FFI, ni altération de .oleanleanchecker --freshdocker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484
Sortie attendue sur une version vulnérable 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
Sur une version de Lean corrigée, le noyau rejette la déclaration opaque mal typée et le script signale que la version n'est pas vulnérable.
Tout système qui considère les preuves vérifiées par le noyau Lean comme une vérité de référence est affecté. Cela inclut :
leanchecker --fresh
accepte également l'exploit. Le format d'export comparator ne peut pas exprimer un
FVar, donc ce chemin de validation n'est pas affecté.Dans src/kernel/environment.cpp, la fonction add_opaque vérifie le type de la
valeur opaque mais n'effectue pas la vérification de clôture :
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());
// ...
}
}
add_definition et add_theorem appellent tous deux check_no_metavar_no_fvar sur
leurs valeurs avant de les vérifier de type. L'omission dans add_opaque est le
point d'entrée.
Le cache d'inférence dans type_checker associe les expressions à leurs types inférés.
Dans infer_type_core, la recherche dans le 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;
déclenche avant que la branche FVar ne valide l'appartenance au contexte local :
case expr_kind::FVar: {
optional<local_decl> d = m_lctx.find_local_decl(e);
if (!d) throw_kernel_exception(...);
return d->get_type();
}
L'attaquant contrôle le peuplement du cache via l'expression de type, rendant le nom de l'entrée obsolète (_kernel_fresh.2) prévisible et ciblable.
| Aspect | #14484 (ce bug) | #14576 |
|---|---|---|
| Classe de bug | Empoisonnement de cache | Confusion de types via la validation de projection |
| Point d'entrée | add_opaque sans vérification de fermeture | Paramètres fantômes inductifs imbriqués |
| Cache impliqué | Oui — cache d'inférence | Oui — comparaison de hachage d'expr |
| Affecte leanchecker | Oui | Oui |
| Affecte le comparateur | Non (FVar non exprimable) | Oui |