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
- The internet is expected to become increasingly critical to modern computing, driven by network operators' demand for higher performance and sophisticated processing capabilities.
- Network outages involving configuration errors are predicted to occur every few years or occasionally within months, potentially triggering cascading failures that disrupt data centers and public cloud providers, resulting in financial and productivity losses.
- A paradigm shift occurring over the last decade has prompted the networking industry to reconsider network architecture and operational models, moving away from the original decentralized design toward more centralized or semi-coordinated structures.
- Software-defined networking (SDN) realization began approximately ten years ago, evolving from concepts with 20-year roots to include modern P4-programmable chips developed around three years ago.
- New RMT (Reconfigurable Match Table) chips are now capable of running P4 programs at line rate without variable performance characteristics, provided the programs do not exhaust memory resources.
- P4 programs face specific risks including undefined behavior from invalid header access, unhandled exceptions, packet metadata errors, parser/de-parser mismatches, and failures to implement security policies if packets bypass access control tables.
- The reference
switch.p4program, which implements a modern switch with roughly 50 states, may produce undefined values if packets lack expected fields such as VLAN tags. - A practical network verification tool developed with Barefoot over six months aims to connect directly to real implementations rather than idealized models, avoiding the need for pre-written formal specifications.
- The tool is projected to verify P4 programs up to tens of thousands of lines in under a minute using SMT solvers without requiring annotations.
- Future work plans include the automatic synthesis of control plane assumptions, exhaustive test case generation for P4 behavior, and the development of tools to decide program equivalence for differential testing.
- Researchers anticipate that within one or two years, new P4 features may emerge to support programmable scheduling algorithms.
- Verification efforts are expected to expand from simple reachability analysis to quantitative properties such as congestion and load balancing reasoning.
- A major weakness in wireless access point security was previously verified by CMU and Stanford with proofs that did not fully match real-world conditions, a gap recently highlighted by a CCS paper showing effective end-to-end security compromises.
- A separate effort at Barefoot involves building a chip-based cache to accelerate key-value store operations.
- The overarching goal is to make formal verification tools accessible to non-expert network engineers.