Goal Reached Thanks to every supporter — we hit 100%!

Goal: 1000 CNY · Raised: 1336 CNY

100%
Buy Us a Coffee

CVE-2026-72705— Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument

Quick assessment

Affected
rocq-prover rocq
Exploitation
No confirmed in-the-wild exploitation; assess based on exposure
Recommended action
Check the vendor advisory and references for a fixed version. If immediate upgrade is impossible, restrict exposure and increase monitoring.

在 Rocq Prover 中，守卫检查器未跟踪通过不动点（fixpoint）自身参数进行的递归调用。一个不动点可能将其自身作为高阶参数传递给另一个不动点，而后者会将其应用于某个值，该值并非结构参数的子项。当递归函数被传递给普通定义时，由于检查器会展开该定义并观察到调用行为，因此此类情况会被拒绝；然而，当递归函数被传递给另一个不动点时，由于未跟踪通过不动点参数进行的高阶递归调用，此类情况会被接受。 此漏洞允许构造一个类型，该类型在定义上等同于其自身的否定，因此纯定义式代码（无需使用策略、公理、插件或不安全标志）中的

CVSS 6.3 · Medium EPSS 0.12% · P2

Possible ATT&CK Techniques 1 AI

T1190 · Exploit Public-Facing Application

Affected Version Matrix 1

VendorProduct Version RangeStatus
rocq-prover rocq < 9.2.0 affected
Get alerts for future matching vulnerabilities Log in to subscribe

I. Basic Information for CVE-2026-72705

Vulnerability Information
Have questions about the vulnerability? See if Shenlong's analysis helps!
View Shenlong Deep Dive ↗

Although we use advanced large model technology, its output may still contain inaccurate or outdated information.Shenlong tries to ensure data accuracy, but please verify and judge based on the actual situation.

Vulnerability Title
Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
Source: 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.
Source: 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
Source: CVE Program / CVE List V5
Vulnerability Type
控制流实现总是不正确
Source: CVE Program / CVE List V5

Affected Products

Vendor Product Affected Versions CPE Subscribe
rocq-prover rocq 0 ~ 9.2.0 -

II. Public POCs for CVE-2026-72705

# POC Description Source Link Shenlong Link
AI-Generated POC Premium

No public POC found.

Login to generate AI POC

III. Intelligence Information for CVE-2026-72705

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

Patches & Fixes for CVE-2026-72705 (1)

Proof of Concept for CVE-2026-72705 (1)

News Coverage for CVE-2026-72705 (1)

Other References for CVE-2026-72705 (2)

Same Patch Batch · rocq-prover · 2026-08-24 · 5 CVEs total

CVE-2026-72714 6.3 MEDIUM Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
CVE-2026-72703 6.3 MEDIUM Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked
CVE-2026-72704 6.3 MEDIUM Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
CVE-2020-37268 6.3 MEDIUM Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Param

IV. Related Vulnerabilities

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

V. Comments for CVE-2026-72705

No comments yet

Leave a comment