論文の概要: Blame-aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation

• arxiv url: http://arxiv.org/abs/2610.26054v1
• Date: Mon, 19 Oct 2026 09:16:37 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-10-20 22:27:03.685376
• Title: Blame-aware Recomposition for Secure Compilation Proofs of Low-Level Compartment Isolation
• Title（参考訳）: 低レベル比較分離型セキュアコンパイル証明のためのブラムアウェア再構成法
• Abstract要約: Abate et al. の証明テクニックは、その証明ステップの1つ、再構成は、基本的に各コンパートメントのコードに関するすべての情報を隠さなければならないため失敗する。 本稿では,それらの証明手法を,コンパートメントが相互のコードを完全に観察できる低レベル設定に拡張することを提案する。
• 参考スコア（独自算出の注目度）: 0.9558392439655014
• License:
• Abstract: The security guarantees of existing formally verified compilers for compartmentalized programs in unsafe languages like C stop at a rather high level, assuming a built-in protection mechanism and a block-based memory model. Verifying a concrete, low-level enforcement mechanism for compartment isolation is still a major challenge for current proof techniques. In particular, Abate et al.'s proof technique fails because one of their proof steps, recomposition, essentially requires hiding all information about the code of each compartment, which is not practically achievable at a low level. We propose an extension of their proof technique to a low-level setting where compartments can fully observe each other's code. To do so, we introduce an overlay semantics that allows us to characterize these observations as a form of undefined behaviour, and we use a novel variant of recomposition that we call blame-aware recomposition, which essentially allows recomposing executions as needed in the original high-level proof technique, even if the low-level context observes the code, because this context is ultimately going to be discarded. We apply this new proof to a compartment isolation mechanism that uses a programmable tag-based reference monitor.
• Abstract（参考訳）: C言語のような安全でない言語において、既存のコンパイラのセキュリティ保証は、ビルトイン保護機構とブロックベースのメモリモデルを前提として、かなり高いレベルで停止する。 コンパートメント分離のための具体的かつ低レベルな強制機構を検証することは、現在の証明技術にとって依然として大きな課題である。 特に、Abate et al の証明テクニックは、その証明ステップの1つは、基本的には各区画のコードに関するすべての情報を隠さなければならないため失敗する。 本稿では,それらの証明手法を,コンパートメントが相互のコードを完全に観察できる低レベル設定に拡張することを提案する。 そのため、オーバーレイ・セマンティクスを導入して、これらの観測を未定義の振る舞いの形式として特徴づけることができ、また、我々は、最初に高レベルな証明技術で必要であったように実行を再コンパイルできるような、非難を意識した再コンパイルと呼ばれる、新しい種類の再コンパイルを使用します。 本稿では,この新たな証明を,プログラム可能なタグベースの参照モニタを用いたコンパートメント分離機構に適用する。

関連論文リスト

• Noisy Test-Time Reinforcement Learning for Code LLMs [49.18760234865557]
  大規模言語モデル(LLM)は、様々なコード関連タスクで顕著なパフォーマンスを示している。 LLMは曖昧でエラーを起こしやすいため、コードLLMの堅牢性には重大な課題がある。 本稿では,NTRL-Code(Noisy Test-time Reinforcement Learning framework)を提案する。
  論文  参考訳（メタデータ） (2026-09-26T02:50:47Z)
• The Illusion of High Utility in Safety Alignment of Text-to-Image Diffusion Models [49.67749928542536]
  テキスト・ツー・イメージ(T2I)拡散モデルの安全性の確保は,有害な世代を抑えることを目的としている。 近年の手法は高いユーティリティで高い安全性を提供するように思われるが、この結論は主に粗いグローバルユーティリティメトリクスに依存している。 構造的評価で実用性を測定すると、この錯覚は壊れる:OnA(質問回答を用いたテキストから画像への忠実度評価) 本研究では,組込み拡散とプロンプト間関係構造を明示的に保存する安全アライメント目標であるStructureAware Geometric Regularization (SAGE)を提案する。
  論文  参考訳（メタデータ） (2026-07-01T04:00:27Z)
• AutoSOUP: Safety-Oriented Unit Proof Generation for Component-level Memory-Safety Verification [10.258883626292265]
  メモリセーフティエラーは、低レベルソフトウェアにおけるゼロデイ脆弱性の永続的な原因である。 現在の検証はほとんど手作業で行われており、専門的な専門知識が必要である。 本稿では,コンポーネントレベルのメモリ安全性検証を自動化するシステムであるAutoSOUPを提案する。
  論文  参考訳（メタデータ） (2026-05-11T15:23:26Z)
• Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
  安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。 敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。 最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
  論文  参考訳（メタデータ） (2026-04-14T06:48:33Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  LLM(Large Language Models)は、コード生成において顕著な能力を示しているが、セキュアなコードを生成する能力は依然として重要で、未調査の領域である。 我々はRealSec-benchを紹介します。RealSec-benchは、現実世界の高リスクなJavaリポジトリから慎重に構築されたセキュアなコード生成のための新しいベンチマークです。
  論文  参考訳（メタデータ） (2026-01-30T08:29:01Z)
• zkStruDul: Programming zkSNARKs with Structural Duality [0.2449909275410287]
  zkStruDulは、入力変換を統一し、定義を単一の複合抽象化に述語する言語である。 我々は、ソースレベルのセマンティクスを提供し、その振る舞いが予測されたセマンティクスと同一であることを証明する。
  論文  参考訳（メタデータ） (2025-11-13T18:06:21Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)
• Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
  大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。 RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。 これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。 我々は、無害な」知識基盤の著作権保護の名称を提案する。
  論文  参考訳（メタデータ） (2025-02-10T09:15:56Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)

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

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