使用基于 LLM 的验证消除 Linux 网络栈中的 Bug

LLM 在发现生产软件中的 Bug 方面已经变得惊人地强大。这加剧了一个本已严重的问题：我们许多关键基础设施都由软件中介，而软件中的每一个 Bug 都是潜在的漏洞。形式化验证提供了通过生成证明来消除整类 Bug 不可能出现的潜力，但由于它需要稀缺且昂贵的专业知识，其实际应用受到限制。幸运的是，LLM 也越来越擅长验证，这指向了一个关键软件基础设施通过构造即安全的未来。

在这篇博客文章中，我们报告了在 Basis 进行的 LLM 引导验证实验的结果。我们的目标是 Linux 网络栈的关键组件：nftables 防火墙编译器和优化器，我们计划在 Rocq 定理证明器中对其进行验证。nftables 就是这样一种关键基础设施。它过滤几乎每台 Linux 机器的流量，其中的漏洞被视为最高严重级别，因为防火墙的错误过滤会暴露它本应保护的每一台机器。

在验证 nftables 的过程中，我们发现了两个影响自 2022 年以来所有 Linux 版本的严重 Bug（这些已向维护者披露1）。我们经过验证的实现被证明不存在这些改变语义的 Bug，而二次实验表明，其中更严重的那个不会通过简单的 LLM Bug 搜索被发现。

我们的实验表明，生成证明和构建健壮的已验证系统所涉及的工作正变得越来越可自动化。文章的其余部分将概述 nftables、我们发现的 Bug，以及我们使用 LLM 验证关键网络软件的过程。

nftables 及其 Bug 快速入门

nftables 是 Linux 操作系统提供的防火墙机制之一。操作系统接收的每个数据包都会经过 nftables，它决定哪些数据包被转发，哪些被丢弃。自 2014 年取代 iptables 成为每个主流 Linux 发行版的默认数据包过滤器以来，nftables 如今守护着从家庭路由器到容器网络的一切；如果 Linux 机器过滤流量，nftables 几乎肯定会决定什么能通过。防火墙是大多数网络安全层的关键组件，其中的漏洞可能危及整个系统。已验证的 nftables 实现将提高对这一关键层的安全保障。

nftables 规则集和编译流水线

nftables 的完整架构如下所示，由用户空间 CLI 工具和内核模块组成：

这个 CLI 工具将用户提供的策略序列作为输入，这些策略表示为有序的规则列表，其中每条规则匹配数据包的某些部分（源地址、目标端口、TCP 标志）并返回判决，即 accept 或 drop。例如，以下规则告诉 nftables 接受目标地址（daddr）为 192.168.50.1 或 192.168.50.2 的任何数据包。

ip daddr 192.168.50.1 accept
ip daddr 192.168.50.2 accept

nft 命令行工具解析这些规则集并将它们编译为紧凑的基于寄存器的字节码，然后将其加载到内核中。在那里，内核的解释器使用字节码为通过网络栈的每个数据包计算判决：要么通过防火墙接受它，要么丢弃它。

由于此字节码在系统看到的每个数据包上运行，它位于内核的热路径上，因此其效率至关重要。出于这个原因，CLI 工具还为源语言提供了一个优化器模块，该模块重写输入规则以更高效地运行（减少读取次数或删除冗余检查）。用户依赖优化器保证的一个关键安全属性是它保留输入规则的语义。换句话说，无论数据包是通过优化还是未优化的规则集传递的，为其计算的判决都应该相同。

我们着手证明 nft 命令行工具的正确性，并在此过程中发现了系统中的两个 Bug。

发现的 Bug

我们的主要结果是发现了优化器不生成等效程序的两个关键情况：

1. 第一个 Bug 是一个无效的优化，如果应用，将导致接受原本会被拒绝的数据包（!!）。

2. 第二个导致优化器将有效规则集转换为被内核拒绝的无效规则集。

我们能够在最新版本的 nftables 用户空间工具中重现这些 Bug，并证明我们已验证的重新实现完全不存在这些改变语义的 Bug。

Bug 1：位掩码字段的无效合并

第一个 Bug 与位掩码字段合并的优化有关。

数据包包含一系列控制标志位——例如，TCP 数据包有 SYN、ACK、FIN 等。

