« Volver al listado

CVE-2026-72844

Estado: AplazadaMedia (6.8)—

The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking.

Leer descripción completaMostrar menos

A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.

CVSS

Probabilidad de explotación (EPSS)

EPSS (Exploit Prediction Scoring System, de FIRST) estima la probabilidad de que una vulnerabilidad sea explotada en 30 días. Complementa a CVSS (impacto) y a CISA KEV (explotación confirmada).

Tecnologías afectadas (1)

⚠ Inferidas por IA a partir de la descripción — NVD aún no ha analizado esta CVE; no son CPE verificados.

Lean — Lean 4AI

CWE

Referencias

JSON original (NVD)

Mostrar
{
  "id": "CVE-2026-72844",
  "cveTags": [],
  "metrics": {
    "ssvcV203": [
      {
        "source": "134c704f-9b21-4f2e-91b3-4a467353bcc0",
        "ssvcData": {
          "id": "CVE-2026-72844",
          "role": "CISA Coordinator",
          "options": [
            {
              "exploitation": "poc"
            },
            {
              "automatable": "no"
            },
            {
              "technicalImpact": "partial"
            }
          ],
          "version": "2.0.3",
          "timestamp": "2026-08-21T21:13:48.944575Z"
        }
      }
    ],
    "cvssMetricV31": [
      {
        "type": "Secondary",
        "source": "disclosure@vulncheck.com",
        "cvssData": {
          "scope": "CHANGED",
          "version": "3.1",
          "baseScore": 6.3,
          "attackVector": "LOCAL",
          "baseSeverity": "MEDIUM",
          "vectorString": "CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N",
          "integrityImpact": "HIGH",
          "userInteraction": "REQUIRED",
          "attackComplexity": "LOW",
          "availabilityImpact": "NONE",
          "privilegesRequired": "NONE",
          "confidentialityImpact": "NONE"
        },
        "impactScore": 4,
        "exploitabilityScore": 1.8
      }
    ],
    "cvssMetricV40": [
      {
        "type": "Secondary",
        "source": "disclosure@vulncheck.com",
        "cvssData": {
          "Safety": "NOT_DEFINED",
          "version": "4.0",
          "Recovery": "NOT_DEFINED",
          "baseScore": 6.8,
          "Automatable": "NOT_DEFINED",
          "attackVector": "LOCAL",
          "baseSeverity": "MEDIUM",
          "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",
          "exploitMaturity": "NOT_DEFINED",
          "providerUrgency": "NOT_DEFINED",
          "userInteraction": "PASSIVE",
          "attackComplexity": "LOW",
          "attackRequirements": "NONE",
          "privilegesRequired": "NONE",
          "subIntegrityImpact": "NONE",
          "vulnIntegrityImpact": "HIGH",
          "integrityRequirement": "NOT_DEFINED",
          "modifiedAttackVector": "NOT_DEFINED",
          "subAvailabilityImpact": "NONE",
          "vulnAvailabilityImpact": "NONE",
          "availabilityRequirement": "NOT_DEFINED",
          "modifiedUserInteraction": "NOT_DEFINED",
          "modifiedAttackComplexity": "NOT_DEFINED",
          "subConfidentialityImpact": "NONE",
          "vulnConfidentialityImpact": "NONE",
          "confidentialityRequirement": "NOT_DEFINED",
          "modifiedAttackRequirements": "NOT_DEFINED",
          "modifiedPrivilegesRequired": "NOT_DEFINED",
          "modifiedSubIntegrityImpact": "NOT_DEFINED",
          "modifiedVulnIntegrityImpact": "NOT_DEFINED",
          "vulnerabilityResponseEffort": "NOT_DEFINED",
          "modifiedSubAvailabilityImpact": "NOT_DEFINED",
          "modifiedVulnAvailabilityImpact": "NOT_DEFINED",
          "modifiedSubConfidentialityImpact": "NOT_DEFINED",
          "modifiedVulnConfidentialityImpact": "NOT_DEFINED"
        }
      }
    ]
  },
  "affected": [
    {
      "source": "disclosure@vulncheck.com",
      "affectedData": [
        {
          "repo": "https://github.com/leanprover/lean4",
          "vendor": "leanprover",
          "product": "lean4",
          "versions": [
            {
              "status": "affected",
              "version": "0",
              "lessThan": "4.32.2",
              "versionType": "semver"
            },
            {
              "status": "unaffected",
              "version": "4.32.2",
              "versionType": "semver"
            },
            {
              "status": "affected",
              "version": "4.33.0-rc1",
              "versionType": "semver"
            }
          ],
          "defaultStatus": "unaffected"
        }
      ]
    }
  ],
  "published": "2026-08-20T18:16:45.290",
  "references": [
    {
      "url": "https://github.com/endrazine/lean-cve-poc",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://github.com/leanprover/lean4",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://github.com/leanprover/lean4/issues/14576",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://github.com/leanprover/lean4/pull/14577",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://github.com/xrchz/CollatzLean",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://www.openwall.com/lists/oss-security/2026/08/02/1",
      "source": "disclosure@vulncheck.com"
    },
    {
      "url": "https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections",
      "source": "disclosure@vulncheck.com"
    }
  ],
  "vulnStatus": "Deferred",
  "weaknesses": [
    {
      "type": "Secondary",
      "source": "disclosure@vulncheck.com",
      "description": [
        {
          "lang": "en",
          "value": "CWE-843"
        }
      ]
    }
  ],
  "descriptions": [
    {
      "lang": "en",
      "value": "The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency."
    }
  ],
  "lastModified": "2026-09-24T20:43:32.537",
  "sourceIdentifier": "disclosure@vulncheck.com"
}