Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
Summary
| CVE | CVE-2026-72704 |
|---|---|
| State | PUBLISHED |
| Assigner | VulnCheck |
| Source Priority | CVE Program / NVD first with legacy fallback |
| Published | 2026-08-24 20:17:18 UTC |
| Updated | 2026-08-24 20:17:18 UTC |
| 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. |
Risk And Classification
Primary CVSS: v4.0 6.8 MEDIUM from [email protected]
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:X
Problem Types: CWE-670 | CWE-670 Always-Incorrect Control Flow Implementation
| Version | Source | Type | Score | Severity | Vector |
|---|---|---|---|---|---|
| 4.0 | [email protected] | Secondary | 6.8 | MEDIUM | 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/C... |
| 4.0 | CNA | CVSS | 6.8 | MEDIUM | 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 |
| 3.1 | [email protected] | Primary | 6.3 | MEDIUM | CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N |
| 3.1 | CNA | CVSS | 6.3 | MEDIUM | CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N |
CVSS v4.0 Breakdown
Attack Vector
LocalAttack Complexity
LowAttack Requirements
NonePrivileges Required
NoneUser Interaction
PassiveConfidentiality
NoneIntegrity
HighAvailability
NoneSub Conf.
NoneSub Integrity
NoneSub Availability
NoneCVSS: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:X
CVSS v3.1 Breakdown
Attack Vector
LocalAttack Complexity
LowPrivileges Required
NoneUser Interaction
RequiredScope
ChangedConfidentiality
NoneIntegrity
HighAvailability
NoneCVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
Vendor Declared Affected Products
| Source | Vendor | Product | Version | Platforms |
|---|---|---|---|---|
| CNA | Rocq-prover | Rocq | affected 9.2.0 custom | Not specified |
References
| Reference | Source | Link | Tags |
|---|---|---|---|
| github.com/endrazine/rocq-cve-poc-22024 | [email protected] | github.com | |
| github.com/rocq-prover/rocq | [email protected] | github.com | |
| github.com/rocq-prover/rocq/pull/22027 | [email protected] | github.com | |
| www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trusts-corrupted... | [email protected] | www.vulncheck.com | |
| github.com/rocq-prover/rocq/issues/22024 | [email protected] | github.com | |
| CVE Program record | CVE.ORG | www.cve.org | canonical |
| NVD vulnerability detail | NVD | nvd.nist.gov | canonical, analysis |
Vendor Comments And Credit
Discovery Credit
CNA: Yann Leray (en)
CNA: Jonathan Brossard (MOABI) (en)
There are currently no legacy QID mappings associated with this CVE.