{"dataType": "CVE_RECORD", "dataVersion": "5.2", "cveMetadata": {"cveId": "CVE-2026-72705", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "state": "PUBLISHED", "assignerShortName": "VulnCheck", "dateReserved": "2026-08-10T13:02:52.001Z", "datePublished": "2026-08-24T20:08:32.535Z", "dateUpdated": "2026-08-24T20:08:32.535Z"}, "containers": {"cna": {"providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-08-24T20:08:32.535Z"}, "datePublic": "2026-02-28T00:00:00.000Z", "title": "Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument", "descriptions": [{"lang": "en", "value": "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."}], "problemTypes": [{"descriptions": [{"lang": "en", "cweId": "CWE-670", "description": "Always-Incorrect Control Flow Implementation", "type": "CWE"}]}], "affected": [{"vendor": "rocq-prover", "product": "rocq", "repo": "https://github.com/rocq-prover/rocq", "packageURL": "pkg:github/rocq-prover/rocq", "defaultStatus": "unaffected", "versions": [{"version": "0", "lessThan": "9.2.0", "status": "affected", "versionType": "custom"}]}], "metrics": [{"format": "CVSS", "cvssV4_0": {"version": "4.0", "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", "baseScore": 6.8, "baseSeverity": "MEDIUM", "attackVector": "LOCAL", "attackComplexity": "LOW", "attackRequirements": "NONE", "privilegesRequired": "NONE", "userInteraction": "PASSIVE", "vulnConfidentialityImpact": "NONE", "vulnIntegrityImpact": "HIGH", "vulnAvailabilityImpact": "NONE", "subConfidentialityImpact": "NONE", "subIntegrityImpact": "NONE", "subAvailabilityImpact": "NONE"}}, {"format": "CVSS", "cvssV3_1": {"version": "3.1", "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N", "baseScore": 6.3, "baseSeverity": "MEDIUM", "attackVector": "LOCAL", "attackComplexity": "LOW", "privilegesRequired": "NONE", "userInteraction": "REQUIRED", "scope": "CHANGED", "confidentialityImpact": "NONE", "integrityImpact": "HIGH", "availabilityImpact": "NONE"}}], "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"]}, {"url": "https://github.com/endrazine/rocq-cve-poc-21683", "tags": ["exploit"]}, {"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"}], "credits": [{"lang": "en", "value": "Tristan St\u00e9rin", "type": "finder"}, {"lang": "en", "value": "Jonathan Brossard (MOABI)", "type": "reporter"}], "x_generator": {"engine": "vulncheck-endgame"}}}}

{}

{"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": "0", "versionType": "custom"}]}], "source": "disclosure@vulncheck.com"}], "cveTags": [], "descriptions": [{"lang": "en", "value": "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."}], "id": "CVE-2026-72705", "lastModified": "2026-08-24T20:17:18.520", "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": "Primary"}], "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"}]}, "published": "2026-08-24T20:17:18.520", "references": [{"source": "disclosure@vulncheck.com", "url": "https://github.com/endrazine/rocq-cve-poc-21683"}, {"source": "disclosure@vulncheck.com", "url": "https://github.com/rocq-prover/rocq"}, {"source": "disclosure@vulncheck.com", "url": "https://github.com/rocq-prover/rocq/issues/21683"}, {"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-fixpoint-passed-as-a-higher-order-argument"}], "sourceIdentifier": "disclosure@vulncheck.com", "vulnStatus": "Received", "weaknesses": [{"description": [{"lang": "en", "value": "CWE-670"}], "source": "disclosure@vulncheck.com", "type": "Primary"}]}

{}

{}