nftables 允许用户编写规则来测试特定位是否设置：tcp flags syn 匹配任何设置了 SYN 位的数据包。因此，以下规则集丢弃每个设置了 SYN 的数据包和每个设置了 ACK 的数据包：

tcp flags syn drop
tcp flags ack drop

优化器 nft -o 将这两条规则合并为一条：

tcp flags { syn, ack } drop

不幸的是，这个重写是不正确的。合并后的规则不表示相同的含义。

具体来说，nft 输入语言的语义被定义为集合查找是精确匹配测试：只有当数据包的标志字节正好等于 syn（设置了 SYN 位且所有其他位都清除）或正好等于 ack 时，数据包才会被丢弃。

原始规则询问“是否设置了此位？”；合并后的规则询问“标志字节是否正好等于此一位，其他所有位都归零？”相同的收窄适用于以这种位测试形式匹配的任何位掩码类型字段。

这个 Bug 特别有害，因为它会悄悄地将限制性策略转换为更宽松的策略，并可能产生严重的安全影响：在之前的示例中，大多数 syn 和 ack 数据包将被丢弃，但优化后，只有仅设置了 SYN 或 ACK 位的数据包才会被丢弃（一组小得多的数据包）。

Bug 2：重叠范围的无效合并

我们发现的第二个 Bug 与基于地址合并规则的优化有关。

当连续规则匹配同一字段时，nft -o 将它们合并为判决映射（vmap）——一个将字段值发送到转发判决的查找表。这将对字段的多次读取减少为一次读取，然后在字节码中跳转。

考虑一个丢弃一个源地址范围并接受另一个范围的规则集：

ip saddr 192.168.50.1-192.168.50.123 drop
ip saddr 192.168.50.120-192.168.50.255 accept

nft -o 将两条规则合并为：

ip saddr vmap { 
   192.168.50.1-192.168.50.123 : drop, 
   192.168.50.120-192.168.50.255 : accept 
}

不幸的是，优化的实现存在 Bug，生成的映射格式不正确。具体来说，nftables 要求 vmap 必须将每个地址映射到单个判决：其键必须引用不重叠的区间。相比之下，在我们的示例中，优化器在未检查其不相交性的情况下重用了原始范围，因此键在 .120–.123 上重叠。因此，优化后，生成的规则集被以错误 Error: conflicting intervals 拒绝。

这个 Bug 导致有效规则集被优化为无效规则集，以便当用户尝试安装优化后的规则集时，会向用户引发错误。在这种情况下，安全考虑不太严重，但这仍然代表了不正确的优化，并最终降低了人们对 nftables 的信任。

形式化验证 nftables

这两个 Bug 都是在持续努力验证 nftables 用户空间组件的过程中，由 LLM 自主发现的，也就是在证明 nft 保留规则集行为的同时。

要形式化证明实现具有此属性，我们首先必须确定规则集的含义，然后根据该含义验证实现。

我们在 Rocq 定理证明器中形式化了四部分：

1. nftables 规则语言的语法和语义，
2. 内核执行的基于寄存器的字节码的语法和语义，
3. 从规则集到字节码的编译器，以及
4. 将规则集重写为更高效规则集的优化器。

部分 (3) 和 (4) 是我们入门中 nft CLI 工具两半的已验证对应物，部分 (2) 扮演内核字节码执行器的角色。

基于形式化的语义，我们陈述并证明了编译器和优化器都是语义保持的。也就是说，编译器生成的字节码接受和丢弃的数据包与输入规则集完全相同，优化后的规则集匹配的数据包与原始规则集完全相同：

有两个部分位于证明之外：将 nftables 规则集转换为 Rocq AST 的解析器，以及将字节码安装到内核中的序列化器。两者都是未验证的 OCaml，打包在我们的 nftc_cli.exe 命令行工具中，该工具链接到已验证的编译器和优化器。

已验证的实现仍处于进行中，但已接近功能对等，~90% 的 nftables 规则语言已建模并验证。已验证实现中的每个定义、代码行和证明都是由 LLM 编写的。

自主验证方法论

本节描述了我们用于自动化开发的方法论。所有代码和证明都是由运行在自动模式下的 Claude CLI 使用 Opus 4.8 作为模型生成的。

