Formal Verification of AWS-LibCrypto

AWS-LibCrypto (AWS-LC) is an open-source cryptography library forked from BoringSSL and OpenSSL, with features and performance improvements developed at Amazon Web Services (AWS). The library contains C implementations as well as low-level assembly code for cryptographic functionalities used on various platforms. AWS-LC is used to support several security or cryptographic libraries, including within AWS. It is under active development to satisfy the needs of even AWS’s most security-conscious customers. 

The impact of AWS-LC is tremendous considering the scale of AWS, therefore safety and correctness of the library becomes essential. Jointly with Galois, we developed a companion library called AWS-LC-Verification. This library contains formal specification and proofs for verifying functional correctness and memory safety of critical algorithms in AWS-LC. The proofs in AWS-LCVerification are run in the Continuous Integration (CI) of the AWS-LC repository, ensuring functional correctness and memory safety of all verified algorithms in each fresh pull request. Verified algorithms are SHA2, HMAC, AES-KW(P), AES-GCM, Elliptic Curve (EC) functions, ECDSA, ECDH and HKDF. 

The highly-optimized low-level code together with C implementations pose challenges for formal verification. This could not be managed in a single tool. Instead, the proofs in AWS-LC-Verification are developed using several formal techniques or tooling with care taken for proof integration.

•  The proofs for C and X86 64 programs are carried out in Software Analysis Workbench (SAW) using Cryptol specifications.
• To address AArch64 assembly code on Graviton machines, we use a lowlevel code symbolic simulation tool currently under-development by AWS. We automatically translate Cryptol specification to the tool language for integration with C proofs. 
• For EC, AWS-LC uses field arithmetic code formally verified by HOLLight from S2N-Bignum and by Coq from Fiat-Crypto. On top of it, we use the theorem prover Coq for establishing group properties of the specification. These mathematical proofs are more easily stated and proved within a theorem prover. 

We will also report on our experience with proof maintenance in the opensource setting.

Yan Peng is an applied scientist at Amazon Web Services. She works on verifying functional correctness and memory safety of cryptographic libraries through formal methods. Yan worked on combining SMT solving with theorem proving for verification of AMS (Analog and Mixed-Signal) and Asynchronous designs in her PhD studies.