論文の概要: The Jasmin Compiler Preserves Cryptographic Security

• arxiv url: http://arxiv.org/abs/2511.11292v1
• Date: Fri, 14 Nov 2025 13:26:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-17 22:42:18.62342
• Title: The Jasmin Compiler Preserves Cryptographic Security
• Title（参考訳）: Jasminコンパイラは暗号化のセキュリティを保っている
• Authors: Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini,
• Abstract要約: Jasminは、効率的で正式に認証された暗号実装を開発するためのフレームワークである。 JasminコンパイラはRocq証明器で機能的に正しいことが証明されている。 Rocqの証明では、フロントエンドは暗号化のセキュリティを保っている。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: Jasminは、効率的で正式な暗号実装を開発するためのプログラミングおよび検証フレームワークである。 フレームワークの主なコンポーネントはJasminコンパイラであり、これはプログラマが量子後暗号標準を含む最先端の暗号プリミティブの効率的な実装を書けるようにするものである。 JasminコンパイラはRocq証明器で機能的に正しいことが証明されている。 しかし、この関数的正当性ステートメントは暗号に不可欠な非決定的あるいは確率的計算には適用されない。 本稿では,ローク証明器において,そのフロントエンド(30パス中25パス)が暗号セキュリティを保っていることを示すことにより,コンパイラの保証を著しく向上させる。 この目的のために、まずコンパイラの正当性証明に適したリレーショナルホア論理を定義する。 我々は、相互作用木に基づくジャスミンプログラムの新しい意味論的意味論として、論理学の健全性を証明する。 次に、プログラムロジックを用いて、(修正されていない)Jasminコンパイラw.r.t.のセマンティクスの関数的正当性を証明します。 最後に、IND-CCAに焦点を当てた暗号化セキュリティをインタラクションツリーで形式化し、Jasminコンパイラが暗号化セキュリティを保存することを証明します。

関連論文リスト

• A Proof-Producing Compiler for Blockchain Applications [0.0873811641236639]
  CairoZeroは、分散アプリケーション(dApps)を大規模に実行するためのプログラミング言語である。 暗号化プロトコルは、ブロックチェーン上での実行結果を効率的に検証するために使用される。 ユーザがLean 3の証明アシスタントで、コンパイルされたコードが高レベルの機能仕様を満たすことを証明できるように、CairoZeroコンパイラをいかに拡張したかを示します。
  論文  参考訳（メタデータ） (2025-01-25T00:31:47Z)
• Secure Semantic Communication With Homomorphic Encryption [52.5344514499035]
  本稿では,SemCom に準同型暗号を適用する可能性について検討する。 タスク指向のSemComスキームを提案する。
  論文  参考訳（メタデータ） (2025-01-17T13:26:14Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [51.898805184427545]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
  Mollyは暗号プロトコルロールを直線プログラムにコンパイルする。 我々は,ランタイムの公理化に基づいて,プロトコルの役割を意味論的に定義する。
  論文  参考訳（メタデータ） (2023-11-22T21:04:07Z)
• Weakening Assumptions for Publicly-Verifiable Deletion [79.61363884631021]
  我々は,様々な暗号システムに公開検証可能な削除を汎用的に付加する,シンプルなコンパイラを開発した。 コンパイラは片道関数のみを使用します。
  論文  参考訳（メタデータ） (2023-04-19T17:51:28Z)
• Quantum copy-protection of compute-and-compare programs in the quantum random oracle model [48.94443749859216]
  計算・比較プログラム(Computer-and-compare program)として知られる回避関数のクラスに対する量子コピー保護スキームを導入する。 我々は,量子乱数オラクルモデル(QROM)において,完全悪意のある敵に対する非自明なセキュリティを実現することを証明した。 補完的な結果として、「セキュアソフトウェアリース」という,ソフトウェア保護の概念の弱さが示される。
  論文  参考訳（メタデータ） (2020-09-29T08:41:53Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。