CVE-2026-72711
中已发布
Lean 4 4.32.2 之前版本的内核接受带有未绑定自由变量的不透明声明
- 已发布
- 2026年8月24日
- 已更新
- 2026年10月26日
- 分配 CNA
- VulnCheck
- 观察到的证据
- 2026年10月26日
初级CVSS
6.8/ 10中
nvd · CVSS 4.0
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:X0.2%
低 · 未来 30 天
- 百分位
- 7.1%
- 型号日期
- 2026年10月25日
EPSS 是统计估计，而不是确定性或影响衡量标准。将其与 CVSS、KEV 状态、暴露程度和您的环境相结合。
总结
Lean 4 内核不检查 opaque 声明的主体是否闭合。`environment::add_opaque` 省略了定义和定理路径所执行的 `check_no_metavar_no_fvar` 调用，因此包含一个不在本地上下文中的自由变量的值不会被直接拒绝。元程序可以首先让内核创建一个类型为 `False` 的临时局部变量，并将其类型记录到类型检查器的推断缓存中，然后在该缓存条目仍保留于同一类型检查器实例上的情况下恢复局部上下文，最后提交一个 opaque 声明，其值就是此时已不再绑定的变量。缓存查找会在本应测试本地上下文成员资格的分支之前返回结果，因此内核推断出缓存中的类型，并接受一个类型为 `False` 的 opaque 常量，由此可以推出任何命题。该声明通过普通的受检查路径在最大内核检查级别下被接受，未使用 `sorry`、`unsafeCast`、`debug.skipKernelTC`、`addDeclWithoutChecking`、外部代码或被修改的 `.olean` 文件，且结果不携带任何公理。已在 4.32.2 中通过添加缺失的闭合检查修复。
来源
CVE-2026-72711 — Lean 4 内核健全性缺陷：推理缓存投毒
负责任的使用
仅在您拥有或有权测试的系统上使用漏洞信息。 Kitploit 链接到公共研究元数据，并且不存储漏洞代码或恶意负载。