CVE-2026-72844：Lean 4 内核健全性漏洞

通过嵌套归纳类型投影验证绕过，在无公理条件下证明 0 = 1。

漏洞摘要

Lean 4 内核不会验证投影表达式中所命名的结构与所投影值的类型是否匹配，并且 src/kernel/inductive.cpp 中的 environment::add_inductive 没有对由辅助类型替换的嵌套归纳类型应用进行类型检查，因此其参数化参数逃逸了检查。

在 Lean 进程中运行的元程序可以注册一个类型错误的嵌套归纳类型，其构造器将 .proj C 0 投影应用于不相关类型 W 的值，内核会在最高内核检查级别下通过常规的已检查 addDecl 路径接受该声明。结果是产生类型混淆，得到一个不携带任何公理的 False 证明，由此可以推导出任何命题——包括 0 = 1。

该漏洞利用：

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

使用方法

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

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

在已修复的 Lean 版本上，内核会拒绝类型错误的归纳类型，脚本会报告该版本不存在漏洞。

影响

任何信任 Lean 内核检查证明作为事实依据的系统都会受到影响。这包括：

• 形式化验证软件：编译器、密码学库、智能合约、航空电子、汽车电子——任何基于 Lean 证明构建的安全论证，如果使用受影响版本构建，都将失效。
• 证明携带代码：Lake 包中的恶意依赖可以静默地引入不健全的声明，下游代码会使用这些声明。
• 独立检查器：同一类缺陷被证明也能绕过 Nanoda 独立类型检查器。

技术细节

根本原因在于内核处理嵌套归纳类型的方式。当消除嵌套出现 I Ds is 时，内核必须验证参数化参数 Ds 与归纳类型声明的参数匹配。存在漏洞的代码未能检查 Ds 中的投影表达式（.proj）是否引用了正确的结构名称——即使当 w : W 且 W ≠ C 时，.proj C 0 w 也会被接受。

结合哈希碰撞（内核在其定义性等式检查中使用 Expr.hash 比较），攻击者可以注册声明，使内核内部的类型分配与实际项语义不一致，从而导致类型混淆和 False 的证明。

参考

• NVD: CVE-2026-72844
• VulnCheck Advisory
• oss-security disclosure
• Lean 4 issue #14576
• Fix PR #14577
• Fix commit

致谢

• 漏洞发现与最小 PoC：@kiranandcode
• 原始 CollatzLean 漏洞利用：@xrchz (Ramana Kumar)
• 内核修复：Leonardo de Moura（PR #14577）
• CVE 提交与 PoC 打包：Jonathan Brossard (@endrazine)