Synthesis of dependable and self-driving communication networks
summary
Claim: polynomial-time verification of MPLS label-stack reachability lets the tool check reachability and waypoint compliance under failures by modeling forwarding as a prefix-rewriting / pushdown-like system. Synthesis uses BDDs enumerating all failover routings to compactly represent alternative configurations and was evaluated on real operator topologies (including NorthernNet and European maps). Arborence decomposition yields provable k/2±1 resilience bounds; perfect/ideal resilience remains open. A verifier-guided synthesis loop with preliminary ML/GNN synthesis with verifier loop and genetic algorithms is explored but has no convergence guarantees yet.
AI-written summary · about
chapters (10)
- 0:00Dependable networks intro
- 1:27Human errors in outages
- 3:54Resilient network config
- 6:28Verification and synthesis
- 11:12Arborescence routing limits
- 13:17Verification complexity
- 15:50MLS label stack forwarding
- 19:49Push-down automata verification
- 21:55Self-driving networks and AI
- 24:08Q&A
related talks
01h 01mNetwork Verification: Past, Present, and Future
20mPlankton: Scalable network configuration verification through model checking
18mLiveness Verification of Stateful Network Functions
12mAvenir: Managing Data Plane Diversity with Control Plane Synthesis
47mDeep Programmability: A New Lens on Networking
12mMetha: Network Verifiers Need To Be Correct Too!
01h 04mInvited Talk: Finding Good Programs by Avoiding Bad Ones
20mContra: A Programmable System for Performance aware Routing