View Item 
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        •   Utrecht University Student Theses Repository Home
        • UU Theses Repository
        • Theses
        • View Item
        JavaScript is disabled for your browser. Some features of this site may not work without it.

        Browse

        All of UU Student Theses RepositoryBy Issue DateAuthorsTitlesSubjectsThis CollectionBy Issue DateAuthorsTitlesSubjects

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

        Thumbnail
        View/Open
        thesis.pdf (322.6Kb)
        Publication date
        2025
        Author
        Cassee, Stijn
        Metadata
        Show full item record
        Summary
        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.
        URI
        https://studenttheses.uu.nl/handle/20.500.12932/49107
        Collections
        • Theses
        Utrecht university logo