Visible to the public P4V: Practical Verification for Programmable Data Planes

TitleP4V: Practical Verification for Programmable Data Planes
Publication TypeConference Paper
Year of Publication2018
AuthorsLiu, Jed, Hallahan, William, Schlesinger, Cole, Sharif, Milad, Lee, Jeongkeun, Soulé, Robert, Wang, Han, Ca\c scaval, C\u alin, McKeown, Nick, Foster, Nate
Conference NameProceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication
ISBN Number978-1-4503-5567-4
Keywordscompositionality, Metrics, P4, programmable data planes, pubcrawl, resilience, Resiliency, Scalability, scalable verification, verification

We present the design and implementation of p4v, a practical tool for verifying data planes described using the P4 programming language. The design of p4v is based on classic verification techniques but adds several key innovations including a novel mechanism for incorporating assumptions about the control plane and domain-specific optimizations which are needed to scale to large programs. We present case studies showing that p4v verifies important properties and finds bugs in real-world programs. We conduct experiments to quantify the scalability of p4v on a wide range of additional examples. We show that with just a few hundred lines of control-plane annotations, p4v is able to verify critical safety properties for switch.p4, a program that implements the functionality of on a modern data center switch, in under three minutes.

Citation Keyliu_p4v:_2018