GCVE-1988-2026-0444

Vulnerability from gna-1988 – Published: 2026-11-02 07:29 – Updated: 2026-11-02 07:29
VLAI
Title
[Bugtraq] CVE-2026-72704: Rocq guard checker trusts corrupted recursive tree after transport (0 = 1 demonstrated) — 0-day
Summary
1. Summary ========== A soundness bug in the Rocq (formerly Coq) kernel's guard checker allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1. The guard checker does not recheck the recursive tree (rectree) for an inductive type parameter after a transport (rewrite via eq_rect/rew) changes that parameter. A fixpoint applies a rewrite along a type equality to its recursive argument; the checker accepts this because the inductive type is preserved, but the rectree is corrupted. A second fixpoint that calls the first inherits the corrupted tree without verification, so a non-structurally-decreasing call passes as terminating. This is a 0-day: no fix has been merged as of Rocq 9.2.0. 2. Context ========== Rocq (formerly Coq) is the reference implementation of the Calculus of Inductive Constructions and one of the most widely deployed proof assistants. Its kernel is the trusted core that checks every proof before acceptance. A soundness bug in the guard checker — the component that enforces termination of recursive definitions — undermines the guarantees of any system built on Rocq-checked proofs. Formally verified systems certified under Common Criteria (ISO 15408) or DO-178C (airborne software) derive their assurance from the correctness of the proof checker. A kernel-level bypass invalidates that assurance chain. 3. Impact ========= - Formally verified compilers (CompCert) - Verified OS kernels (CertiKOS) - Separation logic frameworks (Iris) - Mathematical libraries (MathComp) - Proof-carrying code: a malicious .v file in a dependency could introduce unsound declarations - Verified smart contracts (ConCert) 4. Proof of Concept =================== A Docker-reproducible PoC is available: git clone https://github.com/endrazine/rocq-cve-poc-22024 cd rocq-cve-poc-22024 docker build -t rocq-cve-poc-22024 . docker run --rm rocq-cve-poc-22024 The PoC uses two axioms (e : nat = nat, and e1 : rew [fun T => T] e in 0 = 1) that are consequences of univalence and are consistent with the Calculus of Inductive Constructions. The proof of 0 = 1 exploits the guard checker flaw, not the axioms. 5. Root Cause ============= The guard checker accepts a recursive call when the inductive type of the argument is preserved, but it does not re-derive the rectree after a transport (eq_rect / rew) changes the type parameter. The corrupted rectree is inherited by subsequent fixpoints without reverification. CWE-670: Always-Incorrect Control Flow Implementation. 6. Scoring ========== CVSS 3.1: AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High) 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.8 (Medium) 7. CWE ====== CWE-670: Always-Incorrect Control Flow Implementation 8. CVE ====== CVE-2026-72704 (assigned by VulnCheck as CNA) 9. Affected Versions ==================== Rocq Prover ≤ 9.2.0 (all versions including Coq 8.x) Fixed in: UNFIXED — PR #22027 proposed but not merged. 10. Mitigation ============== - No patched version is available. - Run coqchk on compiled .vo files — coqchk may catch the inconsistency. - Audit dependencies for use of transport (rew / eq_rect) in fixpoint definitions with nested mutual recursion. 11. References ============== Bug report: https://github.com/rocq-prover/rocq/issues/22024 Fix (open): https://github.com/rocq-prover/rocq/pull/22027 PoC: https://github.com/endrazine/rocq-cve-poc-22024 VulnCheck: https://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trust... NVD: https://nvd.nist.gov/vuln/detail/CVE-2026-72704 12. Timeline ============ 2026 Bug reported by Yann Leray (rocq-prover/rocq#22024) 2026 Fix proposed (PR #22027) — not yet merged 2026-08-24 CVE-2026-72704 published by VulnCheck 2026-08-24 Docker-reproducible PoC published 13. Credit ========== Bug discovery: Yann Leray (@yannl35133) PoC packaging: Jonathan Brossard (@endrazine) — MOABI / PSIRT.com
Severity
No CVSS data available.
CWE
Assigner
VULNARCHIVE GNA GNA-1988
GNA scorecard E 38/100 over 556 records in the last 180 days details
References
Impacted products
Vendor Product Version CPE status
rocq-prover rocq Affected: unknown
guessed Create a notification for this product.
Credits
Jonathan Brossard
Relationships
analysis GCVE-1988-2026-0444 (this record)
To clipboard 

