CVE-2026-72703

Full vulnerability record from the local CVENow database.

Description

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.

Severity

MEDIUM

CVSS score

6.8 (v4.0)

Vulnerability status

Deferred

Source identifier

[email protected]

Published

2026-08-24 20:17:18.240000

Last modified

2026-10-26 02:17:07.063000

View original CVE JSON

{
  "id": "CVE-2026-72703",
  "sourceIdentifier": "[email protected]",
  "published": "2026-08-24T20:17:18.240",
  "lastModified": "2026-10-26T02:17:07.063",
  "vulnStatus": "Deferred",
  "cveTags": [],
  "descriptions": [
    {
      "lang": "en",
      "value": "The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0."
    },
    {
      "lang": "es",
      "value": "El verificador de guardas en Rocq Prover trata un parámetro de un punto fijo mutuo anidado como uniforme sin examinar las llamadas entre los diferentes cuerpos de ese punto fijo. find_uniform_parameters en kernel/inductive.ml inspecciona solo las llamadas autorrecursivas, por lo que cuando ningún cuerpo se llama a sí mismo, la función concluye que cada parámetro es uniforme. Un parámetro que crece a través de una llamada cruzada de un cuerpo a otro, por lo tanto, mantiene la especificación de subtérmino que heredó del punto fijo envolvente, y una llamada recursiva protegida por esa especificación es aceptada aunque el argumento no sea estructuralmente menor. Una definición no terminante es admitida como estructuralmente decreciente, lo que produce un término cuyo valor es igual a su propio sucesor y, por lo tanto, una prueba de Falso, de la cual se deduce cualquier proposición. La prueba no requiere axiomas, plugins o banderas inseguras y Print Assumptions lo reporta como cerrado bajo el contexto global. Introducido en Coq 8.20 y corregido en Rocq 9.2.0."
    }
  ],
  "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": "8.20",
              "lessThan": "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-27T14:12:25.906004Z",
          "id": "CVE-2026-72703",
          "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-670"
        }
      ]
    }
  ],
  "references": [
    {
      "url": "https://github.com/endrazine/rocq-cve-poc-21682",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/rocq-prover/rocq",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/rocq-prover/rocq/issues/21682",
      "source": "[email protected]"
    },
    {
      "url": "https://github.com/rocq-prover/rocq/pull/21684",
      "source": "[email protected]"
    },
    {
      "url": "https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls",
      "source": "[email protected]"
    },
    {
      "url": "http://www.openwall.com/lists/oss-security/2026/10/26/4",
      "source": "af854a3a-2127-422b-91ae-364da2661108"
    }
  ]
}