Checking Cloud Contracts in Azure
Staff - Faculty of Informatics
Start date: 17 February 2015
End date: 18 February 2015
The Faculty of Informatics is pleased to announce a seminar given by Nikolaj Bjorner
DATE: Tuesday, February 17th, 2015
PLACE: USI Lugano campus, room SI-003, Informatics building (Via G. Buffi 13)
TIME: 15:30
ABSTRACT:
Cloud Contracts capture architectural requirements in data-centers. They can be expressed as logical constraints over configurations. Contract violation is indicative of miss-configuration that may only be noticed when networks are attacked or correctly configured devices go off-line. In the context of Microsoft Azure's data-center we develop contracts for (1) network access restrictions, (2) forwarding tables, and (3) BGP policies. They are checked using the SecGuru tool that continuously monitors configurations in Azure.
SecGuru is based on the Satisfiability Modulo Theories solver Z3, and uses logical formulas over bit-vectors to model network configurations.
SecGuru is an instance of applying technologies, so far developed for program analysis, towards networks. We claim that Network Verification is an important and exciting new opportunity for formal methods and modern theorem proving technologies. Networking is currently undergoing a revolution thanks to the advent of highly programmable commodity devices for network control, the build out of large scale cloud data-centers and a paradigm shift from network infrastructure as embedded systems into software controlled and defined networking. Tools, programming languages, foundations, and methodologies from software engineering disciplines have a grand opportunity to fuel this transformation.
The talk covers joint work with Karthick Jayaraman and briefly mentions other developments in Network Verification with several other collaborators.
BIO:
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. 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. More information on Nikolaj is available from http://research.microsoft.com/~nbjorner
HOST: Prof. Natasha Sharygina
