CVE-2026-72714 (GCVE-0-2026-72714)

Vulnerability from cvelistv5 – Published: 2026-08-24 20:08 – Updated: 2026-09-24 14:18
VLAI
Title
Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
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.
Severity
6.8 (Medium)
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
6.3 (Medium)
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
SSVC
Exploitation: poc Automatable: no Technical Impact: partial
CISA Coordinator · CISA-ADP (v2.0.3)
Decision recorded 2026-08-25 17:41 UTC
CWE
Assigner
VulnCheck CNA under the mitre root
CNA scorecard B 84/100 over 6106 records in the last 180 days details
References
Impacted products
Vendor Product Version CPE status
rocq-prover rocq Affected: 0 , ≤ 9.2.0 (custom)
guessed Create a notification for this product.
Date Public
2026-07-16 00:00
Credits
Gaëtan Gilbert Jonathan Brossard (MOABI)
Show details on NVD website
To clipboard 

{
  "containers": {
    "adp": [
      {
        "metrics": [
          {
            "other": {
              "content": {
                "id": "CVE-2026-72714",
                "options": [
                  {
                    "Exploitation": "poc"
                  },
                  {
                    "Automatable": "no"
                  },
                  {
                    "Technical Impact": "partial"
                  }
                ],
                "role": "CISA Coordinator",
                "timestamp": "2026-08-25T17:41:19.106957Z",
                "version": "2.0.3"
              },
              "type": "ssvc"
            }
          }
        ],
        "providerMetadata": {
          "dateUpdated": "2026-08-25T17:41:24.594Z",
          "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
          "shortName": "CISA-ADP"
        },
        "references": [
          {
            "tags": [
              "exploit"
            ],
            "url": "https://github.com/rocq-prover/rocq/issues/22287"
          }
        ],
        "title": "CISA ADP Vulnrichment"
      }
    ],
    "cna": {
      "affected": [
        {
          "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"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "Ga\u00ebtan Gilbert"
        },
        {
          "lang": "en",
          "type": "finder",
          "value": "Jonathan Brossard (MOABI)"
        }
      ],
      "datePublic": "2026-07-16T00:00:00.000Z",
      "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."
        }
      ],
      "metrics": [
        {
          "cvssV4_0": {
            "attackComplexity": "LOW",
            "attackRequirements": "NONE",
            "attackVector": "LOCAL",
            "baseScore": 6.8,
            "baseSeverity": "MEDIUM",
            "privilegesRequired": "NONE",
            "subAvailabilityImpact": "NONE",
            "subConfidentialityImpact": "NONE",
            "subIntegrityImpact": "NONE",
            "userInteraction": "PASSIVE",
            "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",
            "version": "4.0",
            "vulnAvailabilityImpact": "NONE",
            "vulnConfidentialityImpact": "NONE",
            "vulnIntegrityImpact": "HIGH"
          },
          "format": "CVSS"
        },
        {
          "cvssV3_1": {
            "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"
          },
          "format": "CVSS"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-459",
              "description": "Incomplete Cleanup",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-09-24T14:18:54.618Z",
        "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "shortName": "VulnCheck"
      },
      "references": [
        {
          "tags": [
            "product"
          ],
          "url": "https://github.com/rocq-prover/rocq"
        },
        {
          "tags": [
            "issue-tracking"
          ],
          "url": "https://github.com/rocq-prover/rocq/issues/22287"
        },
        {
          "tags": [
            "exploit"
          ],
          "url": "https://github.com/endrazine/rocq-cve-poc-22287"
        },
        {
          "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"
        }
      ],
      "title": "Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close",
      "x_generator": {
        "engine": "vulncheck-endgame"
      }
    }
  },
  "cveMetadata": {
    "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
    "assignerShortName": "VulnCheck",
    "cveId": "CVE-2026-72714",
    "datePublished": "2026-08-24T20:08:33.917Z",
    "dateReserved": "2026-08-10T13:02:52.001Z",
    "dateUpdated": "2026-09-24T14:18:54.618Z",
    "state": "PUBLISHED"
  },
  "dataType": "CVE_RECORD",
  "dataVersion": "5.2",
  "vulnerability-lookup:meta": {
    "epss": {
      "cve": "CVE-2026-72714",
      "date": "2026-10-14",
      "epss": "0.00176",
      "percentile": "0.06654"
    },
    "nvd": {
      "cve": {
        "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"
          }
        ]
      }
    },
    "redhat_vex": {
      "current_release_date": "2026-08-24T21:18:53+00:00",
      "cve": "CVE-2026-72714",
      "id": "CVE-2026-72714",
      "initial_release_date": "2026-08-24T20:08:33.917000+00:00",
      "product_status:known_not_affected": "1",
      "source": "Red Hat CSAF VEX",
      "status": "final",
      "title": "rocq: Rocq Prover: Critical integrity bypass via universe checking state desynchronization.",
      "url": "https://security.access.redhat.com/data/csaf/v2/vex/2026/cve-2026-72714.json",
      "version": "3"
    },
    "vulnrichment": {
      "containers": {
        "adp": [
          {
            "metrics": [
              {
                "other": {
                  "content": {
                    "id": "CVE-2026-72714",
                    "options": [
                      {
                        "Exploitation": "poc"
                      },
                      {
                        "Automatable": "no"
                      },
                      {
                        "Technical Impact": "partial"
                      }
                    ],
                    "role": "CISA Coordinator",
                    "timestamp": "2026-08-25T17:41:19.106957Z",
                    "version": "2.0.3"
                  },
                  "type": "ssvc"
                }
              }
            ],
            "providerMetadata": {
              "dateUpdated": "2026-08-25T17:41:00.810Z",
              "orgId": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
              "shortName": "CISA-ADP"
            },
            "references": [
              {
                "tags": [
                  "exploit"
                ],
                "url": "https://github.com/rocq-prover/rocq/issues/22287"
              }
            ],
            "title": "CISA ADP Vulnrichment"
          }
        ],
        "cna": {
          "affected": [
            {
              "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"
                }
              ]
            }
          ],
          "credits": [
            {
              "lang": "en",
              "type": "finder",
              "value": "Ga\u00ebtan Gilbert"
            },
            {
              "lang": "en",
              "type": "finder",
              "value": "Jonathan Brossard (MOABI)"
            }
          ],
          "datePublic": "2026-07-16T00:00:00.000Z",
          "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."
            }
          ],
          "metrics": [
            {
              "cvssV4_0": {
                "attackComplexity": "LOW",
                "attackRequirements": "NONE",
                "attackVector": "LOCAL",
                "baseScore": 6.8,
                "baseSeverity": "MEDIUM",
                "privilegesRequired": "NONE",
                "subAvailabilityImpact": "NONE",
                "subConfidentialityImpact": "NONE",
                "subIntegrityImpact": "NONE",
                "userInteraction": "PASSIVE",
                "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",
                "version": "4.0",
                "vulnAvailabilityImpact": "NONE",
                "vulnConfidentialityImpact": "NONE",
                "vulnIntegrityImpact": "HIGH"
              },
              "format": "CVSS"
            },
            {
              "cvssV3_1": {
                "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"
              },
              "format": "CVSS"
            }
          ],
          "problemTypes": [
            {
              "descriptions": [
                {
                  "cweId": "CWE-459",
                  "description": "Incomplete Cleanup",
                  "lang": "en",
                  "type": "CWE"
                }
              ]
            }
          ],
          "providerMetadata": {
            "dateUpdated": "2026-09-24T14:18:54.618Z",
            "orgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
            "shortName": "VulnCheck"
          },
          "references": [
            {
              "tags": [
                "product"
              ],
              "url": "https://github.com/rocq-prover/rocq"
            },
            {
              "tags": [
                "issue-tracking"
              ],
              "url": "https://github.com/rocq-prover/rocq/issues/22287"
            },
            {
              "tags": [
                "exploit"
              ],
              "url": "https://github.com/endrazine/rocq-cve-poc-22287"
            },
            {
              "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"
            }
          ],
          "title": "Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close",
          "x_generator": {
            "engine": "vulncheck-endgame"
          }
        }
      },
      "cveMetadata": {
        "assignerOrgId": "83251b91-4cc7-4094-a5c7-464a1b83ea10",
        "assignerShortName": "VulnCheck",
        "cveId": "CVE-2026-72714",
        "datePublished": "2026-08-24T20:08:33.917Z",
        "dateReserved": "2026-08-10T13:02:52.001Z",
        "dateUpdated": "2026-09-24T14:18:54.618Z",
        "state": "PUBLISHED"
      },
      "dataType": "CVE_RECORD",
      "dataVersion": "5.2"
    }
  }
}



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.