CVE-2026-72704— Rocq Prover 9.2.0 递归树损坏导致信任问题漏洞
一分钟漏洞结论
影响对象
rocq-prover rocq
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。
Rocq 证明器中的守卫检查器（guard checker）在通过“传输”（transport）修改了归纳类型参数后，并未重新检查该参数的递归树表示。一个不动点定义（fixpoint）可能沿着类型间的等式，对其递归参数应用重写（rewrite）。守卫检查器之所以接受这种操作，是因为归纳类型本身得以保持，但为该参数记录的递归树却发生了改变。另一个调用前一个不动点的第二个不动点，在未经验证的情况下继承了被篡改的递归树，从而将并非结构上递减（structurally decreasing）的调用误认为是终止的。由此产生的
可能的 ATT&CK 技术 1 AI
T1059 · Command and Scripting Interpreter
获取后续新漏洞提醒
登录后订阅
一、 漏洞 CVE-2026-72704 基础信息
漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗
尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。
Vulnerability Title
Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
来源: CVE Program / CVE List V5
Vulnerability Description
The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.
来源: 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-72704 的公开POC
| # | POC 描述 | 源链接 | 神龙链接 |
|---|
AI 生成 POC
高级
未找到公开 POC。
登录以生成 AI POC三、漏洞 CVE-2026-72704 的情报信息
请登录查看更多情报信息。
CVE-2026-72704 补丁与修复 (1)
CVE-2026-72704 厂商安全公告 (1)
CVE-2026-72704 概念验证 (1)
CVE-2026-72704 其他参考 (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-2020-37268 | 6.3 MEDIUM | Coq 和 Rocq 证明器参数内联时省略不安全宇宙检查漏洞 |
IV. Related Vulnerabilities
V. Comments for CVE-2026-72704
暂无评论