CVE-2026-72844— Lean 4 内核类型检查绕过漏洞
一分钟漏洞结论
影响对象
leanprover lean4
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。
Lean 4 内核未验证投影表达式中所指明的结构是否与被投影值的类型相匹配。此外， 中的 函数在对由辅助类型替换的嵌套归纳类型应用进行类型检查时存在疏漏，导致其参数化参数绕过了类型检查。 在 Lean 进程内运行的元程序可以注册一个类型不良的嵌套归纳类型，其构造函数会将一个属于不相关类型 W 的值通过 投影进行访问。内核通过标准的 路径（该路径在最大程度的内核检查下运行）接受此声明，整个过程无需使用 、 、 、 、FFI，也不需要修改 文件。 该漏洞导致类型混淆，进而生成一个无需引入公理（axioms）即可证明 的
可能的 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
受影响产品
| 厂商 | 产品 | 影响版本 | 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 vendor: leanprover
V. Comments for CVE-2026-72844
暂无评论