Formal Methods at Microsoft: Secure and Reliable Programs for Everyone, Everywhere

Abstract: The talk presents several research projects and tools from Microsoft Research and their impact on programming secure and reliable systems. As a common basis they take a formal methods angle where systems are viewed as mathematical objects. For the context of this talk we consider computation through lenses of calculi and measurements. We then describe how these research threads interleave with major developments from academic research and phase shifts in industry. With Microsoft rapidly pivoting on deploying and delivering AI products the talk relates the foundations with recent and current projects, including development of provably secure systems, securing smart contracts, network verification, efficient and correct compilation for ML systems, and programming systems and runtimes for interacting with AI.

Bio: Dr. Nikolaj Bjorner is a partner researcher at Microsoft Research. Nikolaj’s main line of work is around the state-of-the-art SMT constraint solver Z3. Z3 was developed with Leonardo de Mour:a, Lev Nachmanson and Christoph Wintersteiger. Z3 is used for program verification, test case generation among several applications. The work around Z3 has received several awards. Karthick Jayaraman and Nikolaj created the SecGuru tool that is used to validate firewalls and routing configurations for Microsoft Azure. In 2021 Nikolaj Bjorner was named an ACM Fellow