Abstract Interpretation of Distributed Network Control Planes

Speaker(s) Aarti Gupta Princeton University
Date 11 May 2021 – 18:00 to 18:30
Venue INI Seminar Room 1
Session Title Abstract Interpretation of Distributed Network Control Planes
Chair Philippa Gardner
Event [VSOW03] Verified software: from theory to practice
Abstract

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 financial losses for service providers and significant hardship for users. Validation and verification can help find network configuration errors but existing techniques scale poorly on large industrial networks. We explore the use of abstract interpretation for verifying configurations, and build a tool called ShapeShifter for reachability analysis. On a suite of 127 production networks from a large cloud provider, ShapeShifter accurately predicts reachability for all destinations for 95% of the networks and for most destinations for the remaining 5%. We also use abstract interpretation to facilitate a new "hijacking" analysis for the border gateway protocol (BGP), a globally-deployed routing protocol. (This is joint work with Ryan Beckett, Ratul Mahajan, and Dave Walker.)

Supported By