Abstract
We have completed machine-assisted proofs of two highly-optimized cryptographic primitives, AES-256-GCM and SHA-384. We have verified that the implementations of these primitives, written in a mix of C and x86 assembly, are memory safe and functionally correct, by which we mean input-output equivalent to their algorithmic specifications. Our proofs were completed using SAW, a bounded cryptographic verification tool which we have extended to handle embedded x86. The code we have verified comes from AWS LibCrypto. This code is identical to BoringSSL and very similar to OpenSSL, from which it ultimately derives. We believe we are the first to formally verify these implementations, which protect the security of nearly everybody on the internet.
Author supplied keywords
Cite
CITATION STYLE
Boston, B., Breese, S., Dodds, J., Dodds, M., Huffman, B., Petcher, A., & Stefanescu, A. (2021). Verified Cryptographic Code for Everybody. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12759 LNCS, pp. 645–668). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-81685-8_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
