論文の概要: Detecting speculative leaks with compositional semantics

• arxiv url: http://arxiv.org/abs/2603.29800v1
• Date: Tue, 31 Mar 2026 14:32:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-01 15:25:03.719428
• Title: Detecting speculative leaks with compositional semantics
• Title（参考訳）: 構成意味論による投機的漏れの検出
• Authors: Xaver Fabian, Marco Guarnieri, Boris Köpf, Jose F. Morales, Marco Patrignani, Jan Reineke, Andres Sanchez,
• Abstract要約: 本稿では,投機的実行による情報フローの検出と,ソフトウェア防衛に関する推論を行う新しいフレームワークを提案する。 我々は,SMTソルバを利用して脆弱性を検出し,プログラムのセキュリティを検証するシンボリック分析ツールであるSpectectorを開発した。
• 参考スコア（独自算出の注目度）: 9.009704721347575
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Speculative execution enhances processor performance by predicting intermediate results and executing instructions based on these predictions. However, incorrect predictions can lead to security vulnerabilities, as speculative instructions leave traces in microarchitectural components that attackers can exploit. This is demonstrated by the family of Spectre attacks. Unfortunately, existing countermeasures to these attacks lack a formal security characterization, making it difficult to verify their effectiveness. In this paper, we propose a novel framework for detecting information flows introduced by speculative execution and reasoning about software defenses. The theoretical foundation of our approach is speculative non-interference (SNI), a novel semantic notion of security against speculative execution attacks. SNI relates information leakage observed under a standard non-speculative semantics to leakage arising under semantics that explicitly model speculative execution. To capture their combined effects, we extend our framework with a mechanism to safely compose multiple speculative semantics, each focussing on a single aspect of speculation. This allows us to analyze the complex interactions and resulting leaks that can arise when multiple speculative mechanisms operate together. On the practical side, we develop Spectector, a symbolic analysis tool that uses our compositional framework and leverages SMT solvers to detect vulnerabilities and verify program security with respect to multiple speculation mechanisms. We demonstrate the effectiveness of Spectector through evaluations on standard security benchmarks and new vulnerability scenarios.
• Abstract（参考訳）: 投機的実行は、中間結果を予測し、これらの予測に基づいて命令を実行することにより、プロセッサ性能を向上させる。 しかし、誤った予測は、攻撃者が悪用できるマイクロアーキテクチャーコンポーネントの痕跡を投機的指示が残すため、セキュリティ上の脆弱性につながる可能性がある。 これはSpectre攻撃のファミリーによって実証される。 残念ながら、これらの攻撃に対する既存の対策は、正式なセキュリティ特性を欠いているため、その有効性を検証することは困難である。 本稿では,投機的実行による情報フローの検出と,ソフトウェア防衛に関する推論を行う新しいフレームワークを提案する。 提案手法の理論的基礎は投機的非干渉(SNI)であり,投機的実行攻撃に対する新しいセマンティックなセキュリティ概念である。 SNIは、標準的な非投機的セマンティクスの下で観測された情報漏洩と、投機的実行を明示的にモデル化するセマンティクスの下で発生した漏洩とを関連付ける。 これらの組み合わせの効果を捉えるため、我々は複数の投機的セマンティクスを安全に構成する機構でフレームワークを拡張し、それぞれが投機的な一つの側面に焦点をあてる。 これにより、複雑な相互作用を分析し、複数の投機機構が協調して動作するときに発生するリークを発生させることができる。 実用面では、我々の構成フレームワークを使用し、SMTソルバを利用して脆弱性を検出し、複数の投機機構に関するプログラムセキュリティを検証するシンボリック分析ツールであるSpectectorを開発する。 標準セキュリティベンチマークと新たな脆弱性シナリオの評価を通じて、Spectectorの有効性を実証する。

関連論文リスト

• VIGIL: Defending LLM Agents Against Tool Stream Injection via Verify-Before-Commit [44.24310459184061]
  オープン環境で動作するLLMエージェントは、間接的なプロンプトインジェクションによるエスカレーションリスクに直面している。 制約的分離から検証前コミットプロトコルへパラダイムをシフトするフレームワークである textbfVIGIL を提案する。
  論文  参考訳（メタデータ） (2026-01-09T12:19:49Z)
• Servant, Stalker, Predator: How An Honest, Helpful, And Harmless (3H) Agent Unlocks Adversarial Skills [3.0620527758972496]
  本稿では,モデルコンテキストプロトコルに基づくエージェントシステムにおいて,新たな脆弱性クラスを特定し,解析する。 このアタックチェーンは、有害な緊急行動を生み出すために、個々に認可された個々のタスクをどのように編成するかを説明し、実証する。
  論文  参考訳（メタデータ） (2025-08-27T01:11:59Z)
