2024/12/27 by Shengyi Wang, Wang, Shengyi, Pan, Mengying +2
Computer Science · Engineering · #Advanced Data Processing Techniques #Embedded Systems Design Techniques #F.3.1 #FOS: Computer and information sciences #Network Packet Processing and Optimization #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2412.19908
openalex publication_date 2024/12/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.