FKIE_CVE-2026-72714

Vulnerability from fkie_nvd - Published: 2026-08-24 20:17 - Updated: 2026-10-12 15:10
Severity
6.3 (Medium) - CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
Summary
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.
References
disclosure@vulncheck.comhttps://github.com/endrazine/rocq-cve-poc-22287
disclosure@vulncheck.comhttps://github.com/rocq-prover/rocq
disclosure@vulncheck.comhttps://github.com/rocq-prover/rocq/issues/22287
disclosure@vulncheck.comhttps://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close
134c704f-9b21-4f2e-91b3-4a467353bcc0https://github.com/rocq-prover/rocq/issues/22287
Impacted products
Vendor Product Version
To clipboard 

{
  "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\u0027s 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\u0027 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-12T15:10:00.207",
  "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": "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"
    }
  ]
}



Log in or create an account to share your comment.




Tags
Taxonomy of the tags.




Drag nodes to arrange them. Double-click a related vulnerability to open it, or a source to visit its link. The Physics button on the left tunes the layout and the simulation; the legend at the bottom left hides or shows nodes by kind and by sighting type.

Forecast uses a logistic model when the trend is rising, or an exponential decay model when the trend is falling. Fitted via linearized least squares.

Sightings

Author Source Type Date Other

Nomenclature

  • Seen: The vulnerability was mentioned, discussed, or observed by the user.
  • Confirmed: The vulnerability has been validated from an analyst's perspective.
  • Published Proof of Concept: A public proof of concept is available for this vulnerability.
  • Exploited: The vulnerability was observed as exploited by the user who reported the sighting.
  • Patched: The vulnerability was observed as successfully patched by the user who reported the sighting.
  • Not exploited: The vulnerability was not observed as exploited by the user who reported the sighting.
  • Not confirmed: The user expressed doubt about the validity of the vulnerability.
  • Not patched: The vulnerability was not observed as successfully patched by the user who reported the sighting.
Vulnerability timeline

Sightings and recorded dates, grouped by day · UTC

JSON

Loading timeline…




    Related by attack behaviour

    Vulnerabilities whose description is nearest to this one in the vector space of the CIRCL/vulnerability-attack-technique-biencoder model. This is a similarity search over the bi-encoder space (plain cosine), not a classification, and it has no measured accuracy.