{"id":"CVE-2026-72705","aliases":["EUVD-2026-65141","GHSA-f4rc-7978-q94g"],"status":"published","title":"Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument","description":"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.","severity":{"version":"4.0","score":6.8,"vector":"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","level":"medium","assessor":"cna","from":"cve"},"epss":{"day":"2026-11-11","score":0.00176,"percentile":0.07189,"model":"v2026.06.15"},"facts":{"in_kev":false,"known_exploited":false,"public_exploit":true,"fix_available":false},"cwes":["CWE-670"],"published":"2026-08-24T20:08:32Z","modified":"2026-10-28T02:30:36Z","exploits":[{"source":"pocgithub","id":"endrazine/rocq-cve-poc-21683","title":"endrazine/rocq-cve-poc-21683","date":"2026-08-23","url":"https://github.com/endrazine/rocq-cve-poc-21683"}],"products":[{"vendor":"rocq-prover","product":"rocq"}],"references":[{"url":"https://github.com/rocq-prover/rocq","tags":["product","package"]},{"url":"https://github.com/rocq-prover/rocq/issues/21683","tags":["issue-tracking","report"]},{"url":"https://github.com/rocq-prover/rocq/pull/21684","tags":["issue-tracking","patch","fix"]},{"url":"https://github.com/endrazine/rocq-cve-poc-21683","tags":["exploit","evidence"]},{"url":"https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument","tags":["third-party-advisory","advisory"]},{"url":"http://www.openwall.com/lists/oss-security/2026/10/26/6","tags":["web"]},{"url":"https://nvd.nist.gov/vuln/detail/CVE-2026-72705","tags":["advisory"]},{"url":"https://github.com/advisories/GHSA-f4rc-7978-q94g"},{"url":"https://github.com/CVEProject/cvelistV5/tree/main/cves/2026/72xxx/CVE-2026-72705.json","tags":["advisory"]}],"sources":{"cve":[{"id":"CVE-2026-72705","title":"Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument","description":"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.","status":"published","published":"2026-08-24T20:08:32.535Z","modified":"2026-10-26T01:23:56.439Z","cvss":[{"version":"4.0","score":6.8,"vector":"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","level":"medium","assessor":"cna"},{"version":"3.1","score":6.3,"vector":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N","level":"medium","assessor":"cna"}],"cwes":["CWE-670"],"updated_at":"2026-11-02T14:19:52.016971Z"}],"euvd":[{"id":"EUVD-2026-65141","description":"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.","status":"published","published":"2026-08-24T20:08:32Z","modified":"2026-10-26T01:23:56Z","cvss":[{"version":"4.0","score":6.8,"vector":"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","level":"medium"}],"updated_at":"2026-11-02T16:59:30.362619Z"}],"ghsa":[{"id":"GHSA-f4rc-7978-q94g","title":"The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own...","description":"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.","status":"published","published":"2026-08-24T21:33:44Z","modified":"2026-10-26T03:31:27Z","cvss":[{"version":"4.0","score":6.8,"vector":"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","level":"medium"},{"version":"3.1","score":6.3,"vector":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N","level":"medium"}],"cwes":["CWE-670"],"updated_at":"2026-11-02T15:14:23.372055Z"}],"nvd":[{"id":"CVE-2026-72705","description":"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.","status":"published","published":"2026-08-24T20:17:18.52Z","modified":"2026-10-26T02:17:07.363Z","cvss":[{"version":"4.0","score":6.8,"vector":"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","level":"medium","assessor":"secondary"},{"version":"3.1","score":6.3,"vector":"CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N","level":"medium","assessor":"secondary"}],"cwes":["CWE-670"],"updated_at":"2026-11-02T14:12:41.018848Z"}],"osv":[{"id":"CVE-2026-72705","title":"Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument","description":"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.","status":"published","published":"2026-08-24T20:08:32.535Z","modified":"2026-10-28T02:30:36.793121274Z","cvss":[{"version":"4.0","score":6.8,"vector":"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","level":"medium"}],"cwes":["CWE-670"],"updated_at":"2026-11-02T15:45:15.88521Z"}]}}