Dataplane equivalence and its applications
summary
An algorithm called netdiff models dataplanes in SEFL and uses symbolic execution plus an SMT solver to check packet-by-packet equivalence, matching sets of outputs via maximum bipartite matching. It finds concrete counterexamples (for example a libvirt NAT rule that causes TCP to be dropped), uncovers five Neutron bugs and several config missteps, compares P4 reorderings and FIB updates, and scales to real snapshots (about 2000 OpenFlow rules <5 minutes).
AI-written summary · about
chapters (8)
- 0:00Start
- 0:24Network operation overview
- 2:06Writing policies is hard
- 3:11Dataplane equivalence
- 13:50Applications
- 15:39Verifying Openstack Neutron
- 16:41Example bugs
- 20:37Conclusions
related talks
17mDifferential Network Analysis
12mFlightplan: Dataplane Disaggregation and Placement for P4 Programs
38mDataplane networking acceleration with OpenDataplane
21mParDiff: Practical Static Differential Analysis of Network Protocol Parsers
24mReal Time Network Policy Checking Using Header Space Analysis
24mAutomatically Correcting Networks with NEAt
15mREAL: Emulating Control Plane at Simulator’s Cost
20mPlankton: Scalable network configuration verification through model checking