NetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion
summary
NetComplete autocompletes partial network configs by filling “holes” with concrete values and proving correctness via a constraint encoding of protocol semantics. It uses an SMT backend (Z3 SMT solver), scales with partial evaluation and counterexample-guided inductive synthesis for OSPF weights, and handles static routes, OSPF and BGP. Prototype (Python) outputs Cisco configs and synthesizes realistic network-wide changes of up to 200 routers in few minutes.
AI-written summary · about
chapters (10)
- 0:00Start
- 1:16Bgp Leaks
- 2:55Configuration Synthesis
- 5:35Configuration Sketches
- 8:42Bgp Synthesis
- 11:48Iterative Synthesis for the Bgp Protocol
- 11:59Partial Evaluation
- 13:32Bgp Propagation Graph
- 15:29Configure the Ospf Weights
- 18:33Evaluation
related talks
30mUsing Python to design, configure, and measure large-scale networks
21mFinding Network Misconfigurations by Automatic Template Inference
12mMetha: Network Verifiers Need To Be Correct Too!
18mNetKeeper: Enhancing Network Resilience with Autonomous Network Configuration...
21mConfig2Spec: Mining Network Specifications from Network Configurations
16mTest Coverage for Network Configurations
43mData Networks Neutrality with OpenConfig: Unveiling Challenges and Practical...
32mNetwork Automation: A Journey, Not a Destination