Title: Formal Verification of Distributed Network Control Planes
The control plane in many networks is a complex distributed system that runs various protocols for exchanging messages between routers and selecting paths for routing traffic. Errors in its configuration can lead to expensive outages or critical security breaches. The last decade has seen tremendous advances in applying formal methods to ensure correctness. In this talk, I will describe our efforts that started with a general-purpose symbolic model of the behavior of a network control plane. We encoded the stable states of a network as a satisfying assignment to a logic formula, and leveraged Satisfiability Modulo Theory (SMT) solvers to verify a wide variety of network correctness properties including reachability, fault-tolerance, router equivalence, and load balancing. Although this approach is very general and powerful, and works well for small-sized networks (a few hundred routers), there are scalability challenges. To address these, we embarked on a series of improvements that use key abstractions (symmetry abstractions, nondeterministic routing), abstract interpretation, and modular assume-guarantee reasoning. I will describe how these techniques successfully handle large-sized networks (several thousands of routers) that are in operation in modern data centers.
This talk describes joint work with Ryan Beckett, Ratul Mahajan, Divya Raghunathan, Timothy Alberdingk Thijm, and David Walker.