Visible to the public Biblio

Filters: Author is Soulé, Robert  [Clear All Filters]
2019-06-28
Liu, Jed, Hallahan, William, Schlesinger, Cole, Sharif, Milad, Lee, Jeongkeun, Soulé, Robert, Wang, Han, Ca\c scaval, C\u alin, McKeown, Nick, Foster, Nate.  2018.  P4V: Practical Verification for Programmable Data Planes. Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication. :490-503.

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.