© 2021 Strange Loop
Nearly everybody relies on cryptographic libraries such as OpenSSL, but how can we be sure that those libraries are implemented correctly? Formal verification offers an answer: we use mathematical reasoning to prove code behaves correctly on any input or message. Formal verification is an old idea, but new advances in automated reasoning mean we can now verify the highly optimised code that appears in cryptographic libraries. We may soon be able to verify these libraries end-to-end, and finally stop worrying about OpenSSL.
This talk will explore the tools, techniques, and insights we’ve built up through multiple cryptographic verification projects in industry. We’ll explore why formal verification is so hard, and why it works particularly well for cryptography. We’ll explain what it means for a piece of code to be formally verified, and how bugs can still occur in verified code. We’ll look forward and explain how we can reach the dream of fully verified cryptographic libraries that are still maintainable. Most importantly, we’ll discuss how successful techniques from cryptographic verification can be applied to other types of software systems.
Mike is a principal scientist at Galois Inc, focusing on cryptographic and distributed systems verification. He co-leads Galois' ongoing collaboration with AWS. He also co-leads Galois’ SPARTA project developing safe parsing technologies, and he leads Galois’ work on verifying blockchain and distributed systems protocols. Before joining Galois in 2017, Mike was an academic at the University of York, UK, and a Royal Society Industry Fellow.
Joey is a principal researcher at Galois Inc, focused on applying formal methods and automated reasoning to industry. He co-leads Galois’ ongoing collaboration with AWS. He also co-leads the verification effort that is a collaboration between Galois, Supranational, Ethereum Labs, and Protocol Labs. As a critical part of making those projects work, he also helps drive the direction of the SAW and Cryptol formal verification tools with a focus on making the tools more understandable and usable.