CVE-2026-72703
中已发布
Rocq Prover 8.20 至 9.2.0 之前版本：Guard 检查器通过未检查的交叉调用接受非终止 Fixpoint
- 已发布
- 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 中的 guard checker 在检查嵌套互递归 fixpoint 的参数时，会将该参数视为 uniform，而不检查该 fixpoint 不同函数体之间的调用。kernel/inductive.ml 中的 find_uniform_parameters 只检查自递归调用，因此当没有任何函数体调用自身时，该函数便断定所有参数都是 uniform。于是，某个参数若通过从一个函数体到另一个函数体的交叉调用而增长，就会保留其从外层 fixpoint 继承而来的 subterm 规范，而受该规范保护的递归调用即使实参在结构上并未变小也会被接受。一个非终止的定义被当作结构递减而接纳，从而产生一个其值等于自身后继的项，进而得到 False 的证明，由此可推出任何命题。该证明不需要公理、插件或不安全标志，Print Assumptions 报告其在全局上下文中是封闭的。该问题在 Coq 8.20 中引入，并在 Rocq 9.2.0 中修复。
来源
CVE-2026-72703 — Rocq Guard Checker 通过未检查的交叉调用接受非终止 Fixpoint
负责任的使用
仅在您拥有或有权测试的系统上使用漏洞信息。 Kitploit 链接到公共研究元数据，并且不存储漏洞代码或恶意负载。