Verified Cryptographic Code for Everybody
Date:
Nearly everybody relies on cryptographic libraries such as OpenSSL, but how can we be sure they are secure and bug-free? Formal verification offers an answer: using mathematical reasoning we can prove for certain that code behaves as we expected. Formal verification is an old idea, but recent advances have at last made it cost effective as an assurance tool for real-world cryptographic systems. This talk will explore what formal verification is, how we apply it to cryptography in production, and what lessons we can draw when securing other types of software systems.