Finding Timing leaks in Post-Quantum Cryptography Implementations Using Binary Symbolic Execution

Abstract

Considering side channel attacks in cryptography, timing leaks are particularly dangerous as they can be exploited over a network to leak cryptographic secrets. Post-quantum cryptography (PQC) is a new class of cryptography, designed as quantum-safe replace- ment for public-key cryptography schemes in use today which are vulnerable for an attack with a powerful enough quantum computer. This thesis explores the feasibility of finding timing leaks in PQC implementations at the binary level using symbolic execution. The study focuses on three standardized PQC schemes: ML-KEM, ML-DSA, and SLH-DSA, using the Binsec tool for analysis. We developed a benchmarking harness to facilitate experiments with different compilers, optimisation levels, and configurations. The results highlight significant challenges in scaling binary symbolic execution for PQC, with only SLH-DSA completing the analysis within a reasonable time. Known timing leaks, such as the kyberslash vulnerability, were successfully detected in isolated functions. However, full implementation analysis often resulted in timeouts, highlighting the complexity of PQC schemes compared to classical cryptography. We suggest further work on improved methodologies, such as a modular, per-function analysis. Although promising, binary symbolic execution requires substantial effort in configuration and parameter tuning, lim- iting its current usability as a turnkey solution for constant time verification in PQC implementations.