{
  "containers": {
    "cna": {
      "affected": [
        {
          "product": "rocq",
          "vendor": "rocq-prover",
          "versions": [
            {
              "status": "affected",
              "version": "unknown"
            }
          ]
        }
      ],
      "credits": [
        {
          "lang": "en",
          "type": "finder",
          "value": "Jonathan Brossard"
        }
      ],
      "descriptions": [
        {
          "lang": "en",
          "value": "1. Summary\n==========\nA soundness bug in the Rocq (formerly Coq) kernel\u0027s guard checker allows\nconstruction of a checked proof of False \u2014 and by extension, any\nproposition, including 0 = 1.\nThe guard checker does not recheck the recursive tree (rectree) for an\ninductive type parameter after a transport (rewrite via eq_rect/rew)\nchanges that parameter. A fixpoint applies a rewrite along a type\nequality to its recursive argument; the checker accepts this because the\ninductive type is preserved, but the rectree is corrupted. A second\nfixpoint that calls the first inherits the corrupted tree without\nverification, so a non-structurally-decreasing call passes as\nterminating.\nThis is a 0-day: no fix has been merged as of Rocq 9.2.0.\n2. Context\n==========\nRocq (formerly Coq) is the reference implementation of the Calculus of\nInductive Constructions and one of the most widely deployed proof\nassistants. Its kernel is the trusted core that checks every proof\nbefore acceptance. A soundness bug in the guard checker \u2014 the component\nthat enforces termination of recursive definitions \u2014 undermines the\nguarantees of any system built on Rocq-checked proofs.\nFormally verified systems certified under Common Criteria (ISO 15408) or\nDO-178C (airborne software) derive their assurance from the correctness\nof the proof checker. A kernel-level bypass invalidates that assurance\nchain.\n3. Impact\n=========\n- Formally verified compilers (CompCert)\n- Verified OS kernels (CertiKOS)\n- Separation logic frameworks (Iris)\n- Mathematical libraries (MathComp)\n- Proof-carrying code: a malicious .v file in a dependency could\nintroduce unsound declarations\n- Verified smart contracts (ConCert)\n4. Proof of Concept\n===================\nA Docker-reproducible PoC is available:\ngit clone https://github.com/endrazine/rocq-cve-poc-22024\ncd rocq-cve-poc-22024\ndocker build -t rocq-cve-poc-22024 .\ndocker run --rm rocq-cve-poc-22024\nThe PoC uses two axioms (e : nat = nat, and e1 : rew [fun T =\u003e T] e in\n0 = 1) that are consequences of univalence and are consistent with the\nCalculus of Inductive Constructions. The proof of 0 = 1 exploits the\nguard checker flaw, not the axioms.\n5. Root Cause\n=============\nThe guard checker accepts a recursive call when the inductive type of\nthe argument is preserved, but it does not re-derive the rectree after\na transport (eq_rect / rew) changes the type parameter. The corrupted\nrectree is inherited by subsequent fixpoints without reverification.\nCWE-670: Always-Incorrect Control Flow Implementation.\n6. Scoring\n==========\nCVSS 3.1: AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N \u2014 7.1 (High)\nCVSS 4.0: AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N \u2014 6.8\n(Medium)\n7. CWE\n======\nCWE-670: Always-Incorrect Control Flow Implementation\n8. CVE\n======\nCVE-2026-72704 (assigned by VulnCheck as CNA)\n9. Affected Versions\n====================\nRocq Prover \u2264 9.2.0 (all versions including Coq 8.x)\nFixed in: UNFIXED \u2014 PR #22027 proposed but not merged.\n10. Mitigation\n==============\n- No patched version is available.\n- Run coqchk on compiled .vo files \u2014 coqchk may catch the inconsistency.\n- Audit dependencies for use of transport (rew / eq_rect) in fixpoint\ndefinitions with nested mutual recursion.\n11. References\n==============\nBug report:  https://github.com/rocq-prover/rocq/issues/22024\nFix (open):  https://github.com/rocq-prover/rocq/pull/22027\nPoC:         https://github.com/endrazine/rocq-cve-poc-22024\nVulnCheck:\nhttps://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trust...\nNVD:         https://nvd.nist.gov/vuln/detail/CVE-2026-72704\n12. Timeline\n============\n2026        Bug reported by Yann Leray (rocq-prover/rocq#22024)\n2026        Fix proposed (PR #22027) \u2014 not yet merged\n2026-08-24  CVE-2026-72704 published by VulnCheck\n2026-08-24  Docker-reproducible PoC published\n13. Credit\n==========\nBug discovery:   Yann Leray (@yannl35133)\nPoC packaging:   Jonathan Brossard (@endrazine) \u2014 MOABI / PSIRT.com"
        }
      ],
      "problemTypes": [
        {
          "descriptions": [
            {
              "cweId": "CWE-670",
              "description": "CWE-670",
              "lang": "en",
              "type": "CWE"
            }
          ]
        }
      ],
      "providerMetadata": {
        "dateUpdated": "2026-11-02T07:29:46Z",
        "orgId": "4e2abfbf-4a2a-4b76-a4e0-d77c18ba156c",
        "shortName": "VULNARCHIVE"
      },
      "references": [
        {
          "tags": [
            "technical-description",
            "exploit"
          ],
          "url": "https://vuln.freearchive.org/archive/item/e1397407374b71428bf52966f1f06cf0a80f119990f1679b1418008ce2e9dc72"
        },
        {
          "tags": [
            "technical-description"
          ],
          "url": "https://lists.securityfocus.com/hyperkitty/list/bugtraq@bugtraq.ai/message/45SER5JXY2UO6A5CLBPEOWTV3K46KLTX/"
        },
        {
          "url": "https://github.com/endrazine/rocq-cve-poc-22024"
        },
        {
          "url": "https://github.com/rocq-prover/rocq/issues/22024"
        },
        {
          "url": "https://github.com/rocq-prover/rocq/pull/22027"
        },
        {
          "url": "https://nvd.nist.gov/vuln/detail/CVE-2026-72704"
        },
        {
          "url": "https://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trusts-corrupted-recursive-tree-after-transport"
        }
      ],
      "source": {
        "defect": [
          "74d8252f-d31e-4f51-9c22-11e05eef02a3%40gmail.com"
        ],
        "discovery": "EXTERNAL"
      },
      "title": "[Bugtraq] CVE-2026-72704: Rocq guard checker trusts corrupted recursive tree after transport (0 = 1 demonstrated) \u2014 0-day",
      "x_gcve": [
        {
          "recordType": "analysis",
          "relationships": [
            {
              "destId": "CVE-2026-72704",
              "type": "related"
            }
          ],
          "vulnId": "GCVE-1988-2026-0444",
          "x_vulnarchive": {
            "archiveUrl": "https://vuln.freearchive.org/archive/item/e1397407374b71428bf52966f1f06cf0a80f119990f1679b1418008ce2e9dc72",
            "automated": true,
            "contentSha256": "e1397407374b71428bf52966f1f06cf0a80f119990f1679b1418008ce2e9dc72",
            "evidenceScore": 10,
            "messageId": "74d8252f-d31e-4f51-9c22-11e05eef02a3%40gmail.com",
            "originalUrl": "https://lists.securityfocus.com/hyperkitty/list/bugtraq@bugtraq.ai/message/45SER5JXY2UO6A5CLBPEOWTV3K46KLTX/",
            "policy": "vulnarchive-1",
            "sourceFormat": "text/html",
            "sourcePublishedAt": "2026-11-02T07:29:46Z"
          }
        },
        {
          "recordType": "advisory",
          "vulnId": "gcve-1988-2026-0444"
        }
      ]
    }
  },
  "cveMetadata": {
    "assignerOrgId": "4e2abfbf-4a2a-4b76-a4e0-d77c18ba156c",
    "assignerShortName": "VULNARCHIVE",
    "datePublished": "2026-11-02T07:29:46Z",
    "dateUpdated": "2026-11-02T07:29:46Z",
    "state": "PUBLISHED",
    "vulnId": "GCVE-1988-2026-0444"
  },
  "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
How durations are calculated

Following the VTEM framework (Black Hat USA 2015), time to patch starts when the vendor or a coordinator was informed, total time to patch at discovery, and disclosure to patch at public disclosure; vendor response time runs from the report to its acknowledgement. Time to exploit and time unpatched start at the earliest discovery or report, falling back to public disclosure. Unpatched time ends at the first recorded patch, or the calculation time when no patch is recorded. Exploitation to patch shows the interval between those two events; a published proof of concept is a public exploit, not exploitation.

Each result shows its source dates. A negative interval means the end event came first; when date-only inputs leave the order open, the result says so. Date-only inputs are approximate. The earliest evidence wins: KEV report dates and sightings are labelled as such. Records describing another vulnerability are listed but never calculated from, and a PoC alone does not establish exploitation. Missing patch evidence does not prove that no patch exists. Filters below change the event list only.

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.