論文の概要: Formalizing Stack Safety as a Security Property

• arxiv url: http://arxiv.org/abs/2105.00417v4
• Date: Thu, 21 Mar 2024 10:28:34 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-22 20:55:19.493237
• Title: Formalizing Stack Safety as a Security Property
• Title（参考訳）: 安全財産としてのスタック安全の形式化
• Authors: Sean Noble Anderson, Roberto Blanco, Leonidas Lampropoulos, Benjamin C. Pierce, Andrew Tolmach,
• Abstract要約: 言語に基づくセキュリティの概念を用いて,スタック安全性の新たな形式的特徴付けを提案する。 この定式化は、Roessler と DeHon によって研究された "lazy" stack safety micro-policies と呼ばれる特定の執行機構によって動機付けられている。 ロースラーとデホンのマイクロポリスの正しい実装と不正確な実装を区別するためにそれらを用いて特性を検証する。
• 参考スコア（独自算出の注目度）: 0.6466206145151128
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The term stack safety is used to describe a variety of compiler, run-time, and hardware mechanisms for protecting stack memory. Unlike "the heap," the ISA-level stack does not correspond to a single high-level language concept: different compilers use it in different ways to support procedural and functional abstraction mechanisms from a wide range of languages. This protean nature makes it difficult to nail down what it means to correctly enforce stack safety. We propose a new formal characterization of stack safety using concepts from language-based security. Rather than treating stack safety as a monolithic property, we decompose it into an integrity property and a confidentiality property for each of the caller and the callee, plus a control-flow property: five properties in all. This formulation is motivated by a particular class of enforcement mechanisms, the "lazy" stack safety micro-policies studied by Roessler and DeHon, which permit functions to write into one another's frames but taint the changed locations so that the frame's owner cannot access them. No existing characterization of stack safety captures this style of safety; we capture it here by stating our properties in terms of the observable behavior of the system. Our properties go further than previous formal definitions of stack safety, supporting caller- and callee-saved registers, arguments passed on the stack, and tail-call elimination. We validate the properties by using them to distinguish between correct and incorrect implementations of Roessler and DeHon's micro-policies using property-based random testing. Our test harness successfully identifies several broken variants, including Roessler and DeHon's lazy policy; a repaired version of their policy passes our tests.
• Abstract（参考訳）: スタック安全性という用語は、スタックメモリを保護する様々なコンパイラ、実行時、ハードウェアメカニズムを記述するために使われる。 異なるコンパイラは、広範囲の言語から手続き的および機能的抽象化メカニズムをサポートするために、異なる方法でそれを使用する。 このプロテア的な性質は、スタックの安全性を正しく強制することの意味を断ち切るのを難しくする。 言語に基づくセキュリティの概念を用いて,スタック安全性の新たな形式的特徴付けを提案する。 スタックの安全性をモノリシックなプロパティとして扱うのではなく、呼び出し側と呼び出し側それぞれに対して、整合性プロパティと機密性プロパティに分解します。 この定式化は、Roessler と DeHon が研究した "lazy" stack safety micro-policies という、特定の種類の執行機構によって動機付けられている。 スタック安全性の既存の特徴は、このタイプの安全性をキャプチャするものではなく、システムの観測可能な振る舞いの観点から、私たちの特性を記述することによって、これをキャプチャします。 私たちのプロパティは、スタックの安全性、呼び出し元と呼び出し元が保存したレジスタのサポート、スタックに渡された引数、末尾呼び出しの削除といった、以前の公式定義よりもさらに進んでいます。 プロパティベースのランダムテストを用いて,Roessler と DeHon のマイクロポリスの正しい実装と不正確な実装を区別するために,それらの特性を検証した。 私たちのテストハーネスは、RoesslerやDeHonの遅延ポリシーなど、いくつかの壊れた亜種をうまく識別します。

関連論文リスト

• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal Behaviors [64.9938658716425]
  安全でないユーザリクエストを認識して拒否する、大規模な言語モデル(LLM)の既存の評価は、3つの制限に直面している。 まず、既存の手法では、安全でないトピックの粗い粒度を使い、いくつかのきめ細かいトピックを過剰に表現している。 第二に、プロンプトの言語的特徴とフォーマッティングは、様々な言語、方言など、多くの評価において暗黙的にのみ考慮されているように、しばしば見過ごされる。 第3に、既存の評価は大きなLCMに頼っているため、コストがかかる可能性がある。
  論文  参考訳（メタデータ） (2024-06-20T17:56:07Z)
• Characterizing Unsafe Code Encapsulation In Real-world Rust Systems [2.285834282327349]
  内部アンセーフは、システムソフトウェア開発においてRustコミュニティによって提唱される重要な設計パラダイムである。 Rustコンパイラは、安全でないコードを含む安全な関数の健全性を検証することができない。 安全でないコードの本質的な使用法とカプセル化をモデル化するための,新しいアンセーフティアイソレーショングラフを提案する。
  論文  参考訳（メタデータ） (2024-06-12T06:59:51Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 FoC-BinLLMは、ROUGE-LスコアでChatGPTを14.61%上回った。 FoC-Simは52%高いRecall@1で過去のベストメソッドを上回っている。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• AdaShield: Safeguarding Multimodal Large Language Models from Structure-based Attack via Adaptive Shield Prompting [54.931241667414184]
  textbfAdaptive textbfShield Promptingを提案する。これは、MLLMを構造ベースのジェイルブレイク攻撃から守るための防御プロンプトで入力をプリペイドする。 我々の手法は、構造に基づくジェイルブレイク攻撃に対するMLLMの堅牢性を一貫して改善することができる。
  論文  参考訳（メタデータ） (2024-03-14T15:57:13Z)
• SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
  C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。 本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。 このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
  論文  参考訳（メタデータ） (2024-01-29T16:32:36Z)
• Static Deadlock Detection for Rust Programs [6.596623081054982]
  Rustはスレッドとメモリの安全性を確保するために独自のオーナシップメカニズムに依存している。 Rustの新しい言語機能は、脆弱性検出に新たな課題をもたらす。 本稿では,Rustプログラムに適した静的デッドロック検出手法を提案する。
  論文  参考訳（メタデータ） (2024-01-02T09:09:48Z)
• Certifying LLM Safety against Adversarial Prompting [75.19953634352258]
  大規模言語モデル(LLM)は、入力プロンプトに悪意のあるトークンを追加する敵攻撃に対して脆弱である。 我々は,認証された安全保証とともに,敵のプロンプトを防御する最初の枠組みである消去・チェックを導入する。
  論文  参考訳（メタデータ） (2023-09-06T04:37:20Z)
• Safe Deep Reinforcement Learning by Verifying Task-Level Properties [84.64203221849648]
  コスト関数は、安全深層強化学習(DRL)において一般的に用いられる。 このコストは通常、国家空間における政策決定のリスクの定量化が難しいため、指標関数として符号化される。 本稿では,ドメイン知識を用いて,そのような状態に近接するリスクを定量化するための代替手法について検討する。
  論文  参考訳（メタデータ） (2023-02-20T15:24:06Z)
• Unsafe's Betrayal: Abusing Unsafe Rust in Binary Reverse Engineering toward Finding Memory-safety Bugs via Machine Learning [20.68333298047064]
  Rustは、プログラミングにおけるメモリセーフなバグを避けるために、メモリセーフなメカニズムを提供する。 Rustのユーザビリティを高めるアンセーフコードは、メモリセーフなバグを見つけるための明確な場所を提供する。 これらの安全でないスポットは、マシンラーニングを介してRustバイナリコードで識別可能である、と私たちは主張しています。
  論文  参考訳（メタデータ） (2022-10-31T19:32:18Z)
• A first-order logic characterization of safety and co-safety languages [63.29821624186913]
  有限の接頭辞が、ある単語が言語に属していないか、属していないかを確立するのに十分である安全で共同安全な言語は、モデル検査や反応合成のような問題の複雑さを下げる上で重要な役割を果たす。 本稿では,安全性とコセーフティ言語に関して,FO-TLOの断片であるSafetyFOと,その二重コセーフティについて述べる。
  論文  参考訳（メタデータ） (2022-09-06T09:00:38Z)

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

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