P4Check: Verification and Debugging for Stateful P4 Programs
Abstract
Programmable data planes increasingly rely on stateful P4 programs to implement complex in-network functions. However, verifying and debugging these programs remains challenging because stateful temporal violations can span multiple packets and different program locations. We introduce P4Check, a tool that combines temporal verification with statement-level debugging for stateful P4 programs. P4Check uses a single definitional interpreter to execute P4 programs symbolically for verification and concretely for counterexample replay. Its specification language combines observations made while processing individual packets with temporal properties over packet sequences. When verification refutes a property, P4Check concretely replays the counterexample to support interactive debugging. We evaluate the fidelity of its executable semantics and its ability to detect bounded violations in representative real-world P4 programs.
Tommaso Pacciani
PhD Candidate
