{
    "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érin",
                    "type": "finder"
                },
                {
                    "lang": "en",
                    "value": "Jonathan Brossard (MOABI)",
                    "type": "reporter"
                }
            ],
            "x_generator": {
                "engine": "vulncheck-endgame"
            }
        }
    }
}