論文の概要: SpecIBT: Formally Verified Protection Against Speculative Control-Flow Hijacking
- arxiv url: http://arxiv.org/abs/2601.22978v1
- Date: Fri, 30 Jan 2026 13:42:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-02 18:28:15.477531
- Title: SpecIBT: Formally Verified Protection Against Speculative Control-Flow Hijacking
- Title（参考訳）: SpecIBT: 投機的制御フローハイジャックに対する正式に検証された保護
- Authors: Jonathan Baumann, Yonghyun Kim, Yan Farba, Catalin Hritcu, Julay Leatherman-Brooks,
- Abstract要約: SpecIBTは、正式にはSpectre BTB、RSB、PHTに対する防衛である。
CETスタイルのハードウェア支援制御フロー整合性と、コンパイラを挿入した投機的負荷硬化を組み合わせる。
- 参考スコア（独自算出の注目度）: 2.684996629761352
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper introduces SpecIBT, a formally verified defense against Spectre BTB, RSB, and PHT that combines CET-style hardware-assisted control-flow integrity with compiler-inserted speculative load hardening (SLH). SpecIBT is based on the novel observation that in the presence of CET-style protection, we can precisely detect BTB misspeculation for indirect calls and set the SLH misspeculation flag. We formalize SpecIBT as a transformation in Rocq and provide a machine-checked proof that it achieves relative security: any transformed program running with speculation leaks no more than what the source program leaks without speculation. This strong security guarantee applies to arbitrary programs, even those not following the cryptographic constant-time programming discipline.
- Abstract（参考訳）: 本稿では、CETスタイルのハードウェア支援制御フロー整合性と、コンパイラ挿入型投機負荷硬化(SLH)を組み合わせた、Spectre BTB, RSB, PHTに対する公式な防御であるSpecIBTを紹介する。
SpecIBTは、CETスタイルの保護が存在する場合、間接呼び出しのためのBTB誤特定を正確に検出し、SLH誤特定フラグを設定するという新しい観察に基づいている。
我々は、SpecIBTをRocqの変換として形式化し、相対的なセキュリティを実現するためのマシンチェックされた証明を提供する。
この強力なセキュリティ保証は、暗号定時プログラミングの原則に従わなくても、任意のプログラムに適用できる。
関連論文リスト
- Unsupervised Conformal Inference: Bootstrapping and Alignment to Control LLM Uncertainty [49.19257648205146]
生成のための教師なし共形推論フレームワークを提案する。
我々のゲートは、分断されたUPPよりも厳密で安定した閾値を提供する。
その結果は、ラベルのない、API互換の、テスト時間フィルタリングのゲートになる。
論文 参考訳（メタデータ） (2025-09-26T23:40:47Z) - Exploiting Inaccurate Branch History in Side-Channel Attacks [54.218160467764086]
本稿では,リソース共有と競合が広く実装されているが文書化されていない2つの特徴,バイアスフリー分岐予測と分岐履歴推定にどのように影響するかを検討する。
これらの機能は、ブランチ履歴バッファ(BHB)の更新動作を不注意に修正し、悪意のある誤定義を引き起こす新しいプリミティブを作成することができる。
2つのSpectre攻撃、すなわちSpectre-BSEとSpectre-BHSと、BiasScopeと呼ばれるクロスプライマリ制御フローサイドチャネル攻撃である。
論文 参考訳（メタデータ） (2025-06-08T19:46:43Z) - CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
物理ECUアクティベーションに基づく最初の決定論的侵入検知・防止システムであるCANTXSecを提案する。
CANバスの古典的な攻撃を検知・防止し、文献では調査されていない高度な攻撃を検知する。
物理テストベッド上での解法の有効性を実証し,攻撃の両クラスにおいて100%検出精度を達成し,100%のFIAを防止した。
論文 参考訳（メタデータ） (2025-05-14T13:37:07Z) - FSLH: Flexible Mechanized Speculative Load Hardening [0.1398098625978622]
Spectreの投機的サイドチャネル攻撃は、セキュリティに深刻な脅威をもたらす。
研究によると、暗号定時規律に従っているコードは、Spectre v1に対して効率的に保護できる。
Selective SLH と Ultimate SLH の両方を一般化することにより、両世界のベストを達成できるフレキシブルSLH の概念を導入する。
論文 参考訳（メタデータ） (2025-02-05T14:23:43Z) - Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
我々は、新しいハイブリッドユニバーサルネットワーク符号化暗号(NU-HUNCC)を導入する。
NU-HUNCCは,リンクのサブセットにアクセス可能な盗聴者に対して,個別に情報理論的に保護されていることを示す。
論文 参考訳（メタデータ） (2024-02-13T12:12:39Z) - DECLASSIFLOW: A Static Analysis for Modeling Non-Speculative Knowledge to Relax Speculative Execution Security Measures (Full Version) [9.816078445230305]
投機的実行攻撃は、定数時間プログラミングのセキュリティを損なう。
本稿では,提案するDECLASSIFLOWを用いて,投機的漏洩から一定時間コードを効率よく保護する。
論文 参考訳（メタデータ） (2023-12-14T21:00:20Z) - Tamper-Evident Pairing [55.2480439325792]
Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。
TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。
本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
論文 参考訳（メタデータ） (2023-11-24T18:54:00Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。