論文の概要: CryptOpt: Verified Compilation with Randomized Program Search for
Cryptographic Primitives (full version)
- arxiv url: http://arxiv.org/abs/2211.10665v3
- Date: Mon, 22 May 2023 00:53:32 GMT
- ステータス: 処理完了
- システム内更新日: 2023-05-24 05:09:19.863467
- Title: CryptOpt: Verified Compilation with Randomized Program Search for
Cryptographic Primitives (full version)
- Title（参考訳）: CryptOpt: 暗号化プリミティブのランダム化プログラム検索による検証済みコンパイル(フルバージョン)
- Authors: Joel Kuepper, Andres Erbsen, Jason Gross, Owen Conoly, Chuyue Sun,
Samuel Tian, David Wu, Adam Chlipala, Chitchanok Chuengsatiansup, Daniel
Genkin, Markus Wagner, Yuval Yarom
- Abstract要約: 暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。
CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。
形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
- 参考スコア（独自算出の注目度）: 12.790826917588575
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: Most software domains rely on compilers to translate high-level code to
multiple different machine languages, with performance not too much worse than
what developers would have the patience to write directly in assembly language.
However, cryptography has been an exception, where many performance-critical
routines have been written directly in assembly (sometimes through
metaprogramming layers). Some past work has shown how to do formal verification
of that assembly, and other work has shown how to generate C code automatically
along with formal proof, but with consequent performance penalties vs. the
best-known assembly. We present CryptOpt, the first compilation pipeline that
specializes high-level cryptographic functional programs into assembly code
significantly faster than what GCC or Clang produce, with mechanized proof (in
Coq) whose final theorem statement mentions little beyond the input functional
program and the operational semantics of x86-64 assembly. On the optimization
side, we apply randomized search through the space of assembly programs, with
repeated automatic benchmarking on target CPUs. On the formal-verification
side, we connect to the Fiat Cryptography framework (which translates
functional programs into C-like IR code) and extend it with a new formally
verified program-equivalence checker, incorporating a modest subset of known
features of SMT solvers and symbolic-execution engines. The overall prototype
is quite practical, e.g. producing new fastest-known implementations of
finite-field arithmetic for both Curve25519 (part of the TLS standard) and the
Bitcoin elliptic curve secp256k1 for the Intel $12^{th}$ and $13^{th}$
generations.
- Abstract（参考訳）: ほとんどのソフトウェアドメインは、高レベルのコードを複数の異なるマシン言語に翻訳するコンパイラに依存しており、パフォーマンスは開発者がアセンブリ言語で直接書く忍耐力を持つものよりもそれほど悪くはない。
しかし、暗号は例外であり、多くのパフォーマンスクリティカルなルーチンが直接アセンブリ(時にはメタプログラミング層を通して)で書かれてきた。
いくつかの過去の研究は、そのアセンブリの正式な検証方法を示しており、他の研究は、正式な証明とともにCコードを自動的に生成する方法を示している。
我々は、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする最初のコンパイルパイプラインであるCryptOptを紹介する。
最適化側では、ターゲットcpu上で自動ベンチマークを繰り返して、アセンブリプログラムの空間にランダム検索を適用する。
形式検証側では,関数型プログラムをCライクなIRコードに変換するFiat Cryptographyフレームワークに接続して,SMTソルバとシンボリックエグゼクティブエンジンの既知の特徴の質素なサブセットを組み込んだ,プログラム等価チェッカを新たに正式に認証した。
全体的なプロトタイプは非常に実用的であり、例えばCurve25519(TLS標準の一部)とBitcoin楕円曲線secp256k1(Intel $112^{th}$と13^{th}$世代)の両方に対して、新しい高速な有限フィールド演算の実装を生成する。
関連論文リスト
- Context-aware Code Segmentation for C-to-Rust Translation using Large Language Models [1.8416014644193066]
大きな言語モデル(LLM)は、ルールベースのメソッドよりも自然で安全なコードを生成することで、この翻訳を自動化することを約束している。
大規模Cコードをコンパイル可能なRustコードに変換する際の成功率を改善するLLMベースの翻訳方式を提案する。
4キロのコードを含む20のベンチマークCプログラムの実験では、すべてのプログラムをコンパイル可能なRustコードに変換することに成功した。
論文 参考訳（メタデータ） (2024-09-16T17:52:36Z) - Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
大規模言語モデルは、自然言語の理解と生成において例外的な能力を示した。
しかし、それらの生成速度は、その復号過程の本質的にシーケンシャルな性質によって制限される。
本稿では,データ駆動方式で実装された新しいデコーディング手法であるLexical Unit Decodingを紹介する。
論文 参考訳（メタデータ） (2024-05-24T04:35:13Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - Exploring Continual Learning for Code Generation Models [80.78036093054855]
継続的学習(CL)は、コードドメインの中でまだ過小評価されていない重要な側面である。
コード生成,翻訳,要約,改良など,幅広いタスクをカバーするCodeTask-CLというベンチマークを導入する。
即時選択機構の不安定な訓練により,プロンプトプール (PP) などの有効手法が破滅的な忘れ込みに悩まされることが判明した。
論文 参考訳（メタデータ） (2023-07-05T16:58:39Z) - ArctyrEX : Accelerated Encrypted Execution of General-Purpose
Applications [6.19586646316608]
FHE(Fully Homomorphic Encryption)は、計算中のユーザデータのプライバシとセキュリティを保証する暗号化手法である。
我々は、暗号化実行を高速化する新しい技術を開発し、我々のアプローチの顕著な性能上の利点を実証する。
論文 参考訳（メタデータ） (2023-06-19T15:15:41Z) - SLaDe: A Portable Small Language Model Decompiler for Optimized Assembly [6.080751346188323]
本稿では,実世界のコード上で訓練されたシーケンス・ツー・シーケンス・トランスフォーマをベースとした小型言語モデルデコンパイラであるSLaDeを提案する。
型推論を利用して、標準的な分析や最近のニューラルアプローチよりも読みやすく正確なプログラムを生成する。
論文 参考訳（メタデータ） (2023-05-21T17:31:39Z) - Advising OpenMP Parallelization via a Graph-Based Approach with
Transformers [2.393682571484038]
我々は,OpenMPのプラグマと共有メモリ属性を並列コードで検出し,予測する,OMPifyと呼ばれる新しい手法を提案する。
OMPifyは、ソースコードのグラフベースの表現を利用するTransformerベースのモデルに基づいている。
以上の結果から,OMPifyは汎用および人気の高いChatGPTやPragFormerモデルなど,既存のアプローチよりも優れていることが示された。
論文 参考訳（メタデータ） (2023-05-16T16:56:10Z) - 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) - QParallel: Explicit Parallelism for Programming Quantum Computers [62.10004571940546]
並列量子プログラミングのための言語拡張を提案する。
QParallelは、現在の量子プログラミング言語における並列性に関する曖昧さを取り除く。
並列化によって最も利益を上げるサブルーチンを識別し,並列領域の配置にプログラマを誘導するツールを提案する。
論文 参考訳（メタデータ） (2022-10-07T16:35:16Z) - Natural Language to Code Translation with Execution [82.52142893010563]
実行結果-プログラム選択のための最小ベイズリスク復号化。
そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
論文 参考訳（メタデータ） (2022-04-25T06:06:08Z) - Can We Generate Shellcodes via Natural Language? An Empirical Study [4.82810058837951]
本稿では,ニューラルネットワークを用いたシェルコードの自動生成手法を提案する。
Shellcode_IA32は、実際のLinux/x86シェルコードの3,200のアセンブリコードスニペットで構成されている。
我々は,NMTが自然言語からアセンブリコードスニペットを高い精度で生成できることを示し,多くの場合,誤りのないシェルコード全体を生成可能であることを示した。
論文 参考訳（メタデータ） (2022-02-08T09:57:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。