Understanding Formal Verification: Lessons from Verifying Post-Quantum-Secure Implementations (U12b)
Memory safety (e.g., preventing buffer overflows) and type safety (e.g., avoiding integer overflows) are critical for eliminating classes of bugs that commonly lead to CVEs and serious security breaches. Software verification can prevent these classes of bugs, but selecting the right approach is challenging because no single technique can meet all verification needs. A case study explains some of the challenges: in the open-source mlkem-native project (used in several cryptographic libraries, including AWS-LC, the FIPS 140-3 library for Amazon Web Services), the chosen verification approach failed to catch certain integer overflows.