The Jasmin Compiler Preserves Cryptographic Security
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911265967833088 |
|---|---|
| author | Arranz-Olmos, Santiago Barthe, Gilles Blatter, Lionel Grégoire, Benjamin Laporte, Vincent Torrini, Paolo |
| author_facet | Arranz-Olmos, Santiago Barthe, Gilles Blatter, Lionel Grégoire, Benjamin Laporte, Vincent Torrini, Paolo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_11292 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Jasmin Compiler Preserves Cryptographic Security Arranz-Olmos, Santiago Barthe, Gilles Blatter, Lionel Grégoire, Benjamin Laporte, Vincent Torrini, Paolo Programming Languages Cryptography and Security 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. |
| title | The Jasmin Compiler Preserves Cryptographic Security |
| topic | Programming Languages Cryptography and Security |
| url | https://arxiv.org/abs/2511.11292 |