Postmortem for Kernel Soundness Bug #14576
3 hours ago
- Lean内核中的一个健全性漏洞（#14576）被报告并修复，涉及嵌套归纳类型。
- 该漏洞允许通过幻影参数中的类型错误参数证明False，仅可通过元编程访问。
- 利用该漏洞需要官方内核和nanoda检查器中的两个独立漏洞；两者均已修复。
- 实际后果：独立内核检查需要两个检查器的当前版本。
- lean4lean受同一漏洞影响，因为它移植了参考实现。
- 去除元编程是错误的；内核必须独立拒绝类型错误的项。
- FRO行动包括回归测试、内核强化、AI辅助漏洞查找以及默认运行nanoda。