Formal Verification at Google
COM3 Level 1
Multipurposed Hall 2, COM3 01-27
Abstract:
Software bugs in critical infrastructure can affect billions of users. Historically, we primarily relied on testing and fuzzing automation and manual review to find (many) bugs. But this approach cannot prove that there are no bugs left hiding in the code. Formal verification can. In this talk, I will explain how Google uses mathematical proof to build high-assurance software. Examples include machine-checked cryptographic code in BoringSSL using Rocq (Bedrock2, Fiat-Crypto), and a new assembly verification framework (Kraken) that we are developing in Lean. I will cover what works in practice, where some trade-offs are (performance, maintainability, trusting the toolchain) and which open problems still need solving.
Bios:
Before joining Google, Lukas spent two and a half years as a postdoctoral research fellow in the mathematics department at the University of Auckland, where he had also completed his PhD under the supervision of Steven D. Galbraith. His research there centred on arithmetic geometry, i.e. the interplay of number theory and algebraic geometry, with a particular focus on isogenies of abelian varieties, phenomena in positive characteristic, and the use of isogenies in post-quantum cryptography. Before pursuing mathematics, he studied theoretical physics at ETH Zurich, where he completed his Master.
Thyla leads Applied Cryptography and Formal Verification teams at Google. These teams are comprised of passionate individuals who care about helping everyone to use high-assurance cryptography correctly, and more broadly, about verifying Google’s security-critical code. Prior to joining Google, she served as the Managing Director of the Future Computing Laboratory at ETH Zurich, where she set up an industry-funded research centre focused on next generation computing technologies. Thyla also worked for Mozilla, helping to secure the Firefox browser, and has been involved in several cryptographic standardization initiatives at ISO and the IETF. Her PhD research involved formally verifying the TLS 1.3 protocol, contributing to the development of the TLS 1.3 standard.