LLM 从一个详细的提示开始，该提示指定了验证器（在我们的例子中是 Rocq）和要验证的 nftables 部分，并指向形式化验证和网络方面的先前工作。该提示还阐明了我们期望 LLM 遵循的证明工程和一般工程实践，例如测试驱动开发和频繁的代码审查。

测试工具

我们指示 LLM 使用 systemd-vmspawn 启动虚拟机 (VM)，并使用网络命名空间构建测试环境，在这些环境中可以安装 nftables 规则并在不同的网络拓扑上进行测试。VM 还为 LLM 提供了在其中运行官方 nft 命令行工具并试验其行为的沙箱。

在此工具之上，我们运行端到端差异测试：将规则集语料库提供给已验证的编译器和官方 nftables 实现，并比较它们的输出。

对抗性工作流

开发通过两个 LLM 之间的对抗循环进行：一个编写规范、实现和证明，另一个审查特定类型的缺陷并报告发现的内容。循环持续进行，直到审查 LLM 确信缺陷类型已正确修复。

这种工作流在暴露语言语义中的保真度问题方面特别有效，在这种情况下，实现 LLM 过早地声称成功，尽管表达式的含义没有被精确建模（例如，将有副作用的表达式近似为纯表达式）。为了揭示此类语义差距，我们用一个审查 LLM 实例化了对抗模板，该 LLM 根据 nftables 的实际 C 实现交叉检查已验证的代码，标记规范不足。

小型面向证明的测试 (SPOT)

为了进一步压力测试语义，同时生成最终用户可以应用于调试自己防火墙配置的工件，我们构建了特殊测试用例，其中 LLM 必须陈述并证明真实规则集的属性：要么是规则集捕获用户意图的形式化证明，要么是显示该意图可能被违反的反例。当规则集抵制规范和推理时，这表明语义还不够精确，可以改进。

如何发现这些 Bug？

我们在这篇博客文章中包含的两个 Bug 都是在整个开发过程中由 LLM 自主发现的。然而，比 Bug 本身更有趣的是如何发现这些 Bug。

重叠区间 Bug 是通过测试工具发现的。6 月 30 日（69666ba），LLM 合成了一组人工规则集，旨在触发 nftables 的优化器重写并更好地理解其行为。工具在新的网络命名空间内的内核中运行每个规则集通过两个优化器并加载结果。当其中一个规则集在 nft 命令行上引发大声失败（conflicting intervals）时，Bug 偶然出现。

然而，不健全的位掩码合并 Bug 的故事要精彩得多。在提交 17c949a 中，LLM 添加了自己健全版本的位掩码合并优化。当连续规则匹配同一位掩码字段时，其优化器将它们折叠为原始“是否设置了此位？”测试的 OR，而不是 nftables 的精确匹配集合。提交消息显示，LLM 已经意识到集合的精确匹配语义使其不适合合并位掩码类型表达式。然而，LLM 只用该不健全性来证明自己与 nftables 的分歧，而不是将其识别为 nftables 本身的 Bug。

实际上，根据提交消息，LLM 试图通过指出它正在合并的字段（数据包的连接跟踪状态 ct state）一次最多只能设置一位来合理化 nftables 的 Bug 合并行为。因此，合并的集合 ct state { new, established } 将数据包的连接跟踪状态与 new 或 established 的精确位进行比较是无害的，例如可以在 Arch Linux 默认规则集 中找到。

直到我们明确提示 LLM 在 7 月 14 日的提交（c786563）中解释其与官方优化器的分歧，Bug 才浮出水面。那时，LLM 终于意识到 nftables 的优化器确实会导致不健全的行为，因为还有其他位掩码类型表达式如 tcp flags 和 ct status，其中可以同时设置多个位，并通过 VM 测试工具确认了 Bug。形式化验证因此保护我们免受我们和 LLM 都未预料到的 Bug。

在发现这两个 Bug 后，我们进行了一个小实验，我们启动了一个新的 Claude 会话，并指示它使用相同的 VM 测试工具在官方 nftables 优化器中寻找 Bug。LLM 运行了几个小时，设法识别出 16 个 Bug，其中 3 个涉及静默改变语义，13 个涉及因无效优化规则而导致优化器崩溃。我们正在向维护者披露这些 Bug。

# original ruleset
ip daddr 1.1.1.0/24 
     ip daddr 1.1.1.5 accept
ip daddr 2.2.2.0/24
     ip daddr 2.2.2.5 accept

