Plankton: Scalable network configuration verification through model checking
summary
Plankton implements a prototype verifier that encodes the network control plane as an executable model and runs explicit-state model checking (SPIN) over a reduced SPVP protocol abstraction plus symbolic header partitioning; it adds state hashing, partial order reduction and policy-based pruning to cut irrelevant nondeterminism. The system verifies OSPF, BGP and static routing on industrial configs in seconds, handles single-link failures, and reports up to 10,000x speedup versus prior SMT-based tools.
AI-written summary · about
chapters (18)
- 0:00Intro
- 0:14Managing Enterprise Networks
- 0:54Goal: Network configuration verification
- 1:18Challenge: Difficult to model control plane execution
- 3:05Intuition 1: SMT is a bad fit for fast route computation
- 4:39Intuition 2: Not all non-determinism is consequential
- 6:09Explicit-state Model Checking
- 7:20Reduced Simple Path Vector Protocol
- 9:06Plankton Design Elements
- 9:30Plankton Optimizations
- 9:47Optimization: Partial Order Reduction
- 10:07Optimization 1: Prune inconsistent executions
- 12:30Optimization 2: Prioritize deterministic nodes
- 13:54Implementation and Evaluation
- 14:20Comparison with Minesweeper (No Link Failures)
- 14:53Comparison w/ Minesweeper single link failure
- 15:15Experiment Real-world network configurations
- 16:29Conclusion
related talks
01h 01mNetwork Verification: Past, Present, and Future
24mReal Time Network Policy Checking Using Header Space Analysis
28mBounded Model Checking of PLC ST Programs using Rewriting Modulo SMT
25mDataplane equivalence and its applications
29mSynthesis of dependable and self-driving communication networks
47mDeep Programmability: A New Lens on Networking
23mVeriFlow: Verifying Network-Wide Invariants in Real Time
21mModular Control Plane Verification via Temporal Invariants