VeriFlow: Verifying Network-Wide Invariants in Real Time
summary
VeriFlow sits between controller and devices and intercepts controller-to-device updates, building per-update equivalence classes and per-class forwarding graphs to check invariants like loops, blackholes and ACL violations. Prototype integrates with NOX, Mininet and RouteViews/Rocketfuel traces on a 172-node topology and reports that 97.8% of updates are verified within one millisecond (typical case hundreds of microseconds); slow cases grow with the number of affected equivalence classes. An API exposes custom invariant checks.
AI-written summary · about
chapters (21)
- 0:00Intro
- 0:37Challenges in Network Debugging
- 1:24Effects of Network Errors
- 1:58Network Debugging Techniques
- 2:26Limitations of Configuration Verification
- 3:00Our Approach: Data-plane Verification
- 3:28Data Plane Verification in Action
- 4:08Can we run verification in real time?
- 5:05Our Tool: VeriFlow
- 5:41VeriFlow Operation
- 6:461. Limit the Search Space
- 8:02Computing Equivalence Classes
- 9:07Represent Forwarding Behavior
- 9:38Run Query to Check Invariants
- 9:57API to write custom invariants
- 11:16Performance Result 1
- 11:49Effect of Equivalence Class Count
- 12:45Experiment (cont.)
- 13:47Effect on Flow Table Update Throughput
- 14:22Effect of Multiple Header Fields
- 15:57Conclusion
related talks
01h 01mNetwork Verification: Past, Present, and Future
18mLiveness Verification of Stateful Network Functions
18mAPKeep: Realtime Verification for Real Networks
35mNetwork Flow Monitoring in Kubernetes with Contiv/VPP CNI and the Elastic Stack
16mEnabling Silent Telemetry Data Transmission with InvisiFlow
35mNetwork Flow Monitoring in Kubernetes with Contiv/VPP CNI and Elastic Stack
20mPlankton: Scalable network configuration verification through model checking
25mDataplane equivalence and its applications