Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Jasmin Compiler Preserves Cryptographic Security

Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini

TL;DR

This work addresses the gap between security proofs of cryptographic cores and their real implementations by proving that the Jasmin compiler front-end preserves cryptographic security under probabilistic, potentially nonterminating semantics. It introduces two Relational Hoare Logics and an interaction-tree–based denotational semantics to reason about two correlated executions, and then applies this framework to verify the Jasmin front-end across four internal languages. The authors formalize IND-CCA security for KEMs within this setting and prove that compilation preserves the adversary’s advantage, under standard correctness and initialization assumptions. The results yield an end-to-end security guarantee for compiled Jasmin implementations and demonstrate a measurable reduction in proof effort, with an artifact enabling replication and future extensions to back-end verification and side-channel considerations.

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.

The Jasmin Compiler Preserves Cryptographic Security

TL;DR

This work addresses the gap between security proofs of cryptographic cores and their real implementations by proving that the Jasmin compiler front-end preserves cryptographic security under probabilistic, potentially nonterminating semantics. It introduces two Relational Hoare Logics and an interaction-tree–based denotational semantics to reason about two correlated executions, and then applies this framework to verify the Jasmin front-end across four internal languages. The authors formalize IND-CCA security for KEMs within this setting and prove that compilation preserves the adversary’s advantage, under standard correctness and initialization assumptions. The results yield an end-to-end security guarantee for compiled Jasmin implementations and demonstrate a measurable reduction in proof effort, with an artifact enabling replication and future extensions to back-end verification and side-channel considerations.

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.

Paper Structure

This paper contains 29 sections, 5 theorems, 19 equations, 7 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Contribution 1: Relational Hoare Logic for Compiler Correctness
  3. Contribution 2: New Semantics and New Proofs for the Old Jasmin Compiler
  4. Contribution 3: Security Experiments and Preservation of Cryptographic Security
  5. Limitations
  6. Artifact
  7. Interaction Trees
  8. Background on Interaction Trees
  9. Interpretation
  10. Bisimulation
  11. Equivalence up-to-Cutoff
  12. Interaction Tree Semantics for Jasmin
  13. Relational Hoare Logic for an Interaction Trees Semantics
  14. Tuples and Validity
  15. Proof Rules
  16. ...and 14 more sections

Key Result

Theorem 1

If $P_1$ and $P_2$ are related, i.e., ${{{I_{P}},{I_{Q}}}~{{\vdash}^{}~{ {P_1} \mathrel{\sim} {P_2} \mathrel{:} {{\Phi}} \mathrel{\Rightarrow} {{\Psi}} }}}$, then every pair of functions satisfy their specification, i.e., ${{{I_{P}},{I_{Q}}}~{{\models}^{}~{ {P_1} \mathrel{\sim} {P_2} \mathrel{:} {{\

Figures (7)

  • Figure 1: Bisimulation relations ${\overset{\text{\tiny{$e$}}}{\approx}}$ and ${\overset{\text{\tiny{$u$}}}{\approx}}$ . The boxed rules are for ${\overset{\text{\tiny{$u$}}}{\approx}}$ only, all other are valid for both ${\overset{\text{\tiny{$e$}}}{\approx}}$ and ${\overset{\text{\tiny{$u$}}}{\approx}}$ .
  • Figure 2: Core syntax of Jasmin.
  • Figure 3: Interaction tree semantics of Jasmin commands.
  • Figure 4: Relational Hoare Logic.
  • Figure 5: Specialized Relational Hoare Logic.
  • ...and 2 more figures

Theorems & Definitions (7)

  • Definition 1: Valid RHL Command Tuple
  • Definition 2: Valid RHL Program Tuple
  • Theorem 1: Soundness
  • Theorem 2: Compiler Correctness
  • Theorem 3
  • Theorem 4: The Jasmin Compiler Preserves Cryptographic Security
  • Theorem 5