目标达成 感谢每一位支持者 — 我们达成了 100% 目标！

目标: 1000 元 · 已筹: 1359 元

100%
请我们喝杯咖啡

CVE-2026-72705— Rocq Prover 处理逻辑错误漏洞

一分钟漏洞结论

影响对象
rocq-prover rocq
利用判断
尚无明确在野利用证据，仍需结合暴露面评估
建议动作
优先检查厂商安全公告和参考链接中的修复版本；无法立即升级时，限制受影响服务暴露并加强监测。

Rocq Prover是Rocq Prover组织的一个形式化证明辅助软件。 Rocq Prover 9.2.0之前版本存在处理逻辑错误漏洞，该漏洞源于guard checker未跟踪通过fixpoint自身参数进行的高阶递归调用，可能导致类型定义性等价于其自身否定，从而在纯定义性代码中产生False。

CVSS 6.3 · Medium EPSS 0.18% · P7

影响版本矩阵 1

厂商产品 版本范围状态
rocq-prover rocq < 9.2.0 affected
获取后续新漏洞提醒 登录后订阅

一、 漏洞 CVE-2026-72705 基础信息

漏洞信息
对漏洞内容有疑问？看看神龙的深度分析是否有帮助！
查看神龙十问 ↗

尽管我们使用了先进的大模型技术，但其输出仍可能包含不准确或过时的信息。神龙努力确保数据的准确性，但请您根据实际情况进行核实和判断。

Vulnerability Title
Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
来源: CVE Program / CVE List V5
Vulnerability Description
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. 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
Vulnerability Title
Rocq Prover 处理逻辑错误漏洞
来源: 中国国家信息安全漏洞库 CNNVD
Vulnerability Description
Rocq Prover是Rocq Prover组织的一个形式化证明辅助软件。 Rocq Prover 9.2.0之前版本存在处理逻辑错误漏洞，该漏洞源于guard checker未跟踪通过fixpoint自身参数进行的高阶递归调用，可能导致类型定义性等价于其自身否定，从而在纯定义性代码中产生False。
来源: 中国国家信息安全漏洞库 CNNVD
CVSS Information
N/A
来源: 中国国家信息安全漏洞库 CNNVD
Vulnerability Type
N/A
来源: 中国国家信息安全漏洞库 CNNVD

受影响产品

厂商 产品 影响版本 CPE 订阅
rocq-prover rocq 0 ~ 9.2.0 -

二、漏洞 CVE-2026-72705 的公开POC

# POC 描述 源链接 神龙链接
AI 生成 POC 高级

未找到公开 POC。

登录以生成 AI POC

三、漏洞 CVE-2026-72705 的情报信息

请登录查看更多情报信息。

CVE-2026-72705 补丁与修复 (1)

CVE-2026-72705 概念验证 (1)

CVE-2026-72705 新闻报道 (1)

CVE-2026-72705 其他参考 (2)

同批安全公告 · rocq-prover · 2026-08-24 · 共 5 条

CVE-2026-72714 6.3 MEDIUM Rocq Prover 资源管理错误漏洞
CVE-2026-72703 6.3 MEDIUM Rocq Prover 处理逻辑错误漏洞
CVE-2026-72704 6.3 MEDIUM Rocq Prover 处理逻辑错误漏洞
CVE-2020-37268 6.3 MEDIUM Rocq Prover 日志信息泄露漏洞

IV. Related Vulnerabilities

Same product: rocq
Same vendor: rocq-prover
Same weakness: CWE-670

V. Comments for CVE-2026-72705

暂无评论

发表评论