CVE-2026-72703 (GCVE-0-2026-72703)
Vulnerability from cvelistv5 – Published: 2026-08-24 20:08 – Updated: 2026-10-26 01:23- CWE-670 - Always-Incorrect Control Flow Implementation
| URL | Tags |
|---|---|
| https://github.com/rocq-prover/rocq | product |
| https://github.com/rocq-prover/rocq/issues/21682 | issue-tracking |
| https://github.com/rocq-prover/rocq/pull/21684 | issue-trackingpatch |
| https://github.com/endrazine/rocq-cve-poc-21682 | exploit |
| https://www.vulncheck.com/advisories/rocq-prover-… | third-party-advisory |
| http://www.openwall.com/lists/oss-security/2026/10/26/4 |
| Vendor | Product | Version | CPE status | |
|---|---|---|---|---|
| rocq-prover | rocq |
Affected:
8.20 , < 9.2.0
(custom)
|
guessed |
{
"containers": {
"adp": [
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2026-72703",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-27T14:12:25.906004Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2026-08-27T14:12:34.453Z",
"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"shortName": "CISA-ADP"
},
"title": "CISA ADP Vulnrichment"
},
{
"providerMetadata": {
"dateUpdated": "2026-10-26T01:23:54.511Z",
"orgId": "af854a3a-2127-422b-91ae-364da2661108",
"shortName": "CVE"
},
"references": [
{
"url": "http://www.openwall.com/lists/oss-security/2026/10/26/4"
}
],
"title": "CVE Program Container"
}
],
"cna": {
"affected": [
{
"defaultStatus": "unaffected",
"packageURL": "pkg:github/rocq-prover/rocq",
"product": "rocq",
"repo": "https://github.com/rocq-prover/rocq",
"vendor": "rocq-prover",
"versions": [
{
"lessThan": "9.2.0",
"status": "affected",
"version": "8.20",
"versionType": "custom"
}
]
}
],
"credits": [
{
"lang": "en",
"type": "finder",
"value": "Tristan St\u00e9rin"
},
{
"lang": "en",
"type": "finder",
"value": "Jonathan Brossard (MOABI)"
}
],
"datePublic": "2026-02-28T00:00:00.000Z",
"descriptions": [
{
"lang": "en",
"value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
}
],
"metrics": [
{
"cvssV4_0": {
"attackComplexity": "LOW",
"attackRequirements": "NONE",
"attackVector": "LOCAL",
"baseScore": 6.8,
"baseSeverity": "MEDIUM",
"privilegesRequired": "NONE",
"subAvailabilityImpact": "NONE",
"subConfidentialityImpact": "NONE",
"subIntegrityImpact": "NONE",
"userInteraction": "PASSIVE",
"vectorString": "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",
"version": "4.0",
"vulnAvailabilityImpact": "NONE",
"vulnConfidentialityImpact": "NONE",
"vulnIntegrityImpact": "HIGH"
},
"format": "CVSS"
},
{
"cvssV3_1": {
"attackComplexity": "LOW",
"attackVector": "LOCAL",
"availabilityImpact": "NONE",
"baseScore": 6.3,
"baseSeverity": "MEDIUM",
"confidentialityImpact": "NONE",
"integrityImpact": "HIGH",
"privilegesRequired": "NONE",
"scope": "CHANGED",
"userInteraction": "REQUIRED",
"vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
"version": "3.1"
},
"format": "CVSS"
}
],
"problemTypes": [
{
"descriptions": [
{
"cweId": "CWE-670",
"description": "Always-Incorrect Control Flow Implementation",
"lang": "en",
"type": "CWE"
}
]
}
],
"providerMetadata": {
"dateUpdated": "2026-09-24T14:18:50.897Z",
"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"shortName": "VulnCheck"
},
"references": [
{
"tags": [
"product"
],
"url": "https://github.com/rocq-prover/rocq"
},
{
"tags": [
"issue-tracking"
],
"url": "https://github.com/rocq-prover/rocq/issues/21682"
},
{
"tags": [
"issue-tracking",
"patch"
],
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"tags": [
"exploit"
],
"url": "https://github.com/endrazine/rocq-cve-poc-21682"
},
{
"name": "VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"tags": [
"third-party-advisory"
],
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"
}
],
"title": "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"x_generator": {
"engine": "vulncheck-endgame"
}
}
},
"cveMetadata": {
"assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"assignerShortName": "VulnCheck",
"cveId": "CVE-2026-72703",
"datePublished": "2026-08-24T20:08:30.607Z",
"dateReserved": "2026-08-10T13:02:20.829Z",
"dateUpdated": "2026-10-26T01:23:54.511Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.2",
"vulnerability-lookup:meta": {
"epss": {
"cve": "CVE-2026-72703",
"date": "2026-11-08",
"epss": "0.00176",
"percentile": "0.07142"
},
"nvd": {
"cve": {
"affected": [
{
"affectedData": [
{
"defaultStatus": "unaffected",
"packageURL": "pkg:github/rocq-prover/rocq",
"product": "rocq",
"repo": "https://github.com/rocq-prover/rocq",
"vendor": "rocq-prover",
"versions": [
{
"lessThan": "9.2.0",
"status": "affected",
"version": "8.20",
"versionType": "custom"
}
]
}
],
"source": "disclosure@vulncheck.com"
}
],
"cveTags": [],
"descriptions": [
{
"lang": "en",
"value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
},
{
"lang": "es",
"value": "El verificador de guardas en Rocq Prover trata un par\u00e1metro de un punto fijo mutuo anidado como uniforme sin examinar las llamadas entre los diferentes cuerpos de ese punto fijo. find_uniform_parameters en kernel/inductive.ml inspecciona solo las llamadas autorrecursivas, por lo que cuando ning\u00fan cuerpo se llama a s\u00ed mismo, la funci\u00f3n concluye que cada par\u00e1metro es uniforme. Un par\u00e1metro que crece a trav\u00e9s de una llamada cruzada de un cuerpo a otro, por lo tanto, mantiene la especificaci\u00f3n de subt\u00e9rmino que hered\u00f3 del punto fijo envolvente, y una llamada recursiva protegida por esa especificaci\u00f3n es aceptada aunque el argumento no sea estructuralmente menor. Una definici\u00f3n no terminante es admitida como estructuralmente decreciente, lo que produce un t\u00e9rmino cuyo valor es igual a su propio sucesor y, por lo tanto, una prueba de Falso, de la cual se deduce cualquier proposici\u00f3n. La prueba no requiere axiomas, plugins o banderas inseguras y Print Assumptions lo reporta como cerrado bajo el contexto global. Introducido en Coq 8.20 y corregido en Rocq 9.2.0."
}
],
"id": "CVE-2026-72703",
"lastModified": "2026-10-26T02:17:07.063",
"metrics": {
"cvssMetricV31": [
{
"cvssData": {
"attackComplexity": "LOW",
"attackVector": "LOCAL",
"availabilityImpact": "NONE",
"baseScore": 6.3,
"baseSeverity": "MEDIUM",
"confidentialityImpact": "NONE",
"integrityImpact": "HIGH",
"privilegesRequired": "NONE",
"scope": "CHANGED",
"userInteraction": "REQUIRED",
"vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
"version": "3.1"
},
"exploitabilityScore": 1.8,
"impactScore": 4.0,
"source": "disclosure@vulncheck.com",
"type": "Secondary"
}
],
"cvssMetricV40": [
{
"cvssData": {
"Automatable": "NOT_DEFINED",
"Recovery": "NOT_DEFINED",
"Safety": "NOT_DEFINED",
"attackComplexity": "LOW",
"attackRequirements": "NONE",
"attackVector": "LOCAL",
"availabilityRequirement": "NOT_DEFINED",
"baseScore": 6.8,
"baseSeverity": "MEDIUM",
"confidentialityRequirement": "NOT_DEFINED",
"exploitMaturity": "NOT_DEFINED",
"integrityRequirement": "NOT_DEFINED",
"modifiedAttackComplexity": "NOT_DEFINED",
"modifiedAttackRequirements": "NOT_DEFINED",
"modifiedAttackVector": "NOT_DEFINED",
"modifiedPrivilegesRequired": "NOT_DEFINED",
"modifiedSubAvailabilityImpact": "NOT_DEFINED",
"modifiedSubConfidentialityImpact": "NOT_DEFINED",
"modifiedSubIntegrityImpact": "NOT_DEFINED",
"modifiedUserInteraction": "NOT_DEFINED",
"modifiedVulnAvailabilityImpact": "NOT_DEFINED",
"modifiedVulnConfidentialityImpact": "NOT_DEFINED",
"modifiedVulnIntegrityImpact": "NOT_DEFINED",
"privilegesRequired": "NONE",
"providerUrgency": "NOT_DEFINED",
"subAvailabilityImpact": "NONE",
"subConfidentialityImpact": "NONE",
"subIntegrityImpact": "NONE",
"userInteraction": "PASSIVE",
"valueDensity": "NOT_DEFINED",
"vectorString": "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",
"version": "4.0",
"vulnAvailabilityImpact": "NONE",
"vulnConfidentialityImpact": "NONE",
"vulnIntegrityImpact": "HIGH",
"vulnerabilityResponseEffort": "NOT_DEFINED"
},
"source": "disclosure@vulncheck.com",
"type": "Secondary"
}
],
"ssvcV203": [
{
"source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"ssvcData": {
"id": "CVE-2026-72703",
"options": [
{
"exploitation": "poc"
},
{
"automatable": "no"
},
{
"technicalImpact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-27T14:12:25.906004Z",
"version": "2.0.3"
}
}
]
},
"published": "2026-08-24T20:17:18.240",
"references": [
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/endrazine/rocq-cve-poc-21682"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/rocq-prover/rocq"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/rocq-prover/rocq/issues/21682"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"source": "disclosure@vulncheck.com",
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"
},
{
"source": "af854a3a-2127-422b-91ae-364da2661108",
"url": "http://www.openwall.com/lists/oss-security/2026/10/26/4"
}
],
"sourceIdentifier": "disclosure@vulncheck.com",
"vulnStatus": "Deferred",
"weaknesses": [
{
"description": [
{
"lang": "en",
"value": "CWE-670"
}
],
"source": "disclosure@vulncheck.com",
"type": "Secondary"
}
]
}
},
"redhat_vex": {
"current_release_date": "2026-08-24T21:18:43+00:00",
"cve": "CVE-2026-72703",
"id": "CVE-2026-72703",
"initial_release_date": "2026-08-24T20:08:30.607000+00:00",
"product_status:known_not_affected": "1",
"source": "Red Hat CSAF VEX",
"status": "final",
"title": "rocq: Rocq Prover: Logical Flaw Allows Arbitrary Proof Generation via Unchecked Cross-Calls",
"url": "https://security.access.redhat.com/data/csaf/v2/vex/2026/cve-2026-72703.json",
"version": "3"
},
"vulnrichment": {
"containers": {
"adp": [
{
"providerMetadata": {
"dateUpdated": "2026-10-26T01:23:54.511Z",
"orgId": "af854a3a-2127-422b-91ae-364da2661108",
"shortName": "CVE"
},
"references": [
{
"url": "http://www.openwall.com/lists/oss-security/2026/10/26/4"
}
],
"title": "CVE Program Container"
},
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2026-72703",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-27T14:12:25.906004Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2026-08-27T14:12:30.905Z",
"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
"shortName": "CISA-ADP"
},
"title": "CISA ADP Vulnrichment"
}
],
"cna": {
"affected": [
{
"defaultStatus": "unaffected",
"packageURL": "pkg:github/rocq-prover/rocq",
"product": "rocq",
"repo": "https://github.com/rocq-prover/rocq",
"vendor": "rocq-prover",
"versions": [
{
"lessThan": "9.2.0",
"status": "affected",
"version": "8.20",
"versionType": "custom"
}
]
}
],
"credits": [
{
"lang": "en",
"type": "finder",
"value": "Tristan St\u00e9rin"
},
{
"lang": "en",
"type": "finder",
"value": "Jonathan Brossard (MOABI)"
}
],
"datePublic": "2026-02-28T00:00:00.000Z",
"descriptions": [
{
"lang": "en",
"value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
}
],
"metrics": [
{
"cvssV4_0": {
"attackComplexity": "LOW",
"attackRequirements": "NONE",
"attackVector": "LOCAL",
"baseScore": 6.8,
"baseSeverity": "MEDIUM",
"privilegesRequired": "NONE",
"subAvailabilityImpact": "NONE",
"subConfidentialityImpact": "NONE",
"subIntegrityImpact": "NONE",
"userInteraction": "PASSIVE",
"vectorString": "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",
"version": "4.0",
"vulnAvailabilityImpact": "NONE",
"vulnConfidentialityImpact": "NONE",
"vulnIntegrityImpact": "HIGH"
},
"format": "CVSS"
},
{
"cvssV3_1": {
"attackComplexity": "LOW",
"attackVector": "LOCAL",
"availabilityImpact": "NONE",
"baseScore": 6.3,
"baseSeverity": "MEDIUM",
"confidentialityImpact": "NONE",
"integrityImpact": "HIGH",
"privilegesRequired": "NONE",
"scope": "CHANGED",
"userInteraction": "REQUIRED",
"vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
"version": "3.1"
},
"format": "CVSS"
}
],
"problemTypes": [
{
"descriptions": [
{
"cweId": "CWE-670",
"description": "Always-Incorrect Control Flow Implementation",
"lang": "en",
"type": "CWE"
}
]
}
],
"providerMetadata": {
"dateUpdated": "2026-09-24T14:18:50.897Z",
"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"shortName": "VulnCheck"
},
"references": [
{
"tags": [
"product"
],
"url": "https://github.com/rocq-prover/rocq"
},
{
"tags": [
"issue-tracking"
],
"url": "https://github.com/rocq-prover/rocq/issues/21682"
},
{
"tags": [
"issue-tracking",
"patch"
],
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"tags": [
"exploit"
],
"url": "https://github.com/endrazine/rocq-cve-poc-21682"
},
{
"name": "VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"tags": [
"third-party-advisory"
],
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"
}
],
"title": "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls",
"x_generator": {
"engine": "vulncheck-endgame"
}
}
},
"cveMetadata": {
"assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"assignerShortName": "VulnCheck",
"cveId": "CVE-2026-72703",
"datePublished": "2026-08-24T20:08:30.607Z",
"dateReserved": "2026-08-10T13:02:20.829Z",
"dateUpdated": "2026-10-26T01:23:54.511Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.2"
}
}
}
Drag nodes to arrange them. Double-click a related vulnerability to open it, or a source to visit its link. The Physics button on the left tunes the layout and the simulation; the legend at the bottom left hides or shows nodes by kind and by sighting type.
Sightings
| Author | Source | Type | Date | Other |
|---|
Nomenclature
- Seen: The vulnerability was mentioned, discussed, or observed by the user.
- Confirmed: The vulnerability has been validated from an analyst's perspective.
- Published Proof of Concept: A public proof of concept is available for this vulnerability.
- Exploited: The vulnerability was observed as exploited by the user who reported the sighting.
- Patched: The vulnerability was observed as successfully patched by the user who reported the sighting.
- Not exploited: The vulnerability was not observed as exploited by the user who reported the sighting.
- Not confirmed: The user expressed doubt about the validity of the vulnerability.
- Not patched: The vulnerability was not observed as successfully patched by the user who reported the sighting.
Vulnerability timeline
Sightings and recorded dates, grouped by day · UTC
How durations are calculated
Following the VTEM framework (Black Hat USA 2015), time to patch starts when the vendor or a coordinator was informed, total time to patch at discovery, and disclosure to patch at public disclosure; vendor response time runs from the report to its acknowledgement. Time to exploit and time unpatched start at the earliest discovery or report, falling back to public disclosure. Unpatched time ends at the first recorded patch, or the calculation time when no patch is recorded. Exploitation to patch shows the interval between those two events; a published proof of concept is a public exploit, not exploitation.
Each result shows its source dates. A negative interval means the end event came first; when date-only inputs leave the order open, the result says so. Date-only inputs are approximate. The earliest evidence wins: KEV report dates and sightings are labelled as such. Records describing another vulnerability are listed but never calculated from, and a PoC alone does not establish exploitation. Missing patch evidence does not prove that no patch exists. Filters below change the event list only.
Loading timeline…
The approach is described in our paper Mapping CVEs to MITRE ATT&CK Techniques: A Curated Gold-Set Classifier and the Limits of LLM-Assisted Label Expansion.
Browse all ATT&CK techniques and the vulnerabilities related to each.
Related by attack behaviour
Vulnerabilities whose description is nearest to this one in the vector space of the CIRCL/vulnerability-attack-technique-biencoder model. This is a similarity search over the bi-encoder space (plain cosine), not a classification, and it has no measured accuracy.