Abstract Interpretation of distributed network control planes

Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker

Research output: Contribution to journalArticlepeer-review

21 Scopus citations


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.

Original languageEnglish (US)
Article number42
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
StatePublished - Jan 2020

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality


  • Abstract Interpretation
  • Distributed Routing Protocols
  • Network Control Plane
  • Network Reliability
  • Network Simulation
  • Network Verification
  • Router Configuration Verification


Dive into the research topics of 'Abstract Interpretation of distributed network control planes'. Together they form a unique fingerprint.

Cite this