Verified Cryptographic Code for Everybody
| Autor: | Mike Dodds, Brett Boston, Brian Huffman, Andrei Stefanescu, Josiah Dodds, Samuel Breese, Adam Petcher |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
0303 health sciences
Cryptographic primitive Programming language business.industry Computer science 020207 software engineering Cryptography 02 engineering and technology computer.software_genre Mathematical proof 03 medical and health sciences Bounded function 0202 electrical engineering electronic engineering information engineering Code (cryptography) x86 The Internet Automated reasoning business computer 030304 developmental biology |
| Zdroj: | Computer Aided Verification ISBN: 9783030816841 CAV (1) |
| DOI: | 10.1007/978-3-030-81685-8_31 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|