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

Goal: 1000 CNY · Raised: 1336 CNY

100%
Buy Us a Coffee

CVE-2026-72704— Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport

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 证明器中的守卫检查器（guard checker）在通过“传输”（transport）修改了归纳类型参数后，并未重新检查该参数的递归树表示。一个不动点定义（fixpoint）可能沿着类型间的等式，对其递归参数应用重写（rewrite）。守卫检查器之所以接受这种操作，是因为归纳类型本身得以保持，但为该参数记录的递归树却发生了改变。另一个调用前一个不动点的第二个不动点，在未经验证的情况下继承了被篡改的递归树，从而将并非结构上递减（structurally decreasing）的调用误认为是终止的。由此产生的

CVSS 6.3 · Medium EPSS 0.12% · P2

Possible ATT&CK Techniques 1 AI

T1059 · Command and Scripting Interpreter

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-72704

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 through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
Source: 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.
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-72704

# 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-72704

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

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

Vendor Advisories for CVE-2026-72704 (1)

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

Other References for CVE-2026-72704 (2)

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

CVE-2026-72705 6.3 MEDIUM Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
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-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-72704

No comments yet

Leave a comment