The Jasmin Compiler Preserves Cryptographic Security

TL;DR

This paper enhances the Jasmin compiler framework by formally proving that its front-end preserves cryptographic security, including IND-CCA, through rigorous logic and semantics in the Rocq prover.

Contribution

It introduces a Relational Hoare Logic for compiler correctness and proves that the Jasmin compiler preserves cryptographic security properties.

Findings

The front-end of the Jasmin compiler preserves cryptographic security.

The logic and semantics framework ensures formal security guarantees.

The compiler is proven secure under IND-CCA assumptions.

Abstract

Jasmin is a programming and verification framework for developing efficient, formally verified, cryptographic implementations. A main component of the framework is the Jasmin compiler, which empowers programmers to write efficient implementations of state-of-the-art cryptographic primitives, including post-quantum cryptographic standards. The Jasmin compiler is proven functionally correct in the Rocq prover. However, this functional correctness statement does not apply to nonterminating or probabilistic computations, which are essential features in cryptography. In this paper, we significantly enhance the guarantees of the compiler by showing, in the Rocq prover, that its front-end (25 out of 30 passes) preserves cryptographic security. To this end, we first define a Relational Hoare Logic tailored for compiler correctness proofs. We prove the soundness of our logic w.r.t. a new denotational semantics of Jasmin programs based on interaction trees. Secondly, we use our program logic to prove the functional correctness of the (unmodified) Jasmin compiler w.r.t. said semantics. Lastly, we formalize cryptographic security -- focusing on IND-CCA -- with interaction trees and prove that the Jasmin compiler preserves cryptographic security.