Comprehensive Verification of Packet Processing

TL;DR

This paper introduces a comprehensive formal verification framework for P4-programmable switches, covering control, parsing, deparsing, and other switch components to ensure overall correctness of packet processing.

Contribution

It presents the first unified framework to verify both P4 control logic and additional switch components, enabling complete correctness proofs of switch behavior.

Findings

Verified correctness of packet-stream behavior in two P4 applications

Framework allows composition of proofs for control and switch components

First to enable end-to-end switch behavior verification

Abstract

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.