IMAG 206
28 March 2017 - 14h00
Network Verification for Microsoft Azure
by Nikolaj Bjorner from Microsoft Research
28 March 2017 - 14h00
Network Verification for Microsoft Azure
by Nikolaj Bjorner from Microsoft Research
Abstract: Modern large-scale cloud infrastructures are inherently complex to
configure and deploy: Network access restrictions are enforced at
multiple points, forwarding and filtering policies are programmed or
configured in various formats targeting devices that span different
vendors and generations. On the other hand, well-designed
infrastructures, such as Microsoft Azure, are based on a set of
transparent well-motivated principles. These principles can be captured
using a set of high-level contracts that can be enforced throughout the
life-cycle of a deployment. Contracts typically capture partial
specifications (e.g., a DNS port of a DNS server must be permitted in
firewall rules), and it is possible to formulate more comprehensive
contracts that capture how forwarding logic must be configured in
data-centers. Many contracts can be captured in fragments of first-order
logic. We describe a set of Network Verification tools based on the
Satisfiability Modulo Theories solver Z3. The SecGuru tool checks cloud
contracts in the Microsoft Azure public cloud infrastructure. SecGuru
models network configurations using quantifier-free logical formulas
over bit-vectors. We also describe several techniques for checking
reachability properties in networks. These techniques include using
symmetries and surgeries for simplifying reachability checking in large
data-center networks and using trie-based data-structures to represent
equivalence classes of IP forwarding networks. We think that Network
Verification is an important and exciting new opportunity where formal
methods and modern theorem proving technologies play an important role.
