Trail of Bits Blog·2026-09-09 19:00· 23 天前

Lean 4.33.1 及更早版本存在字符串切片漏洞，可“证明”费马大定理

A “proof” of Fermat’s Last Theorem that fits the margin

AI 导读

Lean 所有 4.33.1 及之前的稳定版本存在一个字符串切片漏洞，攻击者可借此制造矛盾并“证明”费马大定理。问题出在 String.Pos.Raw.extract：在超大位置提取一字节切片时，逻辑定义返回空字符串，而编译后的原生代码返回整个原字符串，两者不一致即可推出空串等于非空串。