Towards a New Generation of Cryptographic Software

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.