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

# 使用基于LLM的验证消除Linux网络栈中的漏洞 来源：https://www.basis.ai/blog/verified-nftables/ LLM在发现生产软件漏洞方面的能力已变得惊人地强大。这加剧了一个本已严峻的风险：我们许多关键基础设施都由软件中介，而这些软件中的每个漏洞都可能成为被利用的突破口。形式化验证通过生成证明来证明整类漏洞不可能存在，从而提供了缓解这一风险的潜力，但它实际使用有限，因为它需要稀缺、昂贵且专业的专家知识。幸运的是，LLM在验证方面也越来越有能力，这预示着未来关键软件基础设施将在构建时即具备安全性。 lean-zip的GitHub页面，这是一个在Lean 4中经过形式化验证的zlib实现：Lean的内核检查DEFLATE编码器和解码器互为逆操作。一张来自Leonardo de Moura的幻灯片，标题为"上个月，发生了一件意想不到的事情"：一个通用AI将zlib转换为Lean，并证明代码对所有可能的输入都是正确的。已测试。已证明。这被认为尚且不可能实现。 lean-zip (https://github.com/kim-em/lean-zip)，一个由松散监督的AI代理编写的经过形式化验证的zlib实现在这篇博文中，我们汇报了Basis在LLM引导验证实验中的结果。我们的目标是Linux网络栈的一个关键组件：nftables防火墙编译器和优化器，我们着手在Rocq定理证明器中对其进行验证。nftables就是这样一个关键基础设施。它过滤几乎所有Linux机器的流量，其中的漏洞被视为最高严重级别，因为一个过滤错误的防火墙会使它本应保护的每台机器都暴露在危险中。 在验证nftables的过程中，我们发现了**两个关键漏洞**，影响自2022年以来的所有Linux版本（这些漏洞已向维护者披露1 (https://www.basis.ai/blog/verified-nftables/#fn:1)）。我们的经过验证的实现被*证明是*没有这些改变语义的漏洞的，并且一个辅助实验表明，较严重的那个漏洞无法通过简单的LLM漏洞搜索发现。 我们的实验表明，生成证明和构建健壮的经过验证的系统所需的工作正变得越来越可自动化。本博文剩余部分将概述nftables、我们发现的漏洞，以及我们使用LLM验证关键网络软件的过程。 ## nftables及其漏洞快速入门 nftables是Linux操作系统提供的防火墙机制之一。你的操作系统接收到的每个数据包都会经过nftables，它决定哪些数据包被转发，哪些被丢弃。自2014年取代`iptables`成为每个主要Linux发行版的默认数据包过滤器以来，nftables如今保护着从家庭路由器到容器网络的一切；如果一台Linux机器过滤流量，那么几乎肯定是由nftables决定什么能通过。防火墙是大多数网络安全层的关键组件，其中的漏洞可能危及整个系统。一个经过验证的nftables实现将增加这个关键层的可信度。 ## nftables规则集和编译流水线 nftables的完整架构如下所示，包括一个用户空间CLI工具和一个内核模块： nftables的架构：虚线边界包围了nft cli工具，包含一个编译器和一个优化器，以及Linux内核内部的字节码执行器，数据包流经其中。`nftables`的架构。`nft` 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`命令行工具的正确性，并在这个过程中发现了系统中的两个漏洞。 ## 发现的漏洞 我们的主要发现是优化器在两个关键情况下*没有*产生等价程序： 1. 第一个漏洞是一个无效的优化，如果应用，会导致接受优化前本应被拒绝的数据包（！！）。 2. 第二个漏洞导致优化器将有效的规则集转换为无效的、被内核拒绝的规则集。 我们能够在最新版本的nftables用户空间工具中重现这些漏洞，并证明我们经过验证的重现实现完全没有这些改变语义的漏洞。 ### 漏洞1：位掩码字段的无效合并 第一个漏洞与一种优化有关，其中位掩码字段被合并。 数据包包含一系列控制标志位——例如，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`（`ACK`比特设置且所有其他比特清零）时才被丢弃。原始规则询问"这个比特是否被设置？"；合并后的规则询问"标志字节是否恰好等于这个比特，且所有其他位都清零？"同样的问题也适用于以这种比特测试形式匹配的任何位掩码类型字段。 这个漏洞特别有害，因为它悄无声息地将限制性策略转换为更宽松的策略，并可能产生*关键性*的安全影响：在前面的例子中，大多数syn和ack数据包会被丢弃，但优化后，只有*仅*设置了`SYN`或`ACK`比特的数据包才会被丢弃（数据包集合大幅缩小）。 ### 漏洞2：重叠范围无效合并 我们发现的第二个漏洞与一种基于地址合并规则的优化有关。 当连续规则匹配相同的字段时，`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 } `` 不幸的是，优化的实现存在一个漏洞，生成的映射是畸形的。具体来说，nftables要求一个`vmap`必须将每个地址映射到*一个*裁决：其键必须指向不重叠的区间。相反，在我们的例子中，优化器重用了原始范围而没有检查它们的不重叠性，因此键在`.120`–`.123`上重叠。因此，优化后，生成的规则集被拒绝，并显示错误`Error: conflicting intervals`。 这个漏洞导致一个有效的规则集被优化成无效的，从而在用户尝试安装优化后的规则集时引发错误。在这种情况下，安全考虑不太严重，但这仍然代表了一个不正确的优化，最终降低了人们对`nftables`的信任。 ## 形式化验证nftables 这两个漏洞都是在持续验证nftables用户空间组件的过程中由LLM自主发现的，即在证明`nft`保持规则集行为的同时发现的。 为了形式化证明一个实现具有这个属性，我们首先必须确定规则集的含义，然后根据该含义验证实现。 我们在Rocq定理证明器中形式化了四个部分： 1. nftables规则语言的语法和语义， 2. 内核执行的基于寄存器的字节码的语法和语义， 3. 从规则集到字节码的编译器，以及 4. 将规则集重写为更高效规则集的优化器。 部分（3）和（4）是我们入门中`nft`CLI工具两部分的经过验证的对等实现，部分（2）扮演内核字节码执行器的角色。 在形式化语义的基础上，我们陈述并证明了编译器和优化器都是保持语义的。也就是说，编译器生成的字节码接受和丢弃的数据包与输入规则集完全一致，优化后的规则集匹配的数据包与原始规则集完全一致： 交换图：规则集r在数据包上求值得出{accept, drop}中的裁决；编译r生成字节码b，该字节码在同一个数据包上执行得出相同的裁决。语义、编译器和证明由LLM生成。编译器的正确性属性。对数据包求值规则集并执行其编译后的字节码在同一个数据包上必须产生相同的裁决；优化器的属性是相同的方形，但两端都是规则集。两个部分位于证明之外：解析器，它将nftables规则集转换为Rocq AST，以及序列化器，它将字节码安装到内核中。两者都是未经验证的OCaml，打包在我们的`nftc_cli.exe`命令行工具中，该工具链接经过验证的编译器和优化器。 经过验证的实现仍在进行中，但已接近功能完善，约90%的nftables规则语言被建模和验证。LLM被用来编写经过验证的实现中的每个定义、代码行和证明。 ## 自主验证方法论 本节描述我们用来自动化开发的方法论。所有代码和证明均由运行在自动模式下的Claude CLI生成，使用Opus 4.8作为模型。 自主验证循环：一个详细的提示词供给实现LLM，它编写经过验证的nftables实现（规范、实现、证明）。一个审查LLM、一个VM测试框架和SPOT测试各自检查开发；报告的错误和测试不匹配反馈给实现LLM。自主验证循环。实现LLM编写规范、实现和证明；审查LLM、VM测试框架和SPOT测试用例检查其输出，它们的反馈驱动下一次迭代。LLM从一个详细的提示词开始，该提示词指定了验证器（在我们的案例中是Rocq）和要验证的nftables部分，并引用了先前关于形式化验证和网络的工作。提示词还阐明了我们希望LLM遵循的证明工程和通用工程实践，例如测试驱动开发和频繁的代码审查。 ## 测试框架 我们指示LLM使用`systemd-vmspawn`启动一个虚拟机（VM），并使用网络命名空间构建测试环境，在该环境中可以安装和在不同网络拓扑上测试nftables规则。VM还为LLM提供了一个沙箱，在其中运行官方的`nft`命令行工具并实验其行为。 在这个框架之上，我们运行了端到端差异测试：一组规则集同时输入到我们的经过验证的编译器和官方的nftables实现中，并比较它们的输出。 ## 对抗性工作流 开发通过两个LLM之间的对抗性循环进行：一个编写规范、实现和证明，另一个针对特定类型的缺陷进行审查并报告发现。循环继续，直到审查LLM确信该类型的缺陷已得到妥善修复。 这个工作流特别有效地暴露了语言语义中的保真度问题，其中实现LLM过早地宣称成功，而实际上某个表达式的含义没有被精确建模（例如，将有副作用的表达式近似为纯表达式）。为了揭示这样的语义差距，我们用审查LLM实例化了对抗性模板，该LLM将经过验证的代码与nftables的实际C实现进行交叉检查，并标记出欠规范的问题。 ## 小证明定向测试（SPOT） 为了进一步压力测试语义，同时生成最终用户可以用于调试自己防火墙配置的工件，我们构建了特殊测试用例，其中LLM必须陈述并证明真实规则集的属性：要么是规则集符合用户意图的形式化证明，要么是展示意图被违反的反例。当一个规则集抵抗规范化和推理时，这表明语义还不够精确，可以改进。 ## 漏洞是如何被发现的？ 我们在这篇博文中包含的两个漏洞都是在开发过程中由LLM自主发现的。然而，比漏洞本身更有趣的是漏洞是如何被发现的。 两个漏洞发现的时间线。6月30日，提交69666ba：当合成规则集触发冲突区间时发现区间漏洞。7月2日，提交17c949a：发现位掩码漏洞，LLM添加了自己的正确合并并合理化nftables的折叠。7月14日，提交c786563：在提示解释其差异后确认位掩码漏洞。两个发现的时间线。实心点标记漏洞出现；虚线环标记差点失手，LLM看到了不合理的折叠并合理化它长达十二天。重叠区间漏洞是由于测试框架发现的。6月30日（`69666ba` (https://github.com/BasisResearch/verified-nftables/commit/69666ba)），LLM合成了一个人工规则集电池，旨在触发nftables的优化器重写，以便更好地理解其行为。框架通过两种优化器运行每个规则集，并将结果加载到内核中一个新网络命名空间内。当其中一个规则集在`nft`命令行上触发一个明显的失败（`conflicting intervals`）时，漏洞偶然被发现了。 然而，不合理的位掩码合并漏洞背后的故事要曲折得多。在提交`17c949a` (https://github.com/BasisResearch/verified-nftables/commit/17c949a)中，LLM添加了自己正确的位掩码合并优化版本。当连续规则匹配相同的位掩码字段时，它的优化器将它们折叠成一个