Assuring Crypto Code with Automated Reasoning

Bugs in software are ubiquitous, but the impact of these bugs can vary widely. Sometimes they are largely benign, and at other times they can have catastrophic effects. Bugs in cryptographic software tend to be especially serious. To add to that, cryptographic algorithms are difficult to design and implement, requiring intricate and rare expertise. And even worse, such software operates in a context that can be assumed to be malicious, rather than random.

To achieve confidence of the correctness of cryptographic implementations in this context, we therefore need to apply a more rigorous testing standard. Ideally, we want to be able to test an implementation on all possible inputs. Fortunately, advances in automated reasoning technology, particularly in SAT and SMT solvers, makes exactly this approach possible, and even efficient.

This talk will describe the capabilities and operation of some open source tools that allow developers to conclusively and largely automatically determine whether a low-level cryptographic implementation, written in a language such as C, exactly matches a higher-level mathematical specification. We will particularly focus on work we have done to integrate these tools into the continuous integration system of Amazon's s2n implementation of TLS.