Lean内核中发现了一个严重的健全性漏洞（bug #14576），该漏洞允许类型不匹配的参数绕过类型检查系统。1这一bug存在于内核对嵌套归纳类型的处理机制中，只能通过metaprogramming访问，需要直接向内核发送归纳类型声明才能触发。1
事件的曝光始于7月25日，当时Ramana Kumar发布了包含虚假Collatz猜想证明的代码库。1三天后的7月28日，Kiran Gopinathan将其进一步化简为False证明，并正式开启issue #14576。1内核开发团队对此反应迅速，在报告后一小时内推送了修复补丁。1随后团队进行了多项后续加固工作，推送了包括#14582、#14607、#14608、#14609、#14613、#14615、#14616、#14621、#14631和#14632在内的多个修复PR。1
此外，OpenAI的Daniel Selsam协助内核团队利用AI安全专家发现了其他内核编程错误。1值得注意的是，Rust实现的独立内核nanoda中存在相关但不同的bug，该bug由Jeremy Chen报告并在Lean官方bug报告前一周被修复。1
A critical soundness vulnerability in the Lean kernel was discovered on July 25, exposing a flaw in how the system handles nested inductive types 1. The bug surfaced through an AI-assisted fake proof of the Collatz conjecture that Ramana Kumar published 1. On July 28, Kiran Gopinathan reduced the issue to a proof of False and opened issue #14576, revealing that ill-typed parameters could circumvent type validation, allowing unsound theorems to be accepted by the system 1.
The Lean kernel team responded swiftly, deploying a fix within one hour of the report through pull request #14577 1. The vulnerability required direct metaprogramming access to send inductive type declarations to the kernel, limiting its exploitability surface 1. Following the initial patch, the team implemented multiple hardening measures across subsequent pull requests #14582, #14607, #14608, #14609, #14613, #14615, #14616, #14621, #14631, and #14632 1. Daniel Selsam from OpenAI assisted the team by working with AI safety experts to identify additional kernel programming errors 1.
A related but distinct bug was discovered independently in nanoda, a Rust implementation of a separate kernel, by Jeremy Chen and was repaired one week before the Lean vulnerability became public 1.
评论
还没有评论，欢迎留下第一条。