Abstract interpretation of distributed network control planes
Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
Abstract
and Intentionet, USA DAVID WALKER, Princeton University, USA The control plane of most computer networks runs distributed routing protocols that determine if and how traffic is forwarded. Errors in the configuration of network control planes frequently knock down critical online services, leading to economic damage for service providers and significant hardship for users. Validation via ahead-of-time simulation can help find configuration errors but such techniques are expensive or even intractable for large industrial networks. We explore the use of abstract interpretation to address this fundamental scaling challenge and find that the right abstractions can reduce the asymptotic complexity of network simulation. Based on this observation, we build a tool called ShapeShifter for reachability analysis. On a suite of 127 production networks from a large cloud provider, ShapeShifter provides an asymptotic improvement in runtime and memory over the state-of-the-art simulator. These gains come with a minimal loss in precision. Our abstract analysis accurately predicts reachability for all destinations for 95% of the networks and for most destinations for the remaining 5%. We also find that abstract interpretation of network control planes not only speeds up existing analyses but also facilitates new kinds of analyses. We illustrate this advantage through a new destination "hijacking" analysis for the border gateway protocol (BGP), the globally-deployed routing protocol.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 15dc51b5-0752-4281-ab1f-7de28e9adf2cCited by top-tier papers14
- Lightyear: Using Modularity to Scale BGP Control Plane VerificationAlan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman et al.SIGCOMM 2023 · 33 citations
- NV: an intermediate language for verification of network control planesNick Giannarakis, Devon Loehr, Ryan Beckett, David WalkerPLDI 2020 · 31 citations
- Modular Control Plane Verification via Temporal InvariantsTimothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David WalkerPLDI 2023 · 22 citations
- Crescent: Emulating Heterogeneous Production Network at ScaleZhaoyu Gao, Anubhavnidhi Abhashkumar, Zhen Sun, Weirong Jiang et al.NSDI 2024 · 15 citations
- Hydra: Effective Runtime Network VerificationSundararajan Renganathan, Benny Rubin, Hyojoon Kim, Pier Luigi Ventre et al.SIGCOMM 2023 · 11 citations
Related papers
- S2: A Distributed Configuration Verifier for Hyper-Scale NetworksDan Wang, Peng Zhang, Wenbing Sun, Wenkai Li et al.SIGCOMM 2025 · 3 citations
- Expresso: Comprehensively Reasoning About External Routes Using Symbolic SimulationDan Wang, Peng Zhang, Aaron Gember-JacobsonSIGCOMM 2024 · 7 citations
- REAL: Emulating Control Plane at Simulator's CostZe Xia, Hao Li, Jinyu Fu, Xin Wan et al.NSDI 2026 · 2 citations
- Differential Network AnalysisPeng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang et al.NSDI 2022
- Nüwa: A Generative Control Plane for AI Network SimulationWenkai Li, Ran Shu, Peng Zhang, Yiren Zhao et al.SIGCOMM 2026
