Nate Foster：验证可编程网络数据平面

我使用 OCaml 编程已经很久了，也很欣赏 Jane Street 支持的工具和工作。我想从 20 世纪 60 年代末最初的 ARPANET 拓扑，以及互联网背后的设计选择讲起。

早期架构师面临从电路交换电话网络转向分组交换的变化，还必须连接硬件和数据包格式各不相同的网络。他们设计的协议实现了这一点，以去中心化和稳健性为组织原则。

现代数据中心网络规模更大、复杂度更高。运营人员管理运行多种协议的数千台交换机，同时还要满足性能和复杂处理需求。一次故障可能在数据中心内级联，影响依赖公有云的服务。

运营人员采用了许多实用技术：高级策略语言生成设备配置，监控和分析工具检查配置，ping 和 traceroute 等工具探测网络行为。这些方法在大多数时候效果很好，但重大故障仍会发生。

我们能否将软件验证技术带入网络领域？或许可以自动检查连通性、冗余、隔离、转发环路和流量均衡。一位听众指出现代基础设施的去中心化程度有所降低；我区分了全球互联网和由单个组织拥有的大型网络，后者有不同的管理需求。

软件定义网络带来了新的机会。现在，抽象、API 和语言都有了相当精确的语义，因此我们可以考虑自动检查网络性质。我将介绍一款用于验证可编程数据平面的工具。

需要提醒的是：证明的价值取决于模型和假设。最近披露的无线协议漏洞说明，如果验证模型与现实不符，正确的形式化证明仍可能与端到端攻击并存。我们希望工具能联系真实实现，而不只是理想化模型。

我们与 Barefoot 的同事开发了这款工具，用来检查 P4 程序的性质。我会先介绍软件定义网络和 P4，再回顾程序验证，最后介绍工具。

传统网络设备有两个部分。控制平面运行软件和 BGP、OSPF 等协议，发现拓扑、计算路径并管理策略；数据平面则使用专用硬件执行这些决策，以高速转发数据包。

软件定义网络试图将数据包处理原语通用化，并将控制功能从设备中分离出来。控制器可以运行在普通服务器上，指挥多个数据平面；控制器集中部署很常见，但并非必要。这使得一些网络算法可以写成普通程序，而不必在每台设备上运行单独的分布式协议。

早期设想遇到了一个问题：OpenFlow 等常见标准在实际中暴露的数据平面功能不够丰富，而且很难获得交换机对复杂功能的支持。硬件设计者转而开发更可编程的数据平面，最终产生了能够用领域专用语言 P4 编程的高速芯片。

RMT 架构在流量管理器两侧各有一条流水线。解析器从进入的数据包中提取字段；入口阶段利用存储器、算术单元和状态进行处理。流量管理器调度流量，出口流水线可以在调度后修改头部，反解析器再重建输出的数据包。

P4 提供了为此类设备编程的更高级方式，也可以面向软件交换机和其他架构。它既有常见的类型和控制流，也有数据包解析器与匹配—动作表。设计目标是让每个数据包所需的工作量和时间可预测：状态有界，不支持指针和复杂数据结构，也排除了普通程序循环。

程序可能超出硬件资源而无法编译；但在我介绍的芯片上，成功编译的程序能以线速运行。这种可预测性是架构的核心，也使这些程序特别适合验证。

匹配—动作表指定要读取哪些字段、如何匹配，以及可以执行哪些动作。例如，对以太网源地址，表可以使用精确匹配，并选择学习动作或空操作：前者向控制平面发送摘要。表还可以指定默认动作和大小。

P4 程序定义的是表的模式，而不是实际表项。控制平面在运行时填入匹配规则和动作选择。当我们不知道表将如何填充而又想验证程序时，这种分工就很重要。

一个小型以太网交换机程序会声明头部和元数据，定义解析器与动作，并在入口和出口控制中连接各张表。标准语言和语义让数据包处理行为变得明确，而不是将其隐藏在设备专属配置中。

可编程性不只适用于传统交换。有一个项目在 Memcached 服务器前的交换机上部署了键值缓存。P4 程序解析请求并利用交换机内存保存缓存值；命中时立即返回，无须联系服务器。

可编程性也引入了新的错误。要推理整个网络的行为，我们需要理解每台设备，而 P4 程序可能有隐蔽的缺陷。头部可能无效，就像对象引用可能为空一样；访问无效头部可能产生未定义值。

动态有效性检查可能影响性能，这促成了这种不安全的语言设计，尽管我不喜欢未定义值。其他问题还包括未处理的异常、错误的元数据、解析与反解析不一致导致的数据包格式错误，以及绕过访问控制表的路径。

开源的 switch.p4 解析器展示了这种复杂性：其状态机约有 50 个状态，用来处理以太网、VLAN 标签栈、IPv4、IPv6 和隧道。没有 VLAN 标签的数据包会使相应头部无效；之后读取它可能产生未定义行为。类型系统并未精确描述所有这些有效性条件。

在演示中，我使用一个更小的 IPv4 路由器。它的解析器先提取以太网头部，再根据类型字段分支：IPv4 数据包会额外获得 IP 头部，其他以太网数据包则不带该头部继续处理。控制逻辑使用表进行路由和地址重写。

如果不指定要检查的性质，运行验证器会直接成功。启用头部有效性检查后则会失败，并产生反例：其中包含导致无效访问的解析器状态、数据包字段、表和动作的轨迹。第一个错误涉及仅含以太网头部的数据包的 IPv4 校验和。

我加入一个条件，使校验和处理只在 IPv4 头部有效时运行。第二个反例揭示了另一次没有保护条件的 IPv4 表访问。再加入有效性条件后，检查成功：现在所有被分析的路径都只访问有效头部。

另一项性质涉及指定输出端口或丢弃决定的标准元数据。该字段最初未定义，因此程序必须在流量管理器需要它之前完成设置。工具发现了一条到达入口处理末尾时仍未定义该字段的路径。

我添加一张表来丢弃相关的非 IPv4 数据包，并在 else 分支中调用它。验证随后成功。这个例子展示了自动插入的安全断言和易读的反例如何帮助加固一个虽小但可运行的路由器。

验证方法建立在 Hoare 和 Dijkstra 使用逻辑推理程序的工作之上。我们将 P4 转换为守卫命令这种理想化的命令式语言，并生成一阶逻辑公式。如果公式有效，在模型设定的条件下，断言和其他编码的性质就不会失败。

Hoare 风格的三元组关联前置条件、命令和后置条件。它表示：如果执行从满足前置条件的状态开始，且命令终止，那么结果状态满足后置条件。前置条件概括了这一结论所依赖的假设。

守卫命令语言包括表达式和逻辑公式、断言、假设、赋值、顺序执行以及非确定性选择。执行到断言时，它必须成立；假设则丢弃不满足条件的执行。假设为假会丢弃所有执行，因此必须谨慎对待假设。

普通条件语句可以表示为两个分支之间的非确定性选择：一个分支假设条件成立，另一个假设其否定成立。只有假设成立的分支才会贡献一条执行路径。这种小型语言足以表示我们需要的控制流。

最弱前置条件推理从命令和期望的后置条件出发，计算描述足够的初始状态的公式。如果初始状态满足该公式，且命令终止，后置条件就成立。这一计算是对程序进行语法转换。

断言对应合取，假设对应蕴含，赋值通过替换表达式处理，顺序执行组合各次变换，而选择要求两个分支都满足性质。直接转换可能生成指数级大小的公式，因此工具使用更高效的等价构造。

我们使用 Z3 SMT 求解器检查所得公式。将公式取反可以把有效性问题转化为可满足性问题：如果否定式不可满足，验证就成功；如果可满足，其模型就提供了反例，我们可以据此构造执行轨迹。

P4 程序只决定整体行为的一部分：它定义处理流水线和表模式，控制平面则提供表项。检查所有可能的表配置，可能会使依赖未声明控制平面假设的真实程序无法通过验证。我们需要明确描述这些假设。

以 switch.p4 中的 VLAN 解封装为例。不同动作分别移除零个、一个或两个标签，一张表读取头部有效性位来选择动作。我们希望表执行后，数据包不再有有效的 VLAN 头部。

不加假设时，这一性质无法成立：控制平面可能安装一条规则，对带两个标签的数据包选择空操作。预期行为依赖控制平面将每种有效性位模式与正确动作配对。要让证明具有我们期望的意义，就必须表达这种关系。

我们为程序插入额外的幽灵状态，称为 zombie state，用来记录表的调用、命中、动作和读取的数据。然后就可以声明假设，例如某张表命中，或带两个标签的数据包执行移除两个标签的动作，并在这些假设下验证数据平面。

实现使用 OCaml 和 Core、Async 等库；前端支持完整语言。工具能生成易读的反例，并包含扩展到大规模程序所需的优化。设计目标之一是尽量减少注解，让非专家也能使用。

内置标志可检查标准性质，例如头部访问有效和算术溢出。Foster 表示，经过优化，一个大型真实程序的检查可在远不到一分钟内完成。偶尔仍需添加的注解用于表达对驱动程序和控制平面的假设。

正在进行的工作包括从反例中合成控制平面假设、自动生成测试用例，以及检查 P4 程序不同版本之间的等价性或差异。限制假设语言的范围，可能使工具能够向程序员提出有用的假设。

更广泛地看，网络领域开始采用编程语言领域的技术，包括精确的抽象、编译器和运行时。重要的开放问题包括跨多设备和共享状态的推理、拥塞与负载均衡等量化性质，以及让不熟悉形式化方法的网络工程师也能使用的工具。

一位听众问演示是否只验证特定输入。我解释说，对于单个无状态设备，该工具会在模型范围内通过符号方式考虑每一种可能的执行。反例是失败的具体见证，并非唯一检查过的输入。

限制条件在于控制平面假设。我们会排除违反所述假设的轨迹，例如违反表命中或动作选择假设的轨迹。一种设想是在控制平面与数据平面的边界用运行时监控器检查这些假设，但我们尚未实现；另一种方法是由经过验证的控制平面保证它们成立。

被问到排队和状态时，我解释说流量管理器负责队列，P4 通过元数据与其通信。我们的工具可以推理这些元数据位，但不能直接证明加权公平排队或没有热点等分布性质。

更详细的分析需要编码输入数据包的分布及其对输出的影响。在演讲时，大多数目标设备使用固定功能调度；可编程数据包调度器的研究可能让调度算法验证成为有趣的未来方向。

一位听众问为何不用类型系统表达这些检查。我最初尝试过受类型化汇编语言研究启发的类型方法。现有 P4 程序依赖的某些不变量无法用简单的组合式类型系统捕获，因此对当前用户而言，基于程序逻辑的验证似乎更实用。

如果从头设计语言，一种类型安全、内存安全的数据包处理语言或许能高效地提供许多标准安全性质。当程序员超出类型系统能表达的范围时，可能需要更多注解或运行时检查。这会是一个很有吸引力的方向。

P4 通常不允许循环；解析器是例外，但实现一般会静态展开解析器循环，并拒绝无法适当确定边界的程序。这一限制是数据平面分析可行的原因之一。

类似的限制能否让控制平面易于验证？我对现有控制平面的全自动验证持怀疑态度。控制平面的软件栈比 P4 数据平面大得多，通常用 C 和 Java 等通用语言编写。从头设计或许能提供更好的抽象，但验证现有软件栈仍然困难。

最后，一位听众问所检查的性质如何表达。我们与 Barefoot 的工程师合作，找出反复出现的错误，再遍历程序的抽象语法树插入断言，例如在每次访问头部之前插入检查。目前这些遍历器是针对具体问题编写的，还不是用于表达性质的通用领域专用语言。