2026-07-22T02:02:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18407 2024-03-06T11:01:49Z ddc:004 open_access

Foundational Verification of Stateful P4 Packet Processing Wang, Qinshi Pan, Mengying Wang, Shengyi Doenges, Ryan Beringer, Lennart Appel, Andrew W. Software Defined Networking Verifiable P4 Stateful data plane programming P4 is a standardized programming language for the network data plane. But P4 is not just for routing anymore. As programmable switches support stateful objects, P4 programs move beyond just stateless forwarders into new stateful applications: network telemetry (heavy hitters, DDoS detection, performance monitoring), middleboxes (firewalls, NAT, load balancers, intrusion detection), and distributed services (in-network caching, lock management, conflict detection). The complexity of stateful programs and their richer specifications are beyond what existing P4 program verifiers can handle. Verifiable P4 is a new interactive verification framework for P4 that (1) allows reasoning about multi-packet properties by specifying the per-packet relation between initial and final states; (2) performs modular verification, especially providing a modular description for stateful objects; (3) is foundational, i.e., with a machine-checked soundness proof with respect to a formal operational semantics of P4_{16} (the current specification of P4) in Coq. In addition, our framework includes a proved-correct reference interpreter. We demonstrate the framework with the specification and verification of a stateful firewall that uses a sliding-window Bloom filter on a Tofino switch to block (most) unsolicited traffic. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Qinshi Wang and Mengying Pan and Shengyi Wang and Ryan Doenges and Lennart Beringer and Andrew W. Appel 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.32 urn:nbn:de:0030-drops-184077 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.32 eng https://creativecommons.org/licenses/by/4.0/legalcode