Abstract interpretation of distributed network control planes
Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了每一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper14
- Lightyear: Using Modularity to Scale BGP Control Plane VerificationAlan Tang, Ryan Beckett, Steven Benaloh, Karthick Jayaraman 等SIGCOMM 2023 · 被引用 33 次
- NV: an intermediate language for verification of network control planesNick Giannarakis, Devon Loehr, Ryan Beckett, David WalkerPLDI 2020 · 被引用 31 次
- Modular Control Plane Verification via Temporal InvariantsTimothy Alberdingk Thijm, Ryan Beckett, Aarti Gupta, David WalkerPLDI 2023 · 被引用 22 次
- Crescent: Emulating Heterogeneous Production Network at ScaleZhaoyu Gao, Anubhavnidhi Abhashkumar, Zhen Sun, Weirong Jiang 等NSDI 2024 · 被引用 15 次
- Hydra: Effective Runtime Network VerificationSundararajan Renganathan, Benny Rubin, Hyojoon Kim, Pier Luigi Ventre 等SIGCOMM 2023 · 被引用 11 次
相关 Paper
- S2: A Distributed Configuration Verifier for Hyper-Scale NetworksDan Wang, Peng Zhang, Wenbing Sun, Wenkai Li 等SIGCOMM 2025 · 被引用 3 次
- Expresso: Comprehensively Reasoning About External Routes Using Symbolic SimulationDan Wang, Peng Zhang, Aaron Gember-JacobsonSIGCOMM 2024 · 被引用 7 次
- REAL: Emulating Control Plane at Simulator's CostZe Xia, Hao Li, Jinyu Fu, Xin Wan 等NSDI 2026 · 被引用 2 次
- Differential Network AnalysisPeng Zhang, Aaron Gember-Jacobson, Yueshang Zuo, Yuhao Huang 等NSDI 2022
- Nüwa: A Generative Control Plane for AI Network SimulationWenkai Li, Ran Shu, Peng Zhang, Yiren Zhao 等SIGCOMM 2026
