CVE-2026-72714— Rocq Prover 9.2.0 模块关闭后宇宙检查状态不同步漏洞
一分钟漏洞结论
影响对象
rocq-prover rocq
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。
在 Coq 定理证明器中，当关闭一个局部禁用宇宙检查的模块时，宇宙检查标志在宇宙图的副本中未能被正确恢复。理论上，模块内部通过 禁用的宇宙检查行为应仅在该模块作用域内有效，并在模块结束时恢复全局标志；然而，宇宙图（universe graph）维护着自己的宇宙检查标志副本，该副本在模块关闭后仍保持禁用状态。 由此导致两种视图出现不一致： 显示宇宙检查处于启用状态，但内核（kernel）实际上仍接受违背宇宙一致性的项（terms）。由于两个宇宙之间的约束不再被强制执行，Hurkens 悖论可被触发，从而构造出对逻辑假
可能的 ATT&CK 技术 1 AI
T1195 · Supply Chain Compromise
获取后续新漏洞提醒
登录后订阅
一、 漏洞 CVE-2026-72714 基础信息
漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗
尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。
Vulnerability Title
Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
来源: CVE Program / CVE List V5
Vulnerability Description
Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available.
来源: 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 | 0 ~ 9.2.0 | - |
|
二、漏洞 CVE-2026-72714 的公开POC
| # | POC 描述 | 源链接 | 神龙链接 |
|---|
AI 生成 POC
高级
未找到公开 POC。
登录以生成 AI POC三、漏洞 CVE-2026-72714 的情报信息
请登录查看更多情报信息。
CVE-2026-72714 厂商安全公告 (1)
CVE-2026-72714 概念验证 (1)
CVE-2026-72714 其他参考 (2)
同批安全公告 · rocq-prover · 2026-08-24 · 共 5 条
| CVE-2026-72705 | 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 递归树损坏导致信任问题漏洞 |
| CVE-2020-37268 | 6.3 MEDIUM | Coq 和 Rocq 证明器参数内联时省略不安全宇宙检查漏洞 |
IV. Related Vulnerabilities
V. Comments for CVE-2026-72714
暂无评论