License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.32
URN: urn:nbn:de:0030-drops-184077
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18407/
Wang, Qinshi ;
Pan, Mengying ;
Wang, Shengyi ;
Doenges, Ryan ;
Beringer, Lennart ;
Appel, Andrew W.
Foundational Verification of Stateful P4 Packet Processing
Abstract
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.
BibTeX - Entry
@InProceedings{wang_et_al:LIPIcs.ITP.2023.32,
author = {Wang, Qinshi and Pan, Mengying and Wang, Shengyi and Doenges, Ryan and Beringer, Lennart and Appel, Andrew W.},
title = {{Foundational Verification of Stateful P4 Packet Processing}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {32:1--32:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18407},
URN = {urn:nbn:de:0030-drops-184077},
doi = {10.4230/LIPIcs.ITP.2023.32},
annote = {Keywords: Software Defined Networking, Verifiable P4, Stateful data plane programming}
}
