The Jasmin Compiler Preserves Cryptographic Security

• URL: http://arxiv.org/abs/2511.11292v1
• Date: Fri, 14 Nov 2025 13:26:36 GMT
• Title: The Jasmin Compiler Preserves Cryptographic Security
• Authors: Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini,
• Abstract summary: Jasmin is a framework for developing efficient, formally verified cryptographic implementations.<n>The Jasmin compiler is proven functionally correct in the Rocq prover.<n>We show, in the Rocq prover, that its front-end preserves cryptographic security.
• Score: 7.306101227450178
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Misquoted No More: Securely Extracting F* Programs with IO [0.3848364262836075]
  Shallow embeddings that use monads to represent effects are popular in proof-oriented languages.<n>Once shallowly embedded programs are verified, they are often extracted to mainstream languages like OCaml or C.<n>We build on this idea, but limit the use of translation validation to a first extraction step.
  arXiv  Detail & Related papers  (2026-02-23T15:37:18Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• A Proof-Producing Compiler for Blockchain Applications [0.0873811641236639]
  CairoZero is a programming language for running decentralized applications (dApps) at scale.<n> cryptographic protocols are used to verify the results of execution efficiently on blockchain.<n>We show how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications.
  arXiv  Detail & Related papers  (2025-01-25T00:31:47Z)
• Secure Semantic Communication With Homomorphic Encryption [52.5344514499035]
  This paper explores the feasibility of applying homomorphic encryption to SemCom.<n>We propose a task-oriented SemCom scheme secured through homomorphic encryption.
  arXiv  Detail & Related papers  (2025-01-17T13:26:14Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs.
  arXiv  Detail & Related papers  (2024-07-21T07:30:30Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  We propose a novel framework called FoC to Figure out the Cryptographic functions in stripped binaries.<n>We first build a binary large language model (FoC-BinLLM) to summarize the semantics of cryptographic functions in natural language.<n>We then build a binary code similarity model (FoC-Sim) upon the FoC-BinLLM to create change-sensitive representations and use it to retrieve similar implementations of unknown cryptographic functions in a database.
  arXiv  Detail & Related papers  (2024-03-27T09:45:33Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  Undefined behavior in C often causes devastating security vulnerabilities.<n>We introduce SECOMP, a compiler for compartmentalized C code with machine-checked proofs.<n>This is the first time such a strong criterion is proven for a mainstream programming language.
  arXiv  Detail & Related papers  (2024-01-29T16:32:36Z)
• Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
  Molly compiles cryptographic protocol roles into straight-line programs. We define a denotational semantics for protocol roles based on an axiomatization of the runtime.
  arXiv  Detail & Related papers  (2023-11-22T21:04:07Z)
• Weakening Assumptions for Publicly-Verifiable Deletion [79.61363884631021]
  We develop a simple compiler that generically adds publicly-verifiable deletion to a variety of cryptosystems. Our compiler only makes use of one-way functions.
  arXiv  Detail & Related papers  (2023-04-19T17:51:28Z)
• Quantum copy-protection of compute-and-compare programs in the quantum random oracle model [48.94443749859216]
  We introduce a quantum copy-protection scheme for a class of evasive functions known as " compute-and-compare programs" We prove that our scheme achieves non-trivial security against fully malicious adversaries in the quantum random oracle model (QROM) As a complementary result, we show that the same scheme fulfils a weaker notion of software protection, called "secure software leasing"
  arXiv  Detail & Related papers  (2020-09-29T08:41:53Z)
• Contrastive Code Representation Learning [95.86686147053958]
  We show that the popular reconstruction-based BERT model is sensitive to source code edits, even when the edits preserve semantics. We propose ContraCode: a contrastive pre-training task that learns code functionality, not form.
  arXiv  Detail & Related papers  (2020-07-09T17:59:06Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.