CVE-2026-72703

{"dataType": "CVE_RECORD", "dataVersion": "5.2", "cveMetadata": {"cveId": "CVE-2026-72703", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "state": "PUBLISHED", "assignerShortName": "VulnCheck", "dateReserved": "2026-08-10T13:02:20.829Z", "datePublished": "2026-08-24T20:08:30.607Z", "dateUpdated": "2026-10-26T01:23:54.511Z"}, "containers": {"cna": {"providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-09-24T14:18:50.897Z"}, "datePublic": "2026-02-28T00:00:00.000Z", "title": "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls", "descriptions": [{"lang": "en", "value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and 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": "8.20", "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/21682", "tags": ["issue-tracking"]}, {"url": "https://github.com/rocq-prover/rocq/pull/21684", "tags": ["issue-tracking", "patch"]}, {"url": "https://github.com/endrazine/rocq-cve-poc-21682", "tags": ["exploit"]}, {"name": "VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls", "tags": ["third-party-advisory"], "url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls"}], "credits": [{"lang": "en", "value": "Tristan St\u00e9rin", "type": "finder"}, {"lang": "en", "value": "Jonathan Brossard (MOABI)", "type": "finder"}], "x_generator": {"engine": "vulncheck-endgame"}}, "adp": [{"metrics": [{"other": {"type": "ssvc", "content": {"timestamp": "2026-08-27T14:12:25.906004Z", "id": "CVE-2026-72703", "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-27T14:12:34.453Z"}}, {"title": "CVE Program Container", "references": [{"url": "http://www.openwall.com/lists/oss-security/2026/10/26/4"}], "providerMetadata": {"orgId": "af854a3a-2127-422b-91ae-364da2661108", "shortName": "CVE", "dateUpdated": "2026-10-26T01:23:54.511Z"}}]}}

{"dataType": "CVE_RECORD", "containers": {"adp": [{"title": "CVE Program Container", "references": [{"url": "http://www.openwall.com/lists/oss-security/2026/10/26/4"}], "providerMetadata": {"orgId": "af854a3a-2127-422b-91ae-364da2661108", "shortName": "CVE", "dateUpdated": "2026-10-26T01:23:54.511Z"}}, {"title": "CISA ADP Vulnrichment", "metrics": [{"other": {"type": "ssvc", "content": {"id": "CVE-2026-72703", "role": "CISA Coordinator", "options": [{"Exploitation": "poc"}, {"Automatable": "no"}, {"Technical Impact": "partial"}], "version": "2.0.3", "timestamp": "2026-08-27T14:12:25.906004Z"}}}], "providerMetadata": {"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0", "shortName": "CISA-ADP", "dateUpdated": "2026-08-27T14:12:30.905Z"}}], "cna": {"title": "Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls", "credits": [{"lang": "en", "type": "finder", "value": "Tristan St\u00e9rin"}, {"lang": "en", "type": "finder", "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": "8.20", "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/21682", "tags": ["issue-tracking"]}, {"url": "https://github.com/rocq-prover/rocq/pull/21684", "tags": ["issue-tracking", "patch"]}, {"url": "https://github.com/endrazine/rocq-cve-poc-21682", "tags": ["exploit"]}, {"url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls", "name": "VulnCheck Advisory: Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls", "tags": ["third-party-advisory"]}], "x_generator": {"engine": "vulncheck-endgame"}, "descriptions": [{"lang": "en", "value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and 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-09-24T14:18:50.897Z"}}}, "cveMetadata": {"cveId": "CVE-2026-72703", "state": "PUBLISHED", "dateUpdated": "2026-10-26T01:23:54.511Z", "dateReserved": "2026-08-10T13:02:20.829Z", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "datePublished": "2026-08-24T20:08:30.607Z", "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": "8.20", "versionType": "custom"}]}], "source": "disclosure@vulncheck.com"}], "cveTags": [], "descriptions": [{"lang": "en", "value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."}, {"lang": "es", "value": "El verificador de guardas en Rocq Prover trata un par\u00e1metro de un punto fijo mutuo anidado como uniforme sin examinar las llamadas entre los diferentes cuerpos de ese punto fijo. find_uniform_parameters en kernel/inductive.ml inspecciona solo las llamadas autorrecursivas, por lo que cuando ning\u00fan cuerpo se llama a s\u00ed mismo, la funci\u00f3n concluye que cada par\u00e1metro es uniforme. Un par\u00e1metro que crece a trav\u00e9s de una llamada cruzada de un cuerpo a otro, por lo tanto, mantiene la especificaci\u00f3n de subt\u00e9rmino que hered\u00f3 del punto fijo envolvente, y una llamada recursiva protegida por esa especificaci\u00f3n es aceptada aunque el argumento no sea estructuralmente menor. Una definici\u00f3n no terminante es admitida como estructuralmente decreciente, lo que produce un t\u00e9rmino cuyo valor es igual a su propio sucesor y, por lo tanto, una prueba de Falso, de la cual se deduce cualquier proposici\u00f3n. La prueba no requiere axiomas, plugins o banderas inseguras y Print Assumptions lo reporta como cerrado bajo el contexto global. Introducido en Coq 8.20 y corregido en Rocq 9.2.0."}], "id": "CVE-2026-72703", "lastModified": "2026-10-26T02:17:07.063", "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-72703", "options": [{"exploitation": "poc"}, {"automatable": "no"}, {"technicalImpact": "partial"}], "role": "CISA Coordinator", "timestamp": "2026-08-27T14:12:25.906004Z", "version": "2.0.3"}}]}, "published": "2026-08-24T20:17:18.240", "references": [{"source": "disclosure@vulncheck.com", "url": "https://github.com/endrazine/rocq-cve-poc-21682"}, {"source": "disclosure@vulncheck.com", "url": "https://github.com/rocq-prover/rocq"}, {"source": "disclosure@vulncheck.com", "url": "https://github.com/rocq-prover/rocq/issues/21682"}, {"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-non-terminating-fixpoint-via-unchecked-cross-calls"}, {"source": "af854a3a-2127-422b-91ae-364da2661108", "url": "http://www.openwall.com/lists/oss-security/2026/10/26/4"}], "sourceIdentifier": "disclosure@vulncheck.com", "vulnStatus": "Deferred", "weaknesses": [{"description": [{"lang": "en", "value": "CWE-670"}], "source": "disclosure@vulncheck.com", "type": "Secondary"}]}

{}

{"affected": [{"configurations": [{"platform": null, "status": "affected", "versions": {"scheme": "generic", "value": "[8.20,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:00:04.867859+00:00", "updated": "2026-08-28T20:38:48.635694+00:00", "vendors": ["rocq-prover", "rocq-prover$PRODUCT$rocq"]}