Foundational Verification of Stateful P4 Packet Processing

Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 P416 (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.

Original languageEnglish (US)
Title of host publication14th International Conference on Interactive Theorem Proving, ITP 2023
EditorsAdam Naumowicz, Rene Thiemann
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772846
DOIs
StatePublished - Jul 2023
Event14th International Conference on Interactive Theorem Proving, ITP 2023 - Bialystok, Poland
Duration: Jul 31 2023Aug 4 2023

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume268
ISSN (Print)1868-8969

Conference

Conference14th International Conference on Interactive Theorem Proving, ITP 2023
Country/TerritoryPoland
CityBialystok
Period7/31/238/4/23

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Software Defined Networking
  • Stateful data plane programming
  • Verifiable P4

Fingerprint

Dive into the research topics of 'Foundational Verification of Stateful P4 Packet Processing'. Together they form a unique fingerprint.

Cite this