Nikolaj Bjorner is a Senior Researcher at Microsoft Research 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 many software engineering tools,
including test-case generation, smart fuzzing, static analysis, program
verification, software model checking, model-based software design and
synthesis. Previously, he designed the DFSR, Distributed File System - Replication,
shipped with Windows Server since 2005 and before that he worked on distributed file
sharing systems at XDegrees (a startup acquired by Microsoft), and program synthesis
and transformation systems at the research company Kestrel Institute. Nikolaj received
his Master's and Ph.D. degrees in computer science from Stanford University.
http://research.microsoft.com/en-us/people/nbjorner/

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Expert Audience

English

60 Minutes

Saarbrücken

SecGuru is a tool for automatically validating network connectivity
restriction policies in large-scale data centers. The problem solved by
SecGuru is acute in data centers offering public cloud services where
multiple tenants are hosted in customized isolation boundaries. Our tool
supports the following interactions: (1) given a policy and a contract
verify that the policy satisfies the contract (2) provide a semantic
difference between policies. The former facilitates property checking
and the latter facilitates identifying configuration drifts. We identify
bit-vector logic as a suitable basis for policy analysis and use the Z3
theorem prover to solve these constraints. We furthermore develop
algorithms for compact enumeration of differences for bit-vector
constraints. Finally, we evaluate SecGuru on large scale production
services where it has been used to identify and fix numerous
configuration errors.

Brigitta Hansen

0681 93039102

--email hidden

passcode not visible

logged in users only