CVE-2026-72844
中已发布
通过不匹配的结构投影绕过 Lean 4 内核类型检查
- 已发布
- 2026年8月20日
- 已更新
- 2026年8月20日
- 分配 CNA
- VulnCheck
- 观察到的证据
- 2026年8月24日
初级CVSS
6.8/ 10中
nvd · CVSS 4.0
CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X0.2%
低 · 未来 30 天
- 百分位
- 8.2%
- 型号日期
- 2026年9月21日
EPSS 是统计估计，而不是确定性或影响衡量标准。将其与 CVSS、KEV 状态、暴露程度和您的环境相结合。
总结
Lean 4 内核不会验证投影表达式中指定的结构是否与被投影值的类型匹配，并且 `src/kernel/inductive.cpp` 中的 `environment::add_inductive` 未对由辅助类型替换的嵌套归纳应用进行类型检查，因此其参数化实参逃逸了检查。在 Lean 进程中运行的元程序可以注册一个类型错误的嵌套归纳，其构造器将 `.proj C 0` 投影应用于无关类型 `W` 的值，而内核在最大内核检查级别下通过普通的 checked addDecl 路径接受该声明，无需 `sorry`、`unsafeCast`、`debug.skipKernelTC`、`addDeclWithoutChecking`、`FFI` 或修改过的 `.olean` 文件。结果是产生类型混淆，得到一个不携带任何公理的 `False` 证明，由此可以推导出任何命题。已发布的概念验证还额外填充两个表达式，直到它们的哈希值和近似深度发生碰撞，从而使内核缓存失效；这是用于触及该缺陷的技术，而非其成因。利用该漏洞需要在进程内运行元程序，例如通过构建项目或导入恶意的 Lake 依赖。
来源
1- lean-cve-pocPoC
CVE-2026-72844 : 利用 Lean 4 内核中的漏洞证明 "0 = 1" 的示例
负责任的使用
仅在您拥有或有权测试的系统上使用漏洞信息。 Kitploit 链接到公共研究元数据，并且不存储漏洞代码或恶意负载。