Basis 团队使用 LLM 辅助形式化验证了 Linux 内核中的 nftables 防火墙编译器。nftables 守护着几乎所有 Linux 机器的网络流量，其漏洞被视为最高严重级别。在 Rocq 定理证明器中进行验证的过程中，团队发现并修复了自 2022 年以来存在于所有 Linux 版本中的两个关键语义错误。经过验证的实现被证明不存在这些漏洞，而辅助实验表明单纯的 LLM 漏洞搜索无法发现其中较严重的一个。这项工作展示了 LLM 从「找 Bug」升级为「证明无 Bug」的可能性。
🔑 核心要点
使用 LLM 辅助 Rocq 定理证明器 验证 Linux nftables 防火墙编译器
发现自 2022 年以来 存在于所有 Linux 版本中的两个关键语义 Bug
nftables 是 几乎所有 Linux 机器 的默认防火墙，漏洞严重性最高
单纯 LLM 漏洞搜索 无法发现较严重的那个 Bug，证明了形式化验证的独特价值
展示了 LLM 从 「找 Bug」升级为「证明无 Bug」 的范式转变
💡 金句
LLMs have grown alarmingly capable at finding bugs. Formal verification offers the potential to produce proofs that entire classes of bugs are impossible.