Network Verification: Past, Present, and Future
summary
A program-verification approach targets real router code written in P4: a verifier called p4v translates P4 to guarded commands, uses a small DSL to model control-plane table constraints, and checks safety with an SMT backend; it analyzes ~6,000-line programs in roughly a minute, finds about 10 real bugs in customer code, and hits one Z3 out-of-memory on a pathological virtualizer. A complementary tool models whole-network probabilistic failover as symbolic Markov chains and verifies F10-style data‑center resilience quantitatively.
AI-written summary · about
chapters (30)
- 0:00Intro
- 1:59Entanglement
- 2:43Diagnosis: No Semantics!
- 4:22What's Different? Why now?
- 15:04SDN Control Plane The brain of the network, it responds to network events by reconfiguring switches
- 15:51This is Partial Evaluation!
- 18:34Conventional Validation
- 20:12Programmable Data Plane
- 22:25Anatomy of a P4 Program
- 24:16P4 Machine Model
- 26:00Running Example: Firewall
- 27:13Let's add 4in6 tunneling!
- 31:13A peek behind the curtain...
- 34:08Common Properties
- 35:07Challenge #1: Imprecise Semantics
- 38:54Symbolic Control Plane
- 39:41Annotation Burden
- 40:22Scaling Up Not using compositional vertication
- 42:28Evaluation: Header Validity
- 43:41Evaluation: switch.p4
- 45:15From Devices to Networks
- 46:39Probabilistic Verification
- 47:42Challenge: Infinite Paths
- 48:40Semantics via Markov Chains
- 50:12Case Study: Topology
- 50:40Case Study: Routing Schemes We implemented F10 as a series of refinements
- 51:16Case Study: k-resilience
- 52:02Case Study: Delivery Probability
- 52:30Open Problems Traditional Control Planes
- 55:24Challenge #2: Control-Plane Model
related talks
18mLiveness Verification of Stateful Network Functions
25mFormal Verification of a Software Defined Delay-Tolerant Network
15mOn Temporal Verification of Stateful P4 Programs
47mDeep Programmability: A New Lens on Networking
01h 08mThe Network is the Computer: A Programming Language Perspective
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
20mPlankton: Scalable network configuration verification through model checking
23mVeriFlow: Verifying Network-Wide Invariants in Real Time