論文の概要: SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations

• arxiv url: http://arxiv.org/abs/2407.15080v3
• Date: Thu, 21 Nov 2024 09:33:54 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-22 11:58:49.708431
• Title: SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
• Title（参考訳）: SNIP:コンパイラ変換のための投機的実行と非干渉保存
• Authors: Sören van der Wall, Roland Meyer,
• Abstract要約: 投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
• 参考スコア（独自算出の注目度）: 0.15800607910450126
• License:
• Abstract: 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. The basis of our proof method is a new form of simulation relation. It operates over directives that model the attacker's control over the micro-architectural state, and it accounts for the fact that the compiler transformation may change the influence of the micro-architectural state on the execution (and hence the directives). Using our proof method, we show the correctness of dead code elimination. When we tried to prove register allocation correct, we identified a previously unknown weakness that introduces violations to non-interference. We have confirmed the weakness for a mainstream compiler on code from the libsodium cryptographic library. To reclaim security once more, we develop a novel static analysis that operates on a product of source program and register-allocated program. Using the analysis, we present an automated fix to existing register allocation implementations. We prove the correctness of the fixed register allocations with our proof method.
• Abstract（参考訳）: 投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。 提案手法の基礎は,シミュレーション関係の新たな形式である。 マイクロアーキテクチャ状態に対する攻撃者の制御をモデル化するディレクティブ上で動作し、コンパイラ変換がマイクロアーキテクチャ状態が実行に与える影響(したがってディレクティブ)を変える可能性があるという事実を考慮します。 本手法を用いて, デッドコード除去の正当性を示す。 レジスタ割り当ての正しさを証明しようとすると、非干渉に違反をもたらす、これまで未知の弱点を特定しました。 我々はlibsodium暗号ライブラリのコード上でのメインストリームコンパイラの弱点を確認した。 セキュリティを再び回復させるために,我々は,ソースプログラムとレジスタ配置プログラムの製品で動作する新しい静的解析を開発した。 そこで本研究では,既存のレジスタ割り当て実装に対する自動修正を提案する。 固定レジスタ割り当ての正しさを証明法により証明する。

関連論文リスト

• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Breaking Bad: How Compilers Break Constant-Time~Implementations [12.486727810118497]
  本稿では,ディフェンシブプログラミング手法によって導入されたプロテクションを,コンパイラがどのように壊すかを検討する。 我々は,現在最先端の暗号ライブラリにそのようなコンパイラによって引き起こされる問題が現れるかどうかを,大規模な実験で検証する。 本研究は,最も高い評価を受けている暗号ライブラリのいくつかにおいて,コンパイラが引き起こす秘密の操作がいくつか発生していることを明らかにする。
  論文  参考訳（メタデータ） (2024-10-17T12:34:02Z)
• miniCodeProps: a Minimal Benchmark for Proving Code Properties [22.548472305010005]
  私たちはLeanの証明アシスタントで201のプログラム仕様のベンチマークであるminiCodePropsを紹介します。 その単純さにもかかわらず、MiniCodePropsは現在のLLMベースのプローバーを壊すのに十分である。
  論文  参考訳（メタデータ） (2024-06-16T21:11:23Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。 本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。 このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
  論文  参考訳（メタデータ） (2024-01-29T16:32:36Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Formalizing Stack Safety as a Security Property [0.6466206145151128]
  言語に基づくセキュリティの概念を用いて,スタック安全性の新たな形式的特徴付けを提案する。 この定式化は、Roessler と DeHon によって研究された "lazy" stack safety micro-policies と呼ばれる特定の執行機構によって動機付けられている。 ロースラーとデホンのマイクロポリスの正しい実装と不正確な実装を区別するためにそれらを用いて特性を検証する。
  論文  参考訳（メタデータ） (2021-05-02T08:18:34Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)
• Towards a Theoretical Understanding of the Robustness of Variational Autoencoders [82.68133908421792]
  敵攻撃や他の入力摂動に対する変分オートエンコーダ(VAE)の堅牢性を理解するために,我々は進出している。 確率モデルにおけるロバスト性のための新しい基準である$r$-robustnessを開発する。 遠心法を用いて訓練したVAEが、ロバストネスの指標でよく評価されていることを示す。
  論文  参考訳（メタデータ） (2020-07-14T21:22:29Z)

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

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