Title: Formal Verification of Distributed Network Control Planes

Speaker: Aarti Gupta    (bio) (bio)

Aarti Gupta is a Professor in the Department of Computer Science at Princeton University. She received a PhD in Computer Science from Carnegie Mellon University. Her research interests are in the areas of formal verification of programs and systems, automatic decision procedures, and electronic design automation. She has served on the technical program committees of many leading conferences, and is currently serving on the Steering Committee of the Computer Aided Verification (CAV) Conference. She has received several Best Paper Awards from leading conferences and journals and has been recognized as an ACM Fellow.

When: Tuesday, 07 June 2022 at 1900 hrs (IST)        

Abstract:
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.