Presentation: Assuring Crypto Code with Automated Reasoning



11:50am - 12:40pm

Day of week:



Key Takeaways

  • Learn how to apply open-source tools to formally verify that software correctly implements a specification
  • Discover how cryptographic algorithms are defined and implemented, and how they can be proven formally correct
  • Apply the techniques to achieve worry-free refactoring


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.


What is the focus of your work today?

The talk will cover tools to help ensure that cryptographic code is correct with an extremely high degree of confidence, by comparing it to a trusted reference specification and against all inputs. It will also mention future plans to expand the scope of these tools beyond the cryptographic domain.

What does the talk cover?

I’ll be talking about an application of a technique known as formal methods. It’s like static analysis, but it’s sound, meaning that it covers all possible behaviours of a program rather than just looking for specific instances of common bugs.

I’m emphasising cryptography because we have results that show that it works really well for that particular domain. It works when you have a specification of what the software should do, which tend not to exist for most software. Cryptographic algorithms tend to have detailed specifications in standards documents published by organizations such as NIST, and therefore are an ideal target for correctness proofs.

In the long run, we expect these techniques to be applicable to a wider variety of software, but for this talk, we’ll be looking at the specific examples where we can demonstrate successful verification. We’ll talk about some of the widely used open-source libraries that we’ve analysed with this process.

What’s the motivation for your talk?

I want to raise awareness of two key points. First, that software that analyzes the structure of other software to determine whether it is correct, rather than just running it and inspecting the output, is feasible, and in fact quite practical for limited domains such as cryptography. Secondly, that we have developed a specific tool, the Software Analysis Workbench (SAW) that implements techniques of this sort.

How you you describe the persona of the target audience of this talk?

It would be most appropriate for advanced level people in the Architect, Tech Lead, or Developer roles, who are interested in using or implementing cryptography. I’m talking about techniques which would be of interest to a larger audience - they techniques could be used in other areas, for example - but the main impact will be in cryptographic environments.

Speaker: Aaron Tomb

Research Lead, Software Correctness @Galois

Dr. Tomb received his B.S., M.S., and Ph.D. in computer science from the University of California, Santa Cruz. His academic work focused on programming language theory, and particularly on the use of advanced programming language technology to improve software reliability. This involves type theory, automated reasoning, program analysis, and a bit of subjective exploration into what makes languages pleasant to use. At Galois, he leads projects focused on applied formal methods, with a particular emphasis on the verification of cryptographic software.

Find Aaron Tomb at

Similar Talks

CTO who understands the science around helping people do their best
Senior Software Engineer @IBM, Committer on Apache Aries
Distributed Systems Engineer Working on Cache @Twitter
Gold Badges Java, JVM, Memory, & Performance @StackOverflow / Lead developer of the OpenHFT project


Conference for Professional Software Developers