Talk Title: SMT-based Verification of Distributed Network Control Planes
The network control plane is a complex distributed system that runs various protocols for exchanging messages between routers and selecting paths for routing traffic. Errors in control plane configurations can lead to expensive outages or critical security breaches. The last decade has seen tremendous advances in applying formal methods to ensure their correctness.
In this talk, I will describe our logic-based approach that leverages 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 general and powerful, and works well for small-sized networks (with a few hundred routers), there are scalability challenges. I will then describe some recent improvements based on key abstractions and modular assume-guarantee reasoning that have enabled our SMT-based approach to successfully handle large-sized networks (with several thousands of routers), similar to those in operation in modern data centers.
This talk describes joint work with Ryan Beckett, Ratul Mahajan, Divya Raghunathan, Timothy Alberdingk Thijm, and David Walker.
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.