# after nft -o
ip daddr 1.1.1.0/24
   ip daddr { 
     1.1.1.5, 2.2.2.5
   } accept
# 2.2.2.5 can never match

Claude 是否设法找到了我们在验证工作中发现的两个 Bug？答案是否定的！虽然重叠区间 Bug 确实被 Claude 发现，但位掩码 Bug 在运行几个小时后仍然隐藏。实际上，从检查聊天历史来看，即使我们运行更长时间，LLM 也不太可能找到这个 Bug，因为它设法重现了能够触发优化器 Bug 的确切规则集，但发现新输出合理并决定继续。不同于 LLM 仅通过观察 Bug 输出规则就设法找到的 3 个静默 Bug，位掩码 Bug 需要对 nftables 语义含义的更深入理解。

最后，一个或许更令人鼓舞的结果是，已验证的实现不易受到 Claude 设法找到的 3 个优化 Bug 的影响。尽管已验证的实现仍在进行中，但 LLM 生成的语义捕获了足够多的 nftables，以用正确性定理拒绝那些 Bug 优化规则。更聪明的模型可能更擅长识别 Bug，但形式化验证确实为我们提供了更高级别的保障。

发现和观察

在这次初步验证工作的过程中，大部分人力投入在验证、审查和细化规范上。虽然失败的证明很容易消除，因为 LLM 会继续工作直到 Rocq 接受，但可能很容易错过一个被悄悄弱化的定理。

对于它不想做的工作，我们经常发现 LLM 会以某种随意阅读很容易错过的方式缩小任务。

我们看到了两种反复出现的形式：

1. LLM 用方便的前置条件弱化了其规范，以及
2. LLM 扭曲了系统的设计，使困难的引理永远不会出现。

用前置条件弱化定理

优化器的正确性定理提供了这种失败模式的代表性示例。

优化器实现的一部分需要生成新名称，这通常意味着在周围代码中穿插名称生成状态。

名称仅在重写具有副作用的规则（更新状态或修改数据包的规则）时需要。LLM 没有进行 plumbing，而是缩小了其定理必须说明的内容：

Theorem optimize_table_correct :
  forall n d c n' d' c' base p,
    optimize_table n d c = (n', d', c') ->
    rules_clean (c_rules c) = true ->
    … ->
    eval_chain c' (set_env p (env_with_sets base d'))
  = eval_chain c  (set_env p (env_with_sets base d)).

具体来说，微妙插入的 rules_clean 假设是一个仅对纯规则成立的谓词。有了这个限制，定理可以在没有 plumbing 基础设施的情况下被证明。定理仍被命名为 optimize_table_correct 并被证明正确，尽管该语句现在对具有副作用的规则什么也没说。

解析器中的寄存器分配

有时 LLM 会通过重塑规范定义本身而不是直接重塑定理来走捷径。寄存器分配实现就是一个例子：nft 编译器针对内核的基于寄存器的字节码解释器，因此在编译流水线的某个点，编译器必须分配寄存器。

LLM 试图通过用寄存器扩展源 AST，让解析器（位于已验证核心之外）分配它们来避免证明关于寄存器分配的引理。

这导致了一个难以理解的设计，其中部分分配发生在解析期间，但在 LLM 的证明义务方面，由于复杂逻辑外包给未验证的代码，编译器变得更容易验证。

结论

验证并不是什么新鲜事。几十年来，研究人员投入了大量劳动力来验证关键软件基础设施，并在此过程中经常发现关键 Bug。新的是这项工作现在正通过使用 LLM 变得越来越可自动化。虽然仍在进行中，但即使是我们在这个项目上的中期进展也可能需要数年的人力才能完成；在 LLM 的推动下，我们在几周内就达到了可工作的实现。我们获得了与传统验证相同的好处：我们正在努力构建一个内置正确性证明的重新实现，并在此过程中发现了 nftables 优化器中的关键 Bug。

然而，其中一些工作仍然是手动的。LLM 反复试图缩小任务范围并拖延具有挑战性的证明。我们开发中的大部分人力投入都用于捕捉这种行为。是否可以通过更复杂的工具或模型能力的进步来自动化最后一步仍有待观察。

我们打算自己找出答案。我们的下一个目标是一个完全自动化的流水线，一个无需人工参与即可大规模验证关键软件基础设施的流水线。