論文の概要: A Proof-Producing Compiler for Blockchain Applications

• arxiv url: http://arxiv.org/abs/2501.15002v1
• Date: Sat, 25 Jan 2025 00:31:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-28 13:53:41.745999
• Title: A Proof-Producing Compiler for Blockchain Applications
• Title（参考訳）: ブロックチェーンアプリケーションのためのプロデューサコンパイラ
• Authors: Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman,
• Abstract要約: CairoZeroは、分散アプリケーション(dApps)を大規模に実行するためのプログラミング言語である。 暗号化プロトコルは、ブロックチェーン上での実行結果を効率的に検証するために使用される。 ユーザがLean 3の証明アシスタントで、コンパイルされたコードが高レベルの機能仕様を満たすことを証明できるように、CairoZeroコンパイラをいかに拡張したかを示します。
• 参考スコア（独自算出の注目度）: 0.0873811641236639
• License:
• Abstract: CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain 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. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.
• Abstract（参考訳）: CairoZeroは、分散アプリケーション(dApps)を大規模に実行するためのプログラミング言語である。 CairoZero言語で記述されたプログラムは、Cairo CPUアーキテクチャのマシンコードにコンパイルされ、ブロックチェーン上での実行結果を効率的に検証するために暗号化プロトコルが使用される。 私たちはどのようにしてCairoZeroコンパイラを拡張したのかを説明し、ユーザーがLean 3の証明アシスタントで、コンパイルされたコードが高レベルの機能仕様を満たすことを証明できるようにしました。 我々は, secp256k1およびsecp256r1曲線を用いた計算のプリミティブの検証と, 前者を用いた暗号署名の検証により, 本手法の有効性を実証する。 また、読み書き辞書データ構造を読み取り専用設定でシミュレートする機構を検証する。 最後に、方法論を反映し、アプローチの利点について論じます。

関連論文リスト

• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。 しきい値暗号システムに対する既存のアプローチは、しきい値暗号プロトコルを実行するための少なくとも1つのメッセージ遅延の遅延オーバーヘッドを導入している。 しきい値が狭いブロックチェーンネイティブのしきい値暗号システムに対して,このオーバーヘッドを取り除く機構を提案する。
  論文  参考訳（メタデータ） (2024-07-16T20:53:04Z)
• Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
  我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。 このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。 我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
  論文  参考訳（メタデータ） (2024-01-06T02:57:44Z)
• Towards a zk-SNARK compiler for Wolfram language [0.0]
  このプロジェクトはWolframのZeroKnowledgeProofs paclet上に構築され、Pinocchioプロトコルに基づいたzk-SNARKコンパイラを実装している。 インタラクティブな証明はブロックチェーンアプリケーションには適していないが、zk-SNARKのような新しいプロトコルはZcashのようなゼロ知識の台帳を可能にする。
  論文  参考訳（メタデータ） (2024-01-05T18:24:32Z)
• Chain of Code: Reasoning with a Language Model-Augmented Code Emulator [115.16975276693267]
  我々は、LMコード駆動推論を改善するシンプルながら驚くほど効果的な拡張であるChain of Codeを提案する。 キーとなるアイデアは、プログラム内のセマンティックなサブタスクを、インタープリタが明示的にキャッチできるフレキシブルな擬似コードとしてフォーマットすることを、LMに促すことである。
  論文  参考訳（メタデータ） (2023-12-07T17:51:43Z)
• Molly: A Verified Compiler for Cryptoprotocol Roles [0.0]
  Mollyは暗号プロトコルロールを直線プログラムにコンパイルする。 我々は,ランタイムの公理化に基づいて,プロトコルの役割を意味論的に定義する。
  論文  参考訳（メタデータ） (2023-11-22T21:04:07Z)
• Exploring Continual Learning for Code Generation Models [80.78036093054855]
  継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。 コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。 即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
  論文  参考訳（メタデータ） (2023-07-05T16:58:39Z)
• HDCC: A Hyperdimensional Computing compiler for classification on embedded systems and high-performance computing [58.720142291102135]
  この研究は、HDC分類メソッドの高レベルな記述を最適化されたCコードに変換する最初のオープンソースコンパイラである、ネームコンパイラを紹介している。 nameは現代のコンパイラのように設計されており、直感的で記述的な入力言語、中間表現(IR)、再ターゲット可能なバックエンドを備えている。 これらの主張を裏付けるために,HDC文献で最もよく使われているデータセットについて,HDCCを用いて実験を行った。
  論文  参考訳（メタデータ） (2023-04-24T19:16:03Z)
• Bounding the quantum value of compiled nonlocal games: from CHSH to BQP verification [2.298932494750101]
  Kalaiらは、非ローカルゲームに適用されるブラックボックス暗号コンパイル手順を定義した。 単一プロデューサプロトコルの量子値の完全な理解に向けて前進する。 我々は,BQPに対して単一プロプライエタリな古典的検証プロトコルを提供し,CHSH剛性解析を用いてその健全性を証明した。
  論文  参考訳（メタデータ） (2023-03-02T19:20:59Z)
• 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)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)
• Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
  qcorはC++とコンパイラの実装の言語拡張で、異種量子古典プログラミング、コンパイル、単一ソースコンテキストでの実行を可能にする。 我々の研究は、量子言語で高レベルな量子カーネル(関数)を表現できる、第一種C++コンパイラを提供する。
  論文  参考訳（メタデータ） (2020-10-08T12:49:07Z)

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

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