KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM

High-assurance cryptography provides strong guarantees that source implementations are functionally correct and provably secure. In this paper, we demonstrate that the Jasmin compiler preserves functional correctness and KEM-IND-CCA security (which were established in prior work) of a highly optimized Jasmin implementation of ML-KEM used in the popular messenger Signal. Our proof of preservation is fully mechanized in the Rocq prover and is based on three general contributions: (1) A general framework for modeling game-based security and for reasoning about preservation of game-based security under compilation. (2) A new, interaction-trees-based semantics of Jasmin and assembly programs. Our new semantics supports features required by ML-KEM, such as probabilistic computations and rejection sampling routines. (3) A new relational Hoare logic for interaction trees, which we use to prove correctness of the Jasmin compiler under our new semantics.

• Security and privacy → Logic and verification.