Abstract: For over a decade, a buffer overflow vulnerability in the “official” SHA-3 implementation by its designers remained unnoticed. This vulnerability was assigned CVE-2022-37454 and impacted several projects such as Python and PHP that relied on this implementation. We provide a proof of concept for arbitrary code execution and explain how we found the vulnerability using the KLEE symbolic execution tool. In light of the upcoming NIST Workshop on Formal Methods within Certification Programs (FMCP 2024), we give an overview of various approaches to mitigate these types of bugs in cryptographic implementations and discuss both their cost and effectiveness.
Bio: Dr. Nicky Mouha is a researcher in cryptography with more than 15 years of experience. Besides his research, he is involved in various standardization activities, mainly at NIST and ISO, including the organization of the upcoming NIST Workshop on Formal Methods within Certification Programs (FMCP 2024). He invented the MILP- and SAT-based techniques for differential and linear cryptanalysis and designed the lightweight Chaskey algorithm (standardized in ISO/IEC 29192-6) which is now widely deployed in the automotive industry. He also discovered vulnerabilities in billions of devices, such as a buffer overflow in the “official” SHA-3 implementation (CVE-2022-37454).