endrazine/lean-cve-poc

# CVE PoC: Lean 4 内核可靠性漏洞 **通过嵌套归纳类型投影验证绕过，在不依赖公理的情况下证明 `0 = 1`。** | 字段 | 值 | |----------------|----------------------------------------------------| | 漏洞报告 | https://github.com/leanprover/lean4/issues/14576 | | 修复 | https://github.com/leanprover/lean4/pull/14577 | | 受影响版本 | Lean 4 ≤ `v4.31.0` / nightly ≤ 2026-07-27 | | 修复版本 | nightly 2026-07-29+ | | CVSS 3.1 | `AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N` — **7.1** | | CWE | CWE-843 (Type Confusion), CWE-20 (Improper Input Validation) | ## 漏洞概述 Lean 4 内核未能验证嵌套归纳类型声明中的投影表达式是否引用了正确的结构体。恶意的元程序可以注册一个归纳类型，其构造子类型将 `.proj C 0` 投影应用于类型为 `W`（而非 `C`）的值。由于内核在某些定义相等性检查中使用了表达式哈希比较，`Bool.false` 和 `Bool.true` 之间精心构造的哈希冲突会导致类型混淆，最终产生一个经过检查的 `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 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` 的证明。 ## 致谢 - **漏洞发现与最小 PoC**：@kiranandcode - **原始 CollatzLean 漏洞利用**：@xrchz (Ramana Kumar) - **内核修复**：Leonardo de Moura (PR #14577)

标签：Lean 4, 可靠性漏洞, 定理证明器, 概念验证, 类型混淆, 请求拦截