CVE-2026-72711 — Lean 4 内核健全性缺陷：推理缓存投毒

通过不透明声明 FVar 缓存投毒，无公理地证明 0 = 1。

字段	值
缺陷报告	leanprover/lean4#14484
修复	leanprover/lean4#14498
受影响版本	Lean 4 ≤ `v4.31.0` / 所有先前版本
修复于	nightly 2026-07-23+，已向后移植至 v4.32.1 和 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（数据元素暴露给错误会话）、CWE-20（输入验证不当）
CVE	CVE-2026-72711

漏洞摘要

Lean 4 内核的 environment::add_opaque 路径不会对声明体调用 check_no_metavar_no_fvar——这与定义和定理不同，后者会在对值进行类型检查之前执行此闭包检查。

对抗性元程序通过推理缓存投毒利用这一遗漏：

预热 — 一个精心构造的类型表达式（cachePrimingType）是一个闭合的 beta-redex，定义上等于 False。在对其进行类型检查时，内核会创建一个临时局部声明 _kernel_fresh.2 : False，并将其推断出的类型缓存到 type_checker 实例的推理缓存中。
上下文失效 — 局部上下文被恢复（临时变量被移除），但推理缓存仍保留在同一个 type_checker 实例上。该缓存条目现在已过期——它映射的标识符不再引用作用域内的任何内容。
利用 — 不透明声明的值是一个指向过期标识符的 Expr.fvar。缓存查找会在 FVar 分支检查局部上下文成员资格之前触发，返回 False 作为类型，而从未检测到未绑定变量。

结果是内核接受了一个类型为 False 的不透明常量，由此可轻易推出 0 = 1。

该利用程序：

仅使用经过检查的 addDecl 内核路径
以 --trust=0（最大检查）运行
通过 #print axioms 报告无公理
不使用 sorry、unsafeCast、debug.skipKernelTC、FFI 或 .olean 篡改
通过 leanchecker --fresh 重放

用法

docker build -t lean-cve-poc-14484 .
docker run --rm lean-cve-poc-14484

在存在漏洞的 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

在已修补的 Lean 版本上，内核会拒绝类型错误的 opaque 声明，脚本会报告该版本不受影响。

影响

任何将 Lean 内核检查的证明视为基准真相的系统都会受到影响。这包括：

形式化验证的软件：编译器、密码学库、智能合约、航空电子设备、汽车——任何基于 Lean 证明构建的安全案例，如果使用受影响的版本构建，都是无效的。
携带证明的代码：Lake 包中的恶意依赖可以静默地引入下游代码所使用的不健全声明。
独立检查器：报告者确认 leanchecker --fresh 重放也接受该漏洞利用。comparator 导出格式无法表达 FVar，因此该验证路径不受影响。
AI 生成的证明：像 AlphaProof、DeepSeek-Prover 和 Kimina-Prover 这样使用 Lean 作为可信后端的系统，可能产生利用内核漏洞而非证明定理的证明。

技术细节

根本原因

在 src/kernel/environment.cpp 中，add_opaque 函数检查 opaque 值的类型，但不执行闭包检查：

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 和 add_theorem 都会在类型检查之前对其值调用 check_no_metavar_no_fvar。add_opaque 中的遗漏正是入口点。

缓存投毒机制

type_checker 中的推断缓存将表达式映射到其推断出的类型。在 infer_type_core 中，缓存查找：

auto it = m_infer_type_cache[binfo_idx(bi)].find(e);
if (it != m_infer_type_cache[binfo_idx(bi)].end())
    return it->second;

fires before the FVar branch validates local-context membership:

case expr_kind::FVar: {
    optional<local_decl> d = m_lctx.find_local_decl(e);
    if (!d) throw_kernel_exception(...);
    return d->get_type();
}

攻击者通过类型表达式控制缓存填充，使陈旧条目的名称（_kernel_fresh.2）可预测且可被定位。

与 #14576 的比较

方面	#14484（本漏洞）	#14576
漏洞类别	缓存投毒	通过投影验证导致的类型混淆
入口点	`add_opaque` 缺少闭包检查	嵌套归纳幻影参数
涉及缓存	是 — 推断缓存	是 — 表达式哈希比较
影响 leanchecker	是	是
影响 comparator	否（FVar 无法表达）	是

致谢

漏洞发现：Patrick Hulin（@phulin），在 GPT-5.6 Sol 的协助下完成
内核修复：Joachim Breitner（@nomeata），PR #14498
PoC 打包：Jonathan Brossard（@endrazine）

lean-cve-poc-14484

最受欢迎