You are now in FULL VIEW

Assuring Crypto-code with Automated Reasoning
Recorded at:

| by Aaron Tomb on Apr 13, 2017 | NOTICE: The next QCon is in New York Jun 26-30, 2017. Join us!

Aaron Tomb describes the capabilities and operation of some open source tools that allow developers to conclusively and largely automatically determine whether a low-level cryptographic implementation exactly matches a higher-level mathematical specification. He focusses on work they have done to integrate these tools into the continuous integration system of Amazon's s2n implementation of TLS.

Sponsored Content


Aaron Tomb works as a Research Lead, Software Correctness at Galois. He leads projects focused on applied formal methods, with a particular emphasis on the verification of cryptographic software.

Software is changing the world. QCon empowers software development by facilitating the spread of knowledge and innovation in the developer community. A practitioner-driven conference, QCon is designed for technical team leads, architects, engineering directors, and project managers who influence innovation in their teams.