Conference Presentation, Keynote, Lecture
Nate Foster: Verifying Network Data Planes
Jane StreetNate Foster, Bill Hallahan, JK Lee, Cole Schlesinger, Steffen Smolks, Robert Soule, Han Wang, Ron
- Nate Foster (Cornell Professor and OCaml programmer) presented a tool for verifying properties of P4 programs running on programmable data planes, developed in collaboration with Barefoot Networks.
- Modern enterprise networks (e.g., Facebook, Amazon) have evolved from the decentralized ARPANET model to complex, centralized topologies managed by autonomous systems, creating a critical need for automated verification to prevent cascading outages caused by configuration errors.
- Software-Defined Networking (SDN) decouples the control plane (software running on general-purpose CPUs) from the data plane (specialized hardware for high-speed packet forwarding), enabling centralized management but introducing new verification challenges.
- P4 is a domain-specific language designed to program the data plane; it ensures predictable performance by prohibiting complex data types, pointers, and loops, allowing constant-time execution on hardware like RMT (Reconfigurable Match-Table) chips.
- A key feature of P4 is the "match-action table," which defines how packets are processed based on header fields, though the table contents are filled by the control plane, creating a separation between program schema and runtime state.
- P4 includes safety hazards similar to C/C++, specifically "undefined behavior" when accessing invalid headers or uninitialized metadata, which can lead to catastrophic failures if not statically checked.
- Foster presented a verification tool that transforms P4 programs into "guarded commands" (an idealized imperative language) to generate first-order logic formulas for automated analysis.
- The tool utilizes the Sacks and Flanagan algorithm to compute weakest preconditions efficiently (quadratic or quartic complexity), avoiding the exponential blowup typical of standard weakest precondition calculus.
- Verification conditions are checked using the Z3 SMT solver; if the formula is unsatisfiable, the program is verified, whereas satisfiability yields a counter-example trace identifying the specific packet flow causing the error.
- The tool automatically converts P4's unsafe access to headers into safe assertions (using the
--failflag) to statically prove that all header accesses occur only on valid headers. - The system handles the separation between data plane and control plane by introducing "zombie state" (ghost state) to instrument the program with trace information, allowing verification to assume specific control plane behaviors (e.g., table entries will match specific VLAN tags).
- Current work focuses on three future directions: automatically synthesizing control plane assumptions, generating exhaustive test cases, and performing differential testing to verify equivalence between program versions.
- Unlike many formal methods tools, this system is designed for zero manual annotations, relying on SMT solver optimization to handle programs up to 20,000 lines of code within minutes.
- The presenter noted that while the approach works well for the finite-state, loop-free data plane, extending these techniques to the complex, large-scale control plane (often C-based) remains a significant challenge due to scale and lack of discipline.
- Future research aims to extend verification to quantitative properties like load balancing and queuing, contingent on future architectural changes that make packet schedulers programmable.