CVE-2026-72704
Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
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.
INFO
Published Date :
Aug. 24, 2026, 8:17 p.m.
Last Modified :
Oct. 26, 2026, 2:17 a.m.
Remotely Exploit :
No
Source :
[email protected]
CVSS Scores
| Score | Version | Severity | Vector | Exploitability Score | Impact Score | Source |
|---|---|---|---|---|---|---|
| CVSS | 134c704f-9b21-4f2e-91b3-4a467353bcc0 | |||||
| CVSS 3.1 | MEDIUM | 83251b91-4cc7-4094-a5c7-464a1b83ea10 | ||||
| CVSS 3.1 | MEDIUM | [email protected] | ||||
| CVSS 3.1 | MEDIUM | MITRE-CVE | ||||
| CVSS 4.0 | MEDIUM | 83251b91-4cc7-4094-a5c7-464a1b83ea10 | ||||
| CVSS 4.0 | MEDIUM | [email protected] |
Solution
- Apply the proposed fix to the guard checker.
- Verify recursive trees after type parameter changes.
- Ensure fixpoints correctly validate recursive structures.
References to Advisories, Solutions, and Tools
Here, you will find a curated list of external links that provide in-depth
information, practical solutions, and valuable tools related to
CVE-2026-72704.
CWE - Common Weakness Enumeration
While CVE identifies
specific instances of vulnerabilities, CWE categorizes the common flaws or
weaknesses that can lead to vulnerabilities. CVE-2026-72704 is
associated with the following CWEs:
Common Attack Pattern Enumeration and Classification (CAPEC)
Common Attack Pattern Enumeration and Classification
(CAPEC)
stores attack patterns, which are descriptions of the common attributes and
approaches employed by adversaries to exploit the CVE-2026-72704
weaknesses.
We scan GitHub repositories to detect new proof-of-concept exploits. Following list is a collection of public exploits and proof-of-concepts, which have been published on GitHub (sorted by the most recently updated).
Results are limited to the first 15 repositories due to potential performance issues.
The following list is the news that have been mention
CVE-2026-72704 vulnerability anywhere in the article.
The following table lists the changes that have been made to the
CVE-2026-72704 vulnerability over time.
Vulnerability history details can be useful for understanding the evolution of a vulnerability, and for identifying the most recent changes that may impact the vulnerability's severity, exploitability, or other characteristics.
-
CVE Modified by [email protected]
Oct. 26, 2026
Action Type Old Value New Value Added Reference https://github.com/endrazine/rocq-cve-poc-22024 Added Reference https://github.com/rocq-prover/rocq Added Reference https://github.com/rocq-prover/rocq/issues/22024 Added Reference https://github.com/rocq-prover/rocq/pull/22027 Added Reference https://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trusts-corrupted-recursive-tree-after-transport Removed Reference https://github.com/endrazine/rocq-cve-poc-22024 Removed Reference https://github.com/rocq-prover/rocq Removed Reference https://github.com/rocq-prover/rocq/issues/22024 Removed Reference https://github.com/rocq-prover/rocq/pull/22027 Removed Reference https://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trusts-corrupted-recursive-tree-after-transport -
CVE Modified by af854a3a-2127-422b-91ae-364da2661108
Oct. 26, 2026
Action Type Old Value New Value Added Reference http://www.openwall.com/lists/oss-security/2026/10/26/5 -
CVE Translated by [email protected]
Oct. 12, 2026
Action Type Old Value New Value Added Translation Title: Rocq de Rocq Prover, Description: El verificador de guardas en Rocq Prover no vuelve a verificar la representación en árbol recursivo de un parámetro de tipo inductivo después de que ese parámetro haya sido modificado por transporte. Un punto fijo puede aplicar una reescritura a lo largo de una igualdad entre tipos a su argumento recursivo, lo cual el verificador de guardas acepta porque el tipo inductivo se preserva, mientras que el árbol recursivo registrado para el parámetro es alterado. Un segundo punto fijo que llama al primero hereda el árbol recursivo alterado sin verificación, por lo que una llamada que no es estructuralmente decreciente es aceptada como terminante. La definición no terminante resultante prueba que un número natural es igual a su propio sucesor y por lo tanto Falso, de lo cual se sigue cualquier proposición. La demostración utiliza dos axiomas que se derivan de la univalencia y son consistentes con el cálculo de construcciones inductivas, por lo que la contradicción proviene del verificador de guardas en lugar de las suposiciones. Se propone una solución pero no se ha fusionado. -
CVE Modified by 134c704f-9b21-4f2e-91b3-4a467353bcc0
Aug. 25, 2026
Action Type Old Value New Value Added SSVC {'id': 'CVE-2026-72704', 'role': 'CISA Coordinator', 'options': [{'exploitation': 'poc'}, {'automatable': 'no'}, {'technicalImpact': 'partial'}], 'version': '2.0.3', 'timestamp': '2026-08-25T16:37:22.786826Z'} -
New CVE Received by [email protected]
Aug. 24, 2026
Action Type Old Value New Value Added Affected [{'repo': 'https://github.com/rocq-prover/rocq', 'vendor': 'rocq-prover', 'product': 'rocq', 'versions': [{'status': 'affected', 'version': '0', 'versionType': 'custom', 'lessThanOrEqual': '9.2.0'}], 'packageURL': 'pkg:github/rocq-prover/rocq', 'defaultStatus': 'unaffected'}] Added 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. Added CVSS V4.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 Added CVSS V3.1 AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N Added CWE CWE-670 Added Reference https://github.com/endrazine/rocq-cve-poc-22024 Added Reference https://github.com/rocq-prover/rocq Added Reference https://github.com/rocq-prover/rocq/issues/22024 Added Reference https://github.com/rocq-prover/rocq/pull/22027 Added Reference https://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trusts-corrupted-recursive-tree-after-transport