Fast, Formal, FIPS — Cryptographic Implementations in AWS-LC (U12a)
This talk describes one step in the speakers’ journey of optimizing, formally verifying, and FIPS validating cryptographic algorithms in AWS-LC. the speakers successfully delivered formally verified and optimized implementations of the post-quantum algorithm ML-KEM to AWS’s FIPS validated cryptographic library AWS-LC, which powers billions of daily cryptographic operations across security-critical AWS services. The speakers will demonstrate how the speakers resolved the fundamental tension between achieving optimal performance through hand-crafted assembly implementations and ensuring functional correctness through formal verification using the HOL Light theorem prover and C Bounded Model Checker (CBMC).