Tools and Algorithms for Network Verification
The lecture takes as starting point a recent surge in network verification. It highlights work from various research groups at Cornell (Foster et al), Princeton (Walker et al), UIUC (Godfrey et al), Stanford, (McKeown et al), Berkeley (Shenker et al), Texas Austin(Lam et al), Purdue (Rao et al), Naval Postgraduate school. (Xie et al), and many other groups including at Microsoft and present these results in a coherent way from the lens of 30 years of program verification (model checking, proof assistants, SAT solvers, automatic test generation programs like DART and Klee). Besides specific tools we survey some of the major ideas in verification such as symbolic model checking, abstraction and partial order methods to reduce state space explosion, and white and black box test generation. We will also present use cases of network verification in production environments, in particular Microsoft Azure where the theorem prover Z3 is used on a continuous basis for checking security policies and router configurations. Students will learn about verification methods and also about what is different about the domain that makes network verification different from standard verification in that old ideas have to be rethought. They will be exposed to new research directions and methods.
I have been at Microsoft Research since 2006 working in the area of Software Engineering, and in particular on developing a theorem prover, more specifically a Satisfiability Modulo Theories solver, called Z3. Before that I developed distributed file replication systems and remote file compression protocols in the core file systems group at Microsoft and in a startup, and prior to that I worked on program synthesis at Kestrel Institute and the Stanford Temporal Prover, studying with Zohar Manna. Z3 is now widely used as a foundation for software analysis and development tools. It received the 2015 ACM SIGPLAN Software Systems award and the most influential tool paper of the first 20 years of TACAS in 2014. In the past few years, I have devoted some attention to applying Z3 to Network Verification. Z3 is used to check all routers and access control policies within Microsoft Azure networks.