CVE-2026-72703— Rocq Prover 8.20至9.2.0 检查器接受非终止定点漏洞
一分钟漏洞结论
影响对象
rocq-prover rocq
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。
在 Rocq Prover 中，守卫检查器（guard checker）将嵌套相互固定点（nested mutual fixpoint）的参数视为一致的（uniform），而未检查该固定点不同主体（body）之间的调用关系。 中的 函数仅检查自递归调用（self-recursive calls）；因此，当没有任何主体调用自身时，该函数会错误地得出结论认为所有参数都是一致的。 若某一参数通过从一个主体到另一个主体的交叉调用（cross-call）而不断增大，则该参数仍保留其从外层固定点继承而来的子项规范（subter
可能的 ATT&CK 技术 1 AI
T1588.001 · Malware
获取后续新漏洞提醒
登录后订阅
一、 漏洞 CVE-2026-72703 基础信息
漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗
尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。
Vulnerability Title
Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
来源: CVE Program / CVE List V5
Vulnerability Description
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
来源: 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.20 ~ 9.2.0 | - |
|
二、漏洞 CVE-2026-72703 的公开POC
| # | POC 描述 | 源链接 | 神龙链接 |
|---|
AI 生成 POC
高级
未找到公开 POC。
登录以生成 AI POC三、漏洞 CVE-2026-72703 的情报信息
请登录查看更多情报信息。
CVE-2026-72703 补丁与修复 (1)
CVE-2026-72703 厂商安全公告 (1)
CVE-2026-72703 新闻报道 (1)
CVE-2026-72703 其他参考 (1)
同批安全公告 · 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-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-72703
暂无评论