• A Survey on Model Extraction Attacks and Defenses for Large Language Models [55.60375624503877]
  モデル抽出攻撃は、デプロイされた言語モデルに重大なセキュリティ脅威をもたらす。 この調査は、抽出攻撃と防御攻撃の包括的分類、機能抽出への攻撃の分類、データ抽出の訓練、およびプロンプトターゲット攻撃を提供する。 モデル保護,データプライバシ保護,迅速なターゲット戦略に編成された防御機構について検討し,その効果を異なる展開シナリオで評価する。
  論文  参考訳（メタデータ） (2025-06-26T22:02:01Z)
• Exploiting Inaccurate Branch History in Side-Channel Attacks [54.218160467764086]
  本稿では,リソース共有と競合が広く実装されているが文書化されていない2つの特徴,バイアスフリー分岐予測と分岐履歴推定にどのように影響するかを検討する。 これらの機能は、ブランチ履歴バッファ(BHB)の更新動作を不注意に修正し、悪意のある誤定義を引き起こす新しいプリミティブを作成することができる。 2つのSpectre攻撃、すなわちSpectre-BSEとSpectre-BHSと、BiasScopeと呼ばれるクロスプライマリ制御フローサイドチャネル攻撃である。
  論文  参考訳（メタデータ） (2025-06-08T19:46:43Z)
• Detecting speculative data flow vulnerabilities using weakest precondition reasoning [4.713817702376467]
  本稿では,データフローの脆弱性であるSpectre-STLとSpectre-PSFを最弱条件推論を用いて検出する手法を提案する。 文献における関連するアプローチを検証するために,本手法をリトマステストのスイートで検証する。
  論文  参考訳（メタデータ） (2025-04-27T07:02:15Z)
• Jailbreaking as a Reward Misspecification Problem [80.52431374743998]
  本稿では,この脆弱性をアライメントプロセス中に不特定性に対処する新たな視点を提案する。 本稿では,報酬の相違の程度を定量化し,その有効性を実証する指標ReGapを紹介する。 ReMissは、報酬ミスの空間で敵のプロンプトを生成する自動レッドチームリングシステムである。
  論文  参考訳（メタデータ） (2024-06-20T15:12:27Z)
• Kick Bad Guys Out! Conditionally Activated Anomaly Detection in Federated Learning with Zero-Knowledge Proof Verification [31.38942054994932]
  フェデレーテッド・ラーニング(FL)システムは敵の攻撃を受けやすい。 RedJasperは、現実世界のFLデプロイメント用に特別に設計された2段階の異常検出手法である。 第1段階で不審な活動を特定し、第2段階を条件付きで活性化し、不審な局所モデルをさらに精査する。
  論文  参考訳（メタデータ） (2023-10-06T07:09:05Z)
• DRSM: De-Randomized Smoothing on Malware Classifier Providing Certified Robustness [58.23214712926585]
  我々は,マルウェア検出領域の非ランダム化スムース化技術を再設計し,DRSM(De-Randomized Smoothed MalConv)を開発した。 具体的には,実行可能ファイルの局所構造を最大に保ちながら,逆数バイトの影響を確実に抑制するウィンドウアブレーション方式を提案する。 私たちは、マルウェア実行ファイルの静的検出という領域で、認証された堅牢性を提供する最初の人です。
  論文  参考訳（メタデータ） (2023-03-20T17:25:22Z)
• Short Paper: Static and Microarchitectural ML-Based Approaches For Detecting Spectre Vulnerabilities and Attacks [0.0]
  投機的侵入は、現代のプロセッサにおける投機的実行設計の脆弱性を悪用する。 現在の最先端検出技術は、これらの脅威を検出するために、微小構造的特徴または脆弱な投機的コードを利用する。 本稿では,静的・微構造解析支援機械学習によるSpectre脆弱性検出手法の総合評価を行う。
  論文  参考訳（メタデータ） (2022-10-26T03:55:39Z)
• Proper Network Interpretability Helps Adversarial Robustness in Classification [91.39031895064223]
  本稿では,解釈の適切な測定を行うことで,予測回避攻撃が解釈の不一致を引き起こすのを防ぐことは困難であることを示す。 我々は,頑健な解釈の促進にのみ焦点をあてて,解釈可能性に配慮した防御手法を開発した。 その結果,我々の防衛力は,強靭な分類と頑健な解釈の両方を達成し,大規模な摂動攻撃に対する最先端の対人訓練方法よりも優れていた。
  論文  参考訳（メタデータ） (2020-06-26T01:31:31Z)

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

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