ABSTRACT:

For this talk, I will recount our experience deploying services that leverage automated theorem proving to assure the availability and safety of Microsoft’s global Azure cloud network. In the first part of the talk, I will describe the Network Change Verification Service (NCVS), a system that safeguards all configuration changes to Azure’s physical datacenter networks. NCVS combines scalable and proactive simulation, emulation, and verification together with a rich specification language for describing network intent. In the second part of the talk, I will then elaborate on ongoing work to verify the correctness of Azure virtual networks that run atop the physical network. I will discuss the ZenGuru verification tool, along with its intermediate language Zen, that we use to model and efficiently verify connectivity between virtual network resources.

BIO:

Ryan Beckett is a researcher at Microsoft working in the area of network reliability. He graduated with his PhD from Princeton in 2018. While a graduate student, Ryan was a recipient of the Google Fellowship and his PhD thesis won the ACM dissertation honorable mention award as well as the SIGCOMM 2018 dissertation award in networking and the John C. Reynolds dissertation award in Programming Languages. His research interests lie primarily at the intersection of programming languages and networks, and he is broadly interested in topics spanning compilers, verification, static analysis, distributed systems, and networks. He has recently focused on improving network reliability by both designing higher-level abstractions for network automation as well as by applying ideas from formal methods to statically verify the correctness of network configurations.

Hosted by Professor Todd Millstein