CVE-2020-37268
中已发布
Coq 与 Rocq Prover 的 Print Assumptions 会遗漏通过 Parameter Inline 内联的不安全宇宙检查
- 已发布
- 2026年8月24日
- 已更新
- 2026年10月26日
- 分配 CNA
- VulnCheck
- 观察到的证据
- 2026年10月26日
初级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 天
- 百分位
- 7.1%
- 型号日期
- 2026年10月27日
EPSS 是统计估计，而不是确定性或影响衡量标准。将其与 CVSS、KEV 状态、暴露程度和您的环境相结合。
总结
Print Assumptions 不会报告某个定义是在禁用宇宙检查的情况下生成的，当该定义通过模块类型中的 Parameter Inline 到达调用方时。应用函子会内联参数的主体，而内联过程丢弃了该术语是在 Unset Universe Checking 下构建的记录，因此生成的常量不携带任何不安全操作的痕迹。因此，一个模块实现可以利用宇宙不一致性证明 False，通过内联参数将其暴露出来，并让 Print Assumptions 将该依赖证明报告为在全局上下文中封闭。由于 Print Assumptions 是用于确认某个开发不依赖于任何意外假设的进程内审计工具，以这种方式构建的依赖能够通过该审计，同时证明任意命题。独立检查器 coqchk 确实会拒绝生成的编译文件。该项目将此记录在 dev/doc/critical-bugs.md 的未修复缺陷部分，并在不使用 coqchk 时将风险评级为中等。
来源
CVE-2020-37268 — Rocq/Coq Print Assumptions 通过参数内联省略不安全宇宙检查
负责任的使用
仅在您拥有或有权测试的系统上使用漏洞信息。 Kitploit 链接到公共研究元数据，并且不存储漏洞代码或恶意负载。