Comprehensive Verification of Packet Processing

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.