Asiacrypt 2025

Title

Towards a new generation of cryptographic software

Abstract

Cryptographic software is currently facing two major challenges. First, upgrading our cryptographic infrastructure to post-quantum primitives is probably the largest and most demanding cryptographic migration effort ever. New software needs to be written, optimized for different platforms, extensively tested and audited, and eventually integrated into protocols and systems.

Second, it becomes increasingly clear that the "constant-time'' programming paradigm is insufficient as a systematic defense against side-channel attacks, even when attackers are constrained to software-visible leakage only. Reasons range from compiler optimizations that eliminate source-level side-channel protections, through Spectre attacks that exploit microarchitectural leakage during speculative exeuction, to attacks like Hertzbleed, which blur the line between hardware-visible and software-visible leakage.

Fortunately, over the last decade, also the field of high-assurance cryptography, has made enormous progress. Research at the intersection of cryptography and formal methods has produced languages and tools that help us tackle these challenges. In my talk I will present what these tools are capable of and how they enable a new generation of cryptographic software with strong formal guarantees of correctness and security. I will use the concrete example of ML-KEM software that is end-to-end formally verified from the assembly level to the IND-CCA security notion, and which establishes a new state of the art in terms of principled protection against microarchitectural attacks.

Biography

Peter Schwabe is scientific director at MPI-SP professor at Radboud University and Adjunct Professor at Ruhr University Bochum. He graduated from RWTH Aachen University in computer science in 2006 and received a Ph.D. from the Faculty of Mathematics and Computer Science of Eindhoven University of Technology in 2011. He then worked as a postdoctoral researcher at the Institute for Information Science and the Research Center for Information Technology Innovation of Academia Sinica, Taiwan and at National Taiwan University.

His research area is cryptographic engineering; in particular the security and performance of cryptographic software. He published more than 80 articles in journals and at international conferences presenting, for example, fast software for a variety of cryptographic primitives including AES, hash functions, elliptic-curve cryptography, and cryptographic pairings. He has also published articles on fast cryptanalysis, in particular attacks on the discrete-logarithm problem.

In recent years he has focused in particular on post-quantum cryptography. He co-authored the "NewHope" and "NTRU-HRSS" lattice-based key-encapsulation schemes which were used in post-quantum TLS experiments by Google and he was co-submitter of seven proposals to the NIST post-quantum crypto project, all of which made it to the second round, five of which made it to the third round, and 3 of which were selected after round 3 for standardization.

In 2021, he co-founded the Formosa-Crypto project, an effort by multiple research groups to build (post-quantum) cryptographic software with formal proofs of functional correctness and security.