To prove the functional correctness of a P4 program running in a programmable network switch or smart NIC, prior works have focused mainly on verifiers for the "control block" (match-action pipeline). But to verify that a switch handles packets according to a desired specification, proving the control block is not enough. We demonstrate a new comprehensive framework for formally specifying and proving the additional components of the switch that handle each packet: P4 parsers and deparsers, as well as non-P4 components such as multicast engines, packet generators, and resubmission paths. These are generally triggered by having the P4 program set header or metadata fields, which prompt other switch components -- fixed-function or configurable -- to execute the corresponding actions. Overall behavior is correct only if the "configurable" components are, indeed, configured properly; and we show how to prove that. We demonstrate our framework by verifying the correctness of packet-stream behavior in two classic P4 applications. Our framework is the first to allow the correctness proof of a P4 program to be composed with the correctness proof for these other switch components to verify that the switch programming as a whole accomplishes a specified behavior.

翻译：为了证明在可编程网络交换机或智能网卡中运行的P4程序的功能正确性，先前的研究主要集中于针对"控制块"（匹配-操作流水线）的验证器。然而，要验证交换机是否按照预期规范处理数据包，仅证明控制块的正确性是不够的。我们提出了一种新的综合性框架，用于形式化地规范和验证交换机中处理每个数据包的附加组件：P4解析器和反解析器，以及非P4组件，如组播引擎、数据包生成器和重提交路径。这些组件通常由P4程序设置包头或元数据字段触发，从而促使交换机的其他组件——无论是固定功能还是可配置的——执行相应的操作。只有当"可配置"组件被正确配置时，整体行为才是正确的；我们展示了如何证明这一点。我们通过验证两个经典P4应用中的数据包流行为来演示我们的框架。我们的框架首次允许将P4程序的正确性证明与这些其他交换机组件的正确性证明相结合，从而验证整个交换机编程是否实现了指定的行为。