CVE-2026-72705 (GCVE-0-2026-72705)
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 does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.
References
| URL | Tags | ||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|||||||||||||||||
Impacted products
| Vendor | Product | Version | ||
|---|---|---|---|---|
| rocq-prover | rocq |
Version: 0 < 9.2.0 |
{
"containers": {
"adp": [
{
"metrics": [
{
"other": {
"content": {
"id": "CVE-2026-72705",
"options": [
{
"Exploitation": "poc"
},
{
"Automatable": "no"
},
{
"Technical Impact": "partial"
}
],
"role": "CISA Coordinator",
"timestamp": "2026-08-26T15:46:51.503814Z",
"version": "2.0.3"
},
"type": "ssvc"
}
}
],
"providerMetadata": {
"dateUpdated": "2026-08-26T16:13:14.137Z",
"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": "0",
"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 does not follow recursive calls made through a fixpoint\u0027s own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. 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:44.348Z",
"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/21683"
},
{
"tags": [
"issue-tracking",
"patch"
],
"url": "https://github.com/rocq-prover/rocq/pull/21684"
},
{
"tags": [
"exploit"
],
"url": "https://github.com/endrazine/rocq-cve-poc-21683"
},
{
"name": "VulnCheck Advisory: Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument",
"tags": [
"third-party-advisory"
],
"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument"
}
],
"title": "Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument",
"x_generator": {
"engine": "vulncheck-endgame"
}
}
},
"cveMetadata": {
"assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
"assignerShortName": "VulnCheck",
"cveId": "CVE-2026-72705",
"datePublished": "2026-08-24T20:08:32.535Z",
"dateReserved": "2026-08-10T13:02:52.001Z",
"dateUpdated": "2026-08-29T11:47:44.348Z",
"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-72705\", \"role\": \"CISA Coordinator\", \"options\": [{\"Exploitation\": \"poc\"}, {\"Automatable\": \"no\"}, {\"Technical Impact\": \"partial\"}], \"version\": \"2.0.3\", \"timestamp\": \"2026-08-26T15:46:51.503814Z\"}}}], \"providerMetadata\": {\"orgId\": \"134c704f-9b21-4f2e-91b3-4a467353bcc0\", \"shortName\": \"CISA-ADP\", \"dateUpdated\": \"2026-08-26T15:46:55.891Z\"}}], \"cna\": {\"title\": \"Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument\", \"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\": \"0\", \"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/21683\", \"tags\": [\"issue-tracking\"]}, {\"url\": \"https://github.com/rocq-prover/rocq/pull/21684\", \"tags\": [\"issue-tracking\", \"patch\"]}, {\"url\": \"https://github.com/endrazine/rocq-cve-poc-21683\", \"tags\": [\"exploit\"]}, {\"url\": \"https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument\", \"name\": \"VulnCheck Advisory: Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument\", \"tags\": [\"third-party-advisory\"]}], \"x_generator\": {\"engine\": \"vulncheck-endgame\"}, \"descriptions\": [{\"lang\": \"en\", \"value\": \"The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint\u0027s own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. 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:44.348Z\"}}}",
"cveMetadata": "{\"cveId\": \"CVE-2026-72705\", \"state\": \"PUBLISHED\", \"dateUpdated\": \"2026-08-29T11:47:44.348Z\", \"dateReserved\": \"2026-08-10T13:02:52.001Z\", \"assignerOrgId\": \"83251b91-4cc7-4094-a5c7-464a1b83ea10\", \"datePublished\": \"2026-08-24T20:08:32.535Z\", \"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…