Abstract
Along with Amazon Web Services, Galois is publishing a new paper titled “Verified Cryptographic Code for Everybody,” and we really do mean everybody. One benefit of the way we’ve done this work is that everyone who was using the code already is now using verified code. The library we’ve verified parts of is called AWS-LibCrypto. Much of that library is code that originated from BoringSSL, and BoringSSL is composed of code originating from OpenSSL. By almost any metric, these are the most-used cryptography libraries in the world, and we have verified some of the most critical code that they contain!
In the proof, we used SAW to verify hand-written cryptography safe and correct with regards to Cryptol specifications. The optimizations and details of the code we were verifying made the work very challenging but equally rewarding and important. We’re happy that our proofs have helped provide assurance for commonly used cryptography. The paper describes how our proofs work, and it also covers some of the challenges and engineering we did to accomplish such a challenging task. I hope you give it a read, and please reach out with your questions.