(Organized in the context of the hiring process for the new cybersecurity professorships.)
The pursuit of performance has produced a tremendous volume of critical cryptographic software. Many different cryptographic algorithms are in widespread use, with many more implementations tuned for speed on different platforms. A tiny bug anywhere in this code base can have disastrous consequences for security. For example, Brumley, Barbosa, Page, and Vercauteren exploited a miniscule carry bug in the commonly used OpenSSL cryptographic library to steal an SSL server's entire private key, allowing easy interception and forgery of user data.
Standard software-testing techniques catch many bugs but did not catch further OpenSSL carry bugs announced in January 2015 and December 2015. Expert audits caught these bugs but certainly have not caught all bugs: auditing is far too time-consuming to scale to the entire cryptographic code base, never mind the question of whether the auditing is reliable.
This talk will present a successful example of a new strategy to integrate highly automated proofs of correctness into real-world cryptographic software engineering. This is joint work with Peter Schwabe.