Nicky Mouha

— On the schedule —

New Insights into the Formal Verification of AWS-LC, a Fork of OpenSSL

In this talk, I will focus on the formal verification of cryptographic implementations, and particularly on the PQC implementations in the AWS-LC library, a fork of OpenSSL. The goals are to achieve memory safety (preventing buffer overflows), type safety (avoiding integer overflows), and, to some extent, functional correctness (assuring that the implementation matches the specification). I will explain how the chosen verification approach failed to catch certain integer overflows. Additionally, I will present a newly discovered soundness bug. While acknowledged and fixed by the developers, this will be the first public talk about it.