COPLAS talk: Checking Cloud Contracts in Azure – Københavns Universitet

COPLAS talk: Checking Cloud Contracts in Azure

COPLAS talk by Nikolaj Bjørner, Microsoft Research, Redmond, WA


Checking Cloud Contracts in Azure


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), though 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. In this context, we describe the SecGuru tool that checks cloud contracts in the Microsoft Azure public cloud infrastructure. The tool is based on the Satisfiability Modulo Theories solver Z3. SecGuru models network configurations using quantifier-free logical formulas over bit-vectors. SecGuru is an instance of applying technologies so-far developed for program analysis towards networks. We also describe several recent research directions in Network Verification at Microsoft Research. We think that Network Verification is an important and exciting new opportunity where formal methods and modern theorem proving technologies play an important role.


Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 is developed by Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger. Z3 received the 2015 ACM SIGPLAN Software System’s award, and the TACAS 20th anniversary most influential tool paper award. SecGuru is developed with Karthick Jayaraman from Microsoft Azure. Previously, he designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.

Hosts: Fritz Henglein (DIKU) and Michael Reichhardt Hansen(DTU)

Everyone are welcome. No registration required.