Verification is Engineering
Presented as part of the 2020 HCSS conference.
|
In 2017, we gave a talk at HCSS on two formal Cryptography correctness proofs that we performed on Amazon Web Services production code. Those two proofs covered around 200 lines of security critical C. Since then, we have pushed our tools forward, and our proofs now cover nearly 3000 lines of AWS C code, including post-quantum algorithms. All of these proofs are included in the continuous integration system, meaning we have scaled our formal methods over both code size and real-world updating of the code that we’ve proved. This talk will discuss the techniques and technology needed for this 15x increase in verified code. One effect has been a huge increase in code change and proof maintenance cost. One proof in particular, our TLS handshake proof, sees particularly high development. This proof has two backup specifications that we never expect to change, so if the proofs break they can often be updated by developers, using the safety nets of the backup specifications to be sure that the desired properties still hold.
|
To address larger and more complicated code, we’ve made a number of changes to our verification tools. One of the most valuable has been an analysis to automatically generate “specification skeletons” which will often prove that code is free from undefined behavior at the push of a button. That proof can then be extended manually with functional correctness. We have also made numerous improvements to our tools to address the increasing demands of verification of post-quantum cryptography code.
The computational and memory demands of post-quantum cryptography dwarf those of most of the current algorithms in use. Unsurprisingly, verifying these algorithms also becomes significantly more challenging. In this talk, we will discuss some of the challenges to verification that we saw in two Cryptographic algorithms that we have verified, BIKE and SIKE. We will explain how we were able to overcome those limitations to arrive at the complete proofs that are running continuously today.
Joey Dodds is a Principal Researcher at Galois, where he focuses on commercial assurance efforts. He co-leads Galois’ efforts with Amazon’s AWS, working on verification projects including s2n, post-quantum cryptography and others. He has also led Galois’s implementation of the ElectionGuard protocol and cryptography. Recently he has been focusing on how Galois can continue to improve its commercial assurance offerings by making the tools and approaches we use both easier to use, and to understand.