The Jasmin Compiler Preserves Cryptographic Security
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Gr\'egoire, Vincent Laporte, Paolo Torrini

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Advanced Authentication Protocols Security
