CVE-2026-72714

{"dataType": "CVE_RECORD", "dataVersion": "5.2", "cveMetadata": {"cveId": "CVE-2026-72714", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "state": "PUBLISHED", "assignerShortName": "VulnCheck", "dateReserved": "2026-08-10T13:02:52.001Z", "datePublished": "2026-08-24T20:08:33.917Z", "dateUpdated": "2026-10-26T01:23:58.366Z"}, "containers": {"cna": {"providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-09-24T14:18:54.618Z"}, "datePublic": "2026-07-16T00:00:00.000Z", "title": "Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close", "descriptions": [{"lang": "en", "value": "Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available."}], "problemTypes": [{"descriptions": [{"lang": "en", "cweId": "CWE-459", "description": "Incomplete Cleanup", "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", "lessThanOrEqual": "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/22287", "tags": ["issue-tracking"]}, {"url": "https://github.com/endrazine/rocq-cve-poc-22287", "tags": ["exploit"]}, {"name": "VulnCheck Advisory: Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close", "tags": ["third-party-advisory"], "url": "https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close"}], "credits": [{"lang": "en", "value": "Ga\u00ebtan Gilbert", "type": "finder"}, {"lang": "en", "value": "Jonathan Brossard (MOABI)", "type": "finder"}], "x_generator": {"engine": "vulncheck-endgame"}}, "adp": [{"references": [{"url": "https://github.com/rocq-prover/rocq/issues/22287", "tags": ["exploit"]}], "metrics": [{"other": {"type": "ssvc", "content": {"timestamp": "2026-08-25T17:41:19.106957Z", "id": "CVE-2026-72714", "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-25T17:41:24.594Z"}}, {"title": "CVE Program Container", "references": [{"url": "http://www.openwall.com/lists/oss-security/2026/10/26/7"}], "providerMetadata": {"orgId": "af854a3a-2127-422b-91ae-364da2661108", "shortName": "CVE", "dateUpdated": "2026-10-26T01:23:58.366Z"}}]}}

{"dataType": "CVE_RECORD", "containers": {"adp": [{"title": "CVE Program Container", "references": [{"url": "http://www.openwall.com/lists/oss-security/2026/10/26/7"}], "providerMetadata": {"orgId": "af854a3a-2127-422b-91ae-364da2661108", "shortName": "CVE", "dateUpdated": "2026-10-26T01:23:58.366Z"}}, {"title": "CISA ADP Vulnrichment", "metrics": [{"other": {"type": "ssvc", "content": {"id": "CVE-2026-72714", "role": "CISA Coordinator", "options": [{"Exploitation": "poc"}, {"Automatable": "no"}, {"Technical Impact": "partial"}], "version": "2.0.3", "timestamp": "2026-08-25T17:41:19.106957Z"}}}], "references": [{"url": "https://github.com/rocq-prover/rocq/issues/22287", "tags": ["exploit"]}], "providerMetadata": {"orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0", "shortName": "CISA-ADP", "dateUpdated": "2026-08-25T17:41:00.810Z"}}], "cna": {"title": "Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close", "credits": [{"lang": "en", "type": "finder", "value": "Ga\u00ebtan Gilbert"}, {"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": "0", "versionType": "custom", "lessThanOrEqual": "9.2.0"}], "packageURL": "pkg:github/rocq-prover/rocq", "defaultStatus": "unaffected"}], "datePublic": "2026-07-16T00:00:00.000Z", "references": [{"url": "https://github.com/rocq-prover/rocq", "tags": ["product"]}, {"url": "https://github.com/rocq-prover/rocq/issues/22287", "tags": ["issue-tracking"]}, {"url": "https://github.com/endrazine/rocq-cve-poc-22287", "tags": ["exploit"]}, {"url": "https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close", "name": "VulnCheck Advisory: Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close", "tags": ["third-party-advisory"]}], "x_generator": {"engine": "vulncheck-endgame"}, "descriptions": [{"lang": "en", "value": "Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available."}], "problemTypes": [{"descriptions": [{"lang": "en", "type": "CWE", "cweId": "CWE-459", "description": "Incomplete Cleanup"}]}], "providerMetadata": {"orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "shortName": "VulnCheck", "dateUpdated": "2026-09-24T14:18:54.618Z"}}}, "cveMetadata": {"cveId": "CVE-2026-72714", "state": "PUBLISHED", "dateUpdated": "2026-10-26T01:23:58.366Z", "dateReserved": "2026-08-10T13:02:52.001Z", "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10", "datePublished": "2026-08-24T20:08:33.917Z", "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": [{"lessThanOrEqual": "9.2.0", "status": "affected", "version": "0", "versionType": "custom"}]}], "source": "disclosure@vulncheck.com"}], "cveTags": [], "descriptions": [{"lang": "en", "value": "Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available."}, {"lang": "es", "value": "Rocq Prover no restaura la copia del grafo de universos del indicador de verificaci\u00f3n de universos cuando se cierra un m\u00f3dulo que deshabilit\u00f3 localmente la verificaci\u00f3n. Se espera que la desactivaci\u00f3n local de la verificaci\u00f3n de universos dentro de un m\u00f3dulo dure solo hasta que el m\u00f3dulo finalice y el indicador global sea restaurado, pero el grafo de universos mantiene su propia copia, que queda deshabilitada. Las dos vistas entonces discrepan: Test Universe Checking informa que la verificaci\u00f3n est\u00e1 habilitada mientras que el kernel contin\u00faa aceptando t\u00e9rminos inconsistentes con los universos. Al no aplicarse ya la restricci\u00f3n entre dos universos, la paradoja de Hurkens se aplica y produce una prueba de Falso, de la cual se deduce cualquier proposici\u00f3n. La prueba no utiliza axiomas, plugins ni caracter\u00edsticas inseguras una vez que el m\u00f3dulo se ha cerrado, y Print Assumptions lo reporta como cerrado bajo el contexto global, por lo que ni la auditor\u00eda de suposiciones ni la consulta del indicador reflejan el estado real del kernel. No hay soluci\u00f3n disponible."}], "id": "CVE-2026-72714", "lastModified": "2026-10-26T02:17:07.680", "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-72714", "options": [{"exploitation": "poc"}, {"automatable": "no"}, {"technicalImpact": "partial"}], "role": "CISA Coordinator", "timestamp": "2026-08-25T17:41:19.106957Z", "version": "2.0.3"}}]}, "published": "2026-08-24T20:17:18.810", "references": [{"source": "disclosure@vulncheck.com", "url": "https://github.com/endrazine/rocq-cve-poc-22287"}, {"source": "disclosure@vulncheck.com", "url": "https://github.com/rocq-prover/rocq"}, {"source": "disclosure@vulncheck.com", "url": "https://github.com/rocq-prover/rocq/issues/22287"}, {"source": "disclosure@vulncheck.com", "url": "https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close"}, {"source": "af854a3a-2127-422b-91ae-364da2661108", "url": "http://www.openwall.com/lists/oss-security/2026/10/26/7"}, {"source": "134c704f-9b21-4f2e-91b3-4a467353bcc0", "url": "https://github.com/rocq-prover/rocq/issues/22287"}], "sourceIdentifier": "disclosure@vulncheck.com", "vulnStatus": "Deferred", "weaknesses": [{"description": [{"lang": "en", "value": "CWE-459"}], "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.402997+00:00", "updated": "2026-08-28T20:38:43.609239+00:00", "vendors": ["rocq-prover", "rocq-prover$PRODUCT$rocq"]}