← Back to CVE Explorer

CVE-2026-72714

Full vulnerability record from the local CVENow database.

Description

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.

Severity
MEDIUM
CVSS score
6.8 (v4.0)
Vulnerability status
Deferred
Source identifier
[email protected]
Published
2026-08-24 20:17:18.810000
Last modified
2026-10-26 02:17:07.680000
View original CVE JSON 
{
  "id": "CVE-2026-72714",
  "sourceIdentifier": "[email protected]",
  "published": "2026-08-24T20:17:18.810",
  "lastModified": "2026-10-26T02:17:07.680",
  "vulnStatus": "Deferred",
  "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ón de universos cuando se cierra un módulo que deshabilitó localmente la verificación. Se espera que la desactivación local de la verificación de universos dentro de un módulo dure solo hasta que el módulo 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ón está habilitada mientras que el kernel continúa aceptando términos inconsistentes con los universos. Al no aplicarse ya la restricción entre dos universos, la paradoja de Hurkens se aplica y produce una prueba de Falso, de la cual se deduce cualquier proposición. La prueba no utiliza axiomas, plugins ni características inseguras una vez que el módulo se ha cerrado, y Print Assumptions lo reporta como cerrado bajo el contexto global, por lo que ni la auditoría de suposiciones ni la consulta del indicador reflejan el estado real del kernel. No hay solución disponible."
    }
  ],
  "affected": [
    {
      "source": "[email protected]",
      "affectedData": [
        {
          "vendor": "rocq-prover",
          "product": "rocq",
          "defaultStatus": "unaffected",
          "repo": "https://github.com/rocq-prover/rocq",
          "packageURL": "pkg:github/rocq-prover/rocq",
          "versions": [
            {
              "version": "0",
              "lessThanOrEqual": "9.2.0",
              "versionType": "custom",
              "status": "affected"
            }
          ]
        }
      ]
    }
  ],
  "metrics": {
    "cvssMetricV40": [
      {
        "source": "[email protected]",
        "type": "Secondary",
        "cvssData": {
          "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/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",
          "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",
          "exploitMaturity": "NOT_DEFINED",
          "confidentialityRequirement": "NOT_DEFINED",
          "integrityRequirement": "NOT_DEFINED",
          "availabilityRequirement": "NOT_DEFINED",
          "modifiedAttackVector": "NOT_DEFINED",
          "modifiedAttackComplexity": "NOT_DEFINED",
          "modifiedAttackRequirements": "NOT_DEFINED",
          "modifiedPrivilegesRequired": "NOT_DEFINED",
          "modifiedUserInteraction": "NOT_DEFINED",
          "modifiedVulnConfidentialityImpact": "NOT_DEFINED",
          "modifiedVulnIntegrityImpact": "NOT_DEFINED",
          "modifiedVulnAvailabilityImpact": "NOT_DEFINED",
          "modifiedSubConfidentialityImpact": "NOT_DEFINED",
          "modifiedSubIntegrityImpact": "NOT_DEFINED",
          "modifiedSubAvailabilityImpact": "NOT_DEFINED",
          "Safety": "NOT_DEFINED",
          "Automatable": "NOT_DEFINED",
          "Recovery": "NOT_DEFINED",
          "valueDensity": "NOT_DEFINED",
          "vulnerabilityResponseEffort": "NOT_DEFINED",
          "providerUrgency": "NOT_DEFINED"
        }
      }
    ],
    "cvssMetricV31": [
      {
        "source": "[email protected]",
        "type": "Secondary",
        "cvssData": {
          "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"
        },
        "exploitabilityScore": 1.8,
        "impactScore": 4.0
      }
    ],
    "ssvcV203": [
      {
        "source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
        "ssvcData": {
          "timestamp": "2026-08-25T17:41:19.106957Z",
          "id": "CVE-2026-72714",
          "options": [
            {
              "exploitation": "poc"
            },
            {
              "automatable": "no"
            },
            {
              "technicalImpact": "partial"
            }
          ],
          "role": "CISA Coordinator",
          "version": "2.0.3"
        }
      }
    ]
  },
  "weaknesses": [
    {
      "source": "[email protected]",
      "type": "Secondary",
      "description": [
        {
          "lang": "en",
          "value": "CWE-459"
        }
      ]
    }
  ],
  "references": [
    {
      "url": "https://github.com/endrazine/rocq-cve-poc-22287",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/rocq-prover/rocq",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/rocq-prover/rocq/issues/22287",
      "source": "[email protected]"
    },
    {
      "url": "https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close",
      "source": "[email protected]"
    },
    {
      "url": "http://www.openwall.com/lists/oss-security/2026/10/26/7",
      "source": "af854a3a-2127-422b-91ae-364da2661108"
    },
    {
      "url": "https://github.com/rocq-prover/rocq/issues/22287",
      "source": "134c704f-9b21-4f2e-91b3-4a467353bcc0"
    }
  ]
}