Network Verification: Calculus and solvers

We examine calculus and solvers for Network Verification. As starting point we take the SecGuru tool that checks network access restrictions in the Microsoft Azure public cloud infrastructure. The tool is based on the Satisfiability Modulo Theories solver Z3. SecGuru is also used for checking Network Invariants for data-centers that are deployed using Azure´s network architecture. In both cases SecGuru relies on a calculus of network configurations in order to capture intent and check these statically. SecGuru models network configurations using quantifier-free logical formulas over bit-vectors. We recall also other scenarios in the context of network verification. They use other fragments of logic and specialized engines for Datalog and quantifier reasoning in Z3. In each case, correctness assertions can be modeled and solved using logics that are supported in state-of-the art theorem provers. Based on our experiences we claim that Network Verification is an important and exciting new opportunity where formal methods and modern theorem proving technologies play an important role. Many formalisms that make it convenient to model scenarios from networking domain are already supported in modern solvers. On the other hand, networking provides an inspiration for additional formalisms that can be supported using new efficient data-structures and solving algorithms.