CVE-2026-72714
中已发布
Rocq Prover 至 9.2.0 版本在模块关闭后宇宙检查状态不同步
- 已发布
- 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月25日
EPSS 是统计估计，而不是确定性或影响衡量标准。将其与 CVSS、KEV 状态、暴露程度和您的环境相结合。
总结
Rocq Prover 在关闭一个局部禁用了宇宙检查的模块时，不会恢复宇宙图所保存的宇宙检查标志副本。模块内局部的 Unset Universe Checking 预期只持续到模块结束，全局标志会被恢复，但宇宙图保留了自己的副本，该副本仍处于禁用状态。于是两种视图出现分歧：Test Universe Checking 报告检查已启用，而内核继续接受宇宙不一致的项。由于两个宇宙之间的约束不再被强制执行，Hurkens 悖论得以适用，并产生 False 的证明，由此可推出任何命题。模块关闭后，该证明不使用任何公理、插件或不安全特性，Print Assumptions 将其报告为在全局上下文中封闭，因此假设审计和标志查询都无法反映实际的内核状态。目前没有可用的修复。
来源
CVE-2026-72714 — Rocq 宇宙检查在模块关闭后状态失同步
负责任的使用
仅在您拥有或有权测试的系统上使用漏洞信息。 Kitploit 链接到公共研究元数据，并且不存储漏洞代码或恶意负载。