論文の概要: Molly: A Verified Compiler for Cryptoprotocol Roles

• arxiv url: http://arxiv.org/abs/2311.13692v1
• Date: Wed, 22 Nov 2023 21:04:07 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-25 13:16:38.665964
• Title: Molly: A Verified Compiler for Cryptoprotocol Roles
• Title（参考訳）: Molly:Cryptocolロール用の検証済みコンパイラ
• Authors: Daniel J. Dougherty, Joshua D. Guttman,
• Abstract要約: Mollyは暗号プロトコルロールを直線プログラムにコンパイルする。 我々は,ランタイムの公理化に基づいて,プロトコルの役割を意味論的に定義する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Molly is a program that compiles cryptographic protocol roles written in a high-level notation into straight-line programs in an intermediate-level imperative language, suitable for implementation in a conventional programming language. We define a denotational semantics for protocol roles based on an axiomatization of the runtime. A notable feature of our approach is that we assume that encryption is randomized. Thus, at the runtime level we treat encryption as a relation rather than a function. Molly is written in Coq, and generates a machine-checked proof that the procedure it constructs is correct with respect to the runtime semantics. Using Coq's extraction mechanism, one can build an efficient functional program for compilation.
• Abstract（参考訳）: Mollyは、高レベルの表記法で書かれた暗号プロトコルのロールを中間レベルの命令型言語の直線プログラムにコンパイルするプログラムであり、従来のプログラミング言語の実装に適している。 我々は,ランタイムの公理化に基づいて,プロトコルの役割を意味論的に定義する。 このアプローチの注目すべき特徴は、暗号化がランダム化されていると仮定することです。 したがって、実行時レベルでは、暗号化は関数ではなく関係として扱う。 Molly は Coq で書かれており、マシンチェックによって構築された手順が実行時の意味論に関して正しいという証明を生成する。 Coqの抽出機構を使うことで、効率的なコンパイル機能プログラムを構築することができる。

関連論文リスト

• What can Large Language Models Capture about Code Functional Equivalence? [24.178831487657945]
  SeqCoBenchは、コード-LLMがコード関数同値をキャプチャする方法を評価するベンチマークである。 我々は,SeqCoBenchにおける意味論的に等価なプログラムと異なるプログラムのペアを識別できるかどうかを,最先端(Code-)LLMで評価する。
  論文  参考訳（メタデータ） (2024-08-20T11:19:06Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• SparseCoder: Identifier-Aware Sparse Transformer for File-Level Code Summarization [51.67317895094664]
  本稿では,大規模なソースコードプロジェクトの理解と維持を支援するファイルレベルのコード要約について検討する。 長いコードシーケンスを効果的に処理するための識別子対応スパース変換器であるSparseCoderを提案する。
  論文  参考訳（メタデータ） (2024-01-26T09:23:27Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。 キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
  論文  参考訳（メタデータ） (2023-12-07T17:51:43Z)
• Outline, Then Details: Syntactically Guided Coarse-To-Fine Code Generation [61.50286000143233]
  ChainCoderは、Pythonコードを段階的に生成するプログラム合成言語モデルである。 自然言語記述と構文的に整合したI/Oデータサンプルを共同で符号化するために、カスタマイズされたトランスフォーマーアーキテクチャを利用する。
  論文  参考訳（メタデータ） (2023-04-28T01:47:09Z)
• A Formalization of Operads in Coq [0.0]
  本稿では,証明アシスタントであるCoqで操作された関数の形式化について論じる。 CoqはV-SPELLS内でのメタ言語開発のための公式な数学的基盤を提供する。 私たちの研究は、私たちの知る限りでは、重要な自動化を備えた証明アシスタント内でのオペラッドの初めての公式化も提供しています。
  論文  参考訳（メタデータ） (2023-03-15T19:29:40Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)

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

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