Keynote: From C to Rust: a Software Verification Journey

ABSTRACT

In recent years, formal verification has gone mainstream: both major open-source projects and large companies have embraced verified code for better safety, security and reliability. Based on my experience, notably with the HACL* cryptographic library, I will draw some lessons on what makes a large-scale verification effort successful, and how to bring verified C code to industrial-grade projects such as Python or Firefox. I will then focus on a recent paradigm shift in the verification landscape: the embrace of Rust for the next generation of verification toolchains, and what it means for practitioners.

Author

Jonathan Protzenko is a Principal Researcher in the RiSE group at Microsoft Research Redmond. His research focuses on advancing the theory and practice of software verification, i.e. showing with mathematical certainty that a critical piece of code exhibits the intended behavior. This is important for the software industry (e.g. cryptography), but also for society at large (e.g. the law).

His joint work (with many wonderful collaborators!) has made it into the Linux kernel, the Python programming language, and the Firefox web browser, among others. His research on verified cryptography was featured in Quanta Magazine and IEEE Computer Magazine; my research on computational law appeared in Communications of the ACM.