CVE-2020-37268— Coq 和 Rocq 证明器参数内联时省略不安全宇宙检查漏洞
一分钟漏洞结论
影响对象
rocq-prover rocq
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。
未报告在禁用宇宙检查（universe checking）时产生的定义，因为该定义通过模块类型（module type）中的参数内联（Parameter Inline）传递给了调用方。当对 functor 进行应用时，参数的主体会被内联，且内联过程会丢弃“该项是在关闭宇宙检查的情况下构建的”这一记录，导致生成的常量不再带有执行不安全操作的痕迹。因此，模块实现可以利用宇宙不一致性（universe inconsistency）证明 ，并通过内联的参数将其暴露出来，使 将该依赖证明报告为在全局上下文下的闭合证明。由于
可能的 ATT&CK 技术 1 AI
T1190 · Exploit Public-Facing Application
获取后续新漏洞提醒
登录后订阅
一、 漏洞 CVE-2020-37268 基础信息
漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗
尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。
Vulnerability Title
Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Parameter Inline
来源: CVE Program / CVE List V5
Vulnerability Description
Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built under Unset Universe Checking, so the resulting constant carries no trace of the unsafe operation. A module implementation can therefore prove False using a universe inconsistency, expose it through an inlined parameter, and have Print Assumptions report the dependent proof as closed under the global context. Because Print Assumptions is the in-process audit used to confirm that a development rests on no unexpected assumptions, a dependency built this way passes that audit while proving arbitrary propositions. The standalone checker coqchk does reject the resulting compiled file. The project records this in dev/doc/critical-bugs.md under non-fixed bugs and rates the risk as moderate when coqchk is not used.
来源: 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 | 订阅 |
|---|---|---|---|---|
| rocq-prover | rocq | 8.11 ~ 9.2.0 | - |
|
二、漏洞 CVE-2020-37268 的公开POC
| # | POC 描述 | 源链接 | 神龙链接 |
|---|
AI 生成 POC
高级
未找到公开 POC。
登录以生成 AI POC三、漏洞 CVE-2020-37268 的情报信息
请登录查看更多情报信息。
CVE-2020-37268 厂商安全公告 (1)
CVE-2020-37268 概念验证 (1)
CVE-2020-37268 其他参考 (2)
同批安全公告 · rocq-prover · 2026-08-24 · 共 5 条
| CVE-2026-72705 | 6.3 MEDIUM | Rocq Prover 9.2.0前版本高阶参数传递漏洞 |
| CVE-2026-72714 | 6.3 MEDIUM | Rocq Prover 9.2.0 模块关闭后宇宙检查状态不同步漏洞 |
| CVE-2026-72703 | 6.3 MEDIUM | Rocq Prover 8.20至9.2.0 检查器接受非终止定点漏洞 |
| CVE-2026-72704 | 6.3 MEDIUM | Rocq Prover 9.2.0 递归树损坏导致信任问题漏洞 |
IV. Related Vulnerabilities
V. Comments for CVE-2020-37268
暂无评论