BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage Presentations Assuring Crypto-code with Automated Reasoning

Assuring Crypto-code with Automated Reasoning

Bookmarks
44:37

Summary

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.

Bio

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.

About the conference

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.

Recorded at:

Apr 13, 2017

BT