BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Colloquium : Network Verification in Microsoft Azure
DTSTART:20161031T161500
DTEND:20161031T173000
DTSTAMP:20260407T095715Z
UID:835dc8c779f9dd88c59e16614ce448424f581c88806cf762cfa58201
CATEGORIES:Conferences - Seminars
DESCRIPTION:By: Nikolaj Bjorner - Microsoft Research\n\nAbstract:\nModern 
 large-scale cloud infrastructures are inherently complex to configure and 
 deploy: Network access restrictions are enforced at multiple points\, forw
 arding and filtering policies are programmed or configured in various form
 ats 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 par
 tial specifications (e.g.\, a DNS port of a DNS server must be permitted i
 n firewall rules)\, and it is possible to formulate more comprehensive con
 tracts that capture how forwarding logic must be configured in data-center
 s. Many contracts can be captured in fragments of first-order logic. We de
 scribe a set of Network Verification tools based on the Satisfiability Mod
 ulo Theories solver Z3. The SecGuru tool checks cloud contracts in the Mic
 rosoft Azure public cloud infrastructure. SecGuru models network configura
 tions using quantifier-free logical formulas over bit-vectors. We also des
 cribe several techniques for checking reachability properties in networks.
  These techniques include using symmetries and surgeries for simplifying r
 eachability checking in large data-center networks and using trie-based da
 ta-structures to represent equivalence classes of IP forwarding networks. 
 We think that Network Verification is an important and exciting new opport
 unity where formal methods and modern theorem proving technologies play an
  important role.\n\nBio:\nNikolaj Bjorner is a Principal Researcher at Mic
 rosoft Research\, Redmond\, working in the area of Automated Theorem Provi
 ng and Software Engineering. His current main line of work with Leonardo d
 e Moura  and Christoph Wintersteiger is around the state-of-the art theor
 em prover Z3\, which is used as a foundation of several software engineeri
 ng tools. Z3 received the 2015 ACM SIGPLAN Software System award and most 
 influential tool paper in the first 20 years of TACAS in 2014. Previously\
 , he developed the DFSR\, Distributed File System - Replication\, and Remo
 te Differential Compression protocols\, RDC\, part of Windows Server since
  2005 and before that worked on distributed file sharing systems at a star
 tup\, and program synthesis and transformation systems at the Kestrel Inst
 itute. He received his Master’s and Ph.D. degrees in computer science fr
 om Stanford University\, and spent the first few years of university at DT
 U and DIKU.\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR