CVE-2026-72844— Lean 4 缓冲区错误漏洞
一分钟漏洞结论
影响对象
leanprover lean4
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。
Lean 4是Lean组织的一个交互式定理证明与函数式编程框架。 Lean 4 4.32.2之前版本和4.33.0-rc1版本存在缓冲区错误漏洞，该漏洞源于内核未验证投影表达式中的结构类型与值类型匹配，且environment::add_inductive未对嵌套归纳应用进行类型检查，可能导致类型混淆，进而产生无公理False证明并推导出任意命题。
可能的 ATT&CK 技术 1 AI
T1195 · Supply Chain Compromise影响版本矩阵 3
| 厂商 | 产品 | 版本范围 | 状态 |
|---|---|---|---|
| leanprover | lean4 | < 4.32.2 |
affected |
4.32.2 |
unaffected | ||
4.33.0-rc1 |
affected |
获取后续新漏洞提醒
登录后订阅
一、 漏洞 CVE-2026-72844 基础信息
漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗
尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。
Vulnerability Title
Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
来源: CVE Program / CVE List V5
Vulnerability Description
The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
来源: CVE Program / CVE List V5
CVSS Information
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
来源: CVE Program / CVE List V5
Vulnerability Type
使用不兼容类型访问资源(类型混淆)
来源: CVE Program / CVE List V5
Vulnerability Title
Lean 4 缓冲区错误漏洞
来源: 中国国家信息安全漏洞库 CNNVD
Vulnerability Description
Lean 4是Lean组织的一个交互式定理证明与函数式编程框架。 Lean 4 4.32.2之前版本和4.33.0-rc1版本存在缓冲区错误漏洞，该漏洞源于内核未验证投影表达式中的结构类型与值类型匹配，且environment::add_inductive未对嵌套归纳应用进行类型检查，可能导致类型混淆，进而产生无公理False证明并推导出任意命题。
来源: 中国国家信息安全漏洞库 CNNVD
CVSS Information
N/A
来源: 中国国家信息安全漏洞库 CNNVD
Vulnerability Type
N/A
来源: 中国国家信息安全漏洞库 CNNVD
受影响产品
| 厂商 | 产品 | 影响版本 | CPE | 订阅 |
|---|---|---|---|---|
| leanprover | lean4 | 0 ~ 4.32.2 | - |
|
二、漏洞 CVE-2026-72844 的公开POC
| # | POC 描述 | 源链接 | 神龙链接 |
|---|
AI 生成 POC
高级
未找到公开 POC。
登录以生成 AI POC三、漏洞 CVE-2026-72844 的情报信息
请登录查看更多情报信息。
CVE-2026-72844 补丁与修复 (2)
CVE-2026-72844 厂商安全公告 (1)
CVE-2026-72844 概念验证 (2)
CVE-2026-72844 邮件列表归档 (1)
CVE-2026-72844 其他参考 (1)
IV. Related Vulnerabilities
Same product: lean4
V. Comments for CVE-2026-72844
暂无评论