目标达成 感谢每一位支持者 — 我们达成了 100% 目标！

目标: 1000 元 · 已筹: 1336 元

100%
请我们喝杯咖啡

CVE-2026-72711— Lean 4 <4.32.2 内核接受带有未绑定自由变量的不透明声明

一分钟漏洞结论

影响对象
leanprover lean4
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。

Lean 4 内核未检查不透明声明（opaque declaration）的主体是否已闭合（closed）。 跳过了 和 路径中所执行的 检查，因此，若一个值包含自由变量（free variable）但该变量不在局部上下文（local context）中，内核不会直接拒绝它。 元程序（metaprogram）可以首先导致内核创建一个类型为 的临时局部变量，并将其类型记录在类型检查器的推理缓存（inference cache）中；随后，在该缓存条目仍驻留在同一类型检查器实例上期间，恢复局部上下文；最后提交一个不透明声

CVSS 6.3 · Medium EPSS 0.12% · P2

影响版本矩阵 1

厂商产品 版本范围状态
leanprover lean4 < 4.32.2 affected
获取后续新漏洞提醒 登录后订阅

一、 漏洞 CVE-2026-72711 基础信息

漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗

尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。

Vulnerability Title
Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable
来源: CVE Program / CVE List V5
Vulnerability Description
The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.
来源: 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-72711 的公开POC

# POC 描述 源链接 神龙链接
AI 生成 POC 高级

未找到公开 POC。

登录以生成 AI POC

三、漏洞 CVE-2026-72711 的情报信息

请登录查看更多情报信息。

CVE-2026-72711 补丁与修复 (1)

CVE-2026-72711 厂商安全公告 (1)

CVE-2026-72711 概念验证 (2)

IV. Related Vulnerabilities

Same product: lean4
Same vendor: leanprover
Same weakness: CWE-20

V. Comments for CVE-2026-72711

暂无评论

发表评论