CVE-2026-72705
中已发布
Rocq Prover 9.2.0 之前版本的 Guard Checker 接受作为高阶参数传递的 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月27日
EPSS 是统计估计，而不是确定性或影响衡量标准。将其与 CVSS、KEV 状态、暴露程度和您的环境相结合。
总结
Rocq Prover 中的守卫检查器不会追踪通过不动点自身参数进行的递归调用。一个不动点可以将自身作为高阶参数传递给第二个不动点，后者再将其应用于一个并非结构参数子项的值。将递归函数传递给普通定义会被拒绝，因为检查器会展开该定义并观察到该调用，但将其传递给不动点则会被接受，因为通过不动点参数进行的高阶递归调用未被追踪。这引入了一个在定义上等于其自身否定的类型，因此自应用会在纯定义性代码中产生 False，无需策略、公理、插件或不安全标志，并且 Print Assumptions 会将结果报告为在全局上下文中封闭。已在 Rocq 9.2.0 中修复。
来源
CVE-2026-72705 — Rocq Guard Checker 接受作为高阶参数传入的 Fixpoint
负责任的使用
仅在您拥有或有权测试的系统上使用漏洞信息。 Kitploit 链接到公共研究元数据，并且不存储漏洞代码或恶意负载。