Config2Spec: Mining Network Specifications from Network Configurations
summary
Config2Spec automatically synthesizes a formal network specification from device configurations plus a failure model, combining data‑plane analysis and control‑plane verification to explore policies efficiently. Prototype (Python/Java) uses Batfish and Minesweeper, starts the candidate space from one data‑plane snapshot, and adaptively selects environments so it reaches a tight candidate set after ~37 environments instead of double for random sampling. It scales to ~150 routers and in experiments trims verifier work down to 3.5% of initial queries.
AI-written summary · about
chapters (8)
- 0:00The specification problem
- 2:25Introduction to ConvictSpec
- 4:12Data and control plane analysis
- 6:42Handling dense and sparse violations
- 9:00Hybrid optimization strategy
- 10:53Improving algorithmic efficiency
- 13:17Evaluation and results
- 17:31Conclusion and Q&A
related talks
12mMetha: Network Verifiers Need To Be Correct Too!
27mNetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion
16mConfig-Snob: Tuning for the Best Configurations of Networking Protocol Stack
16mTest Coverage for Network Configurations
19mComputing Precise Control Interface Specifications
22mIntroduction to Batfish for Automated Network Testing & Verification
15mStatic Detection of Silent Misconfigurations with Deep Interaction Analysis
25mDataplane equivalence and its applications