CVE-2026-72703 (GCVE-0-2026-72703)
Vulnerability from cvelistv5
Published
2026-08-24 20:08
Modified
2026-08-29 11:47
Severity ?
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
6.3 (Medium) - CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
6.3 (Medium) - CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
VLAI Severity ?
EPSS score ?
CWE
- CWE-670 - Always-Incorrect Control Flow Implementation
Summary
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.
References
| URL | Tags | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|||||||||||||||||
Impacted products
| Vendor | Product | Version | ||
|---|---|---|---|---|
| rocq-prover | rocq |
Version: 8.20 < 9.2.0 |
{
"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"
}
],
"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": "reporter",
"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-08-29T11:47:43.005Z",
"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-08-29T11:47:43.005Z",
"state": "PUBLISHED"
},
"dataType": "CVE_RECORD",
"dataVersion": "5.2",
"vulnerability-lookup:meta": {
"vulnrichment": {
"containers": "{\"adp\": [{\"title\": \"CISA ADP Vulnrichment\", \"metrics\": [{\"other\": {\"type\": \"ssvc\", \"content\": {\"id\": \"CVE-2026-72703\", \"role\": \"CISA Coordinator\", \"options\": [{\"Exploitation\": \"poc\"}, {\"Automatable\": \"no\"}, {\"Technical Impact\": \"partial\"}], \"version\": \"2.0.3\", \"timestamp\": \"2026-08-27T14:12:25.906004Z\"}}}], \"providerMetadata\": {\"orgId\": \"134c704f-9b21-4f2e-91b3-4a467353bcc0\", \"shortName\": \"CISA-ADP\", \"dateUpdated\": \"2026-08-27T14:12:30.905Z\"}}], \"cna\": {\"title\": \"Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls\", \"credits\": [{\"lang\": \"en\", \"type\": \"finder\", \"value\": \"Tristan St\\u00e9rin\"}, {\"lang\": \"en\", \"type\": \"reporter\", \"value\": \"Jonathan Brossard (MOABI)\"}], \"metrics\": [{\"format\": \"CVSS\", \"cvssV4_0\": {\"version\": \"4.0\", \"baseScore\": 6.8, \"attackVector\": \"LOCAL\", \"baseSeverity\": \"MEDIUM\", \"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\", \"userInteraction\": \"PASSIVE\", \"attackComplexity\": \"LOW\", \"attackRequirements\": \"NONE\", \"privilegesRequired\": \"NONE\", \"subIntegrityImpact\": \"NONE\", \"vulnIntegrityImpact\": \"HIGH\", \"subAvailabilityImpact\": \"NONE\", \"vulnAvailabilityImpact\": \"NONE\", \"subConfidentialityImpact\": \"NONE\", \"vulnConfidentialityImpact\": \"NONE\"}}, {\"format\": \"CVSS\", \"cvssV3_1\": {\"scope\": \"CHANGED\", \"version\": \"3.1\", \"baseScore\": 6.3, \"attackVector\": \"LOCAL\", \"baseSeverity\": \"MEDIUM\", \"vectorString\": \"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N\", \"integrityImpact\": \"HIGH\", \"userInteraction\": \"REQUIRED\", \"attackComplexity\": \"LOW\", \"availabilityImpact\": \"NONE\", \"privilegesRequired\": \"NONE\", \"confidentialityImpact\": \"NONE\"}}], \"affected\": [{\"repo\": \"https://github.com/rocq-prover/rocq\", \"vendor\": \"rocq-prover\", \"product\": \"rocq\", \"versions\": [{\"status\": \"affected\", \"version\": \"8.20\", \"lessThan\": \"9.2.0\", \"versionType\": \"custom\"}], \"packageURL\": \"pkg:github/rocq-prover/rocq\", \"defaultStatus\": \"unaffected\"}], \"datePublic\": \"2026-02-28T00:00:00.000Z\", \"references\": [{\"url\": \"https://github.com/rocq-prover/rocq\", \"tags\": [\"product\"]}, {\"url\": \"https://github.com/rocq-prover/rocq/issues/21682\", \"tags\": [\"issue-tracking\"]}, {\"url\": \"https://github.com/rocq-prover/rocq/pull/21684\", \"tags\": [\"issue-tracking\", \"patch\"]}, {\"url\": \"https://github.com/endrazine/rocq-cve-poc-21682\", \"tags\": [\"exploit\"]}, {\"url\": \"https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls\", \"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\"]}], \"x_generator\": {\"engine\": \"vulncheck-endgame\"}, \"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.\"}], \"problemTypes\": [{\"descriptions\": [{\"lang\": \"en\", \"type\": \"CWE\", \"cweId\": \"CWE-670\", \"description\": \"Always-Incorrect Control Flow Implementation\"}]}], \"providerMetadata\": {\"orgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"shortName\": \"VulnCheck\", \"dateUpdated\": \"2026-08-29T11:47:43.005Z\"}}}",
"cveMetadata": "{\"cveId\": \"CVE-2026-72703\", \"state\": \"PUBLISHED\", \"dateUpdated\": \"2026-08-29T11:47:43.005Z\", \"dateReserved\": \"2026-08-10T13:02:20.829Z\", \"assignerOrgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"datePublished\": \"2026-08-24T20:08:30.607Z\", \"assignerShortName\": \"VulnCheck\"}",
"dataType": "CVE_RECORD",
"dataVersion": "5.2"
}
}
}
Loading…
Loading…
Sightings
| Author | Source | Type | Date |
|---|
Nomenclature
- Seen: The vulnerability was mentioned, discussed, or seen somewhere by the user.
- Confirmed: The vulnerability is confirmed from an analyst perspective.
- Published Proof of Concept: A public proof of concept is available for this vulnerability.
- Exploited: This vulnerability was exploited and seen by the user reporting the sighting.
- Patched: This vulnerability was successfully patched by the user reporting the sighting.
- Not exploited: This vulnerability was not exploited or seen by the user reporting the sighting.
- Not confirmed: The user expresses doubt about the veracity of the vulnerability.
- Not patched: This vulnerability was not successfully patched by the user reporting the sighting.
Loading…
Loading…