{"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-26T16:13:14.137Z"}, "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"}}, "adp": [{"metrics": [{"other": {"type": "ssvc", "content": {"timestamp": "2026-08-26T15:46:51.503814Z", "id": "CVE-2026-72705", "options": [{"Exploitation": "poc"}, {"Automatable": "no"}, {"Technical Impact": "partial"}], "role": "CISA Coordinator", "version": "2.0.3"}}}], "title": "CISA ADP Vulnrichment", "providerMetadata": {"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0", "shortName": "CISA-ADP", "dateUpdated": "2026-08-26T16:13:14.137Z"}}]}}

{"dataType": "CVE_RECORD", "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"]}, {"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'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", "type": "CWE", "cweId": "CWE-670", "description": "Always-Incorrect Control Flow Implementation"}]}], "providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-08-24T20:08:32.535Z"}}}, "cveMetadata": {"cveId": "CVE-2026-72705", "state": "PUBLISHED", "dateUpdated": "2026-08-26T16:13:14.137Z", "dateReserved": "2026-08-10T13:02:52.001Z", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "datePublished": "2026-08-24T20:08:32.535Z", "assignerShortName": "VulnCheck"}, "dataVersion": "5.2"}

{"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-26T17:17:13.657", "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-72705", "options": [{"exploitation": "poc"}, {"automatable": "no"}, {"technicalImpact": "partial"}], "role": "CISA Coordinator", "timestamp": "2026-08-26T15:46:51.503814Z", "version": "2.0.3"}}]}, "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": "Secondary"}]}

{}

{"affected": [{"configurations": [{"platform": null, "status": "affected", "versions": {"scheme": "generic", "value": "[0,9.2.0)"}}], "enrichment": {"confidence": 100.0, "confidence_source": "cna", "scores": [{"score": 100.0, "source": "cna"}]}, "original": {"product": "rocq", "source": "cna", "vendor": "rocq-prover"}, "product": "rocq", "vendor": "rocq-prover"}], "created": "2026-08-24T22:45:03.403186+00:00", "updated": "2026-08-28T20:38:45.296957+00:00", "vendors": ["rocq-prover", "rocq-prover$PRODUCT$rocq"]}