CS-ECE Distinguished Seminar Series: Verifying and Repairing Network Control Planes

A computer network's control plane governs how the network forwards data. Typical control planes are composed of several routing protocols spread across many routers and switches that compute paths for network flows in a distributed fashion. Computer networks play a critical role in the Internet infrastructure, and the control plane in particular is used as a vehicle to impose various communication policies. These include: who can/not communicate for security or compliance reasons, which flows to isolate, what performance classes to associate with different communication flows, etc. Unfortunately, control planes are often complex and bugs can easily creep in. Crucially, many bugs manifest only under unexpected failures. As such, networks are routinely plagued with catastrophic problems, such as routing blackholes, isolation breaches, network overload, and unavailability of critical services. In this talk, I will survey recent advances in the exciting new areas of network verification and repair that aim to improve network control plane resilience. Inspired by ideas from formal methods, these techniques automatically verify whether networks satisfy important safety properties, and if not, they repair networks with minimal human involvement. I will present my group's work on a new control plane abstraction called ARC which can speed up verification by nearly two orders of magnitude (from hours or days to seconds), as well as the first control plane repair approach.