InfoQ Homepage Presentations Assuring Crypto-code with Automated Reasoning
Assuring Crypto-code with Automated Reasoning
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.
Apr 13, 2017