論文の概要: SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
- arxiv url: http://arxiv.org/abs/2609.17399v1
- Date: Tue, 15 Sep 2026 16:33:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-16 14:56:08.619618
- Title: SCHERI: Provably Secure Speculation Under the Constant-Time Policy for CHERI (Extended Version)
- Title(参考訳): SCHERI: CHERI(Extended Version)の定時ポリシーの下でのおそらくセキュアな推測
- Abstract要約: 我々は,CHERIに対して安全な投機を提供することは自明であり,既存の提案では機密性保証の維持に失敗していることを示す。
本稿では,このフレームワーク内での新しいプロセッサ設計であるSCHERIについて述べる。
- 参考スコア(独自算出の注目度): 9.43713777107964
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Capability-based architectures such as CHERI provide strong support for the architectural isolation of software components. To additionally protect against microarchitectural leakage, software can be written in a constant-time fashion. Modern processors, however, rely heavily on speculative execution, which can invalidate the constant-time guarantees and leak isolated secrets transiently. In this work, we show that providing secure speculation for CHERI is non-trivial, and that existing proposals fail to preserve the confidentiality guarantees. We develop a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security, and use it to demonstrate potential leaks. We then present SCHERI, a new processor design within this framework, and formally prove that it provides end-to-end secure speculation guarantees for the constant-time policy. Our results provide formal foundations and practical guidance for building future capability-based processors, which are resilient to Spectre attacks for constant-time programs.
- Abstract(参考訳): CHERIのような機能ベースのアーキテクチャは、ソフトウェアコンポーネントのアーキテクチャ分離を強力にサポートします。
マイクロアーキテクチャの漏洩を防止するため、ソフトウェアは一定時間で書ける。
しかし、現代のプロセッサは投機的実行に大きく依存しており、一定の時間保証を無効にし、孤立したシークレットを透過的にリークすることができる。
本研究は,CHERIに対する安全な投機を提供することは容易ではなく,既存の提案では機密性保証の維持に失敗していることを示す。
我々は、機能安全性、投機的実行、情報フローセキュリティを共同で推論するための公式なフレームワークを開発し、潜在的なリークを示すためにそれを使用する。
次に、このフレームワーク内での新しいプロセッサ設計であるSCHERIを提示し、その定数時間ポリシーに対して、エンドツーエンドのセキュアな憶測を提供することを正式に証明する。
本研究は,定時プログラムにおけるSpectre攻撃に対する耐性の高い,将来的な機能ベースのプロセッサ構築のための公式な基礎と実践的ガイダンスを提供する。
関連論文リスト
- SeClaw: Spec-Driven Security Task Synthesis for Evaluating Autonomous Agents [87.26967184869198]
SeClawは、仕様駆動のセキュリティタスク合成と、自律エージェントの実行ベースのセキュリティ評価を組み合わせたフレームワークである。
ベンチマークは、リソース、ユーザタスク、環境、本質的なエージェントの振る舞いから生じるリスクをカバーしている。
論文 参考訳(メタデータ) (2026-06-01T14:23:42Z) - Provably Secure Agent Guardrail [89.79561918065122]
既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。
本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
論文 参考訳(メタデータ) (2026-05-28T02:12:41Z) - 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) - CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
AIエージェントは、悪意のあるコンテンツがエージェントの行動をハイジャックして認証情報を盗んだり、金銭的損失を引き起こすような、インジェクション攻撃に弱い。
CUAのためのシングルショットプランニングでは、信頼できるプランナーが、潜在的に悪意のあるコンテンツを観察する前に、条件付きブランチで完全な実行グラフを生成する。
このアーキテクチャ分離は命令インジェクションを効果的に防止するが、ブランチステアリング攻撃を防ぐには追加の対策が必要であることを示す。
論文 参考訳(メタデータ) (2026-01-14T23:06:35Z) - Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
大規模言語モデル(LLM)ベースのAIエージェントは、データソース、API、検索エンジン、コードサンドボックス、さらにはその他のエージェントなどのツールへのアクセスを可能にすることで、機能を拡張する。
LLMは意図しないツールインタラクションを起動し、機密データを漏洩したり、クリティカルレコードを上書きしたりするリスクを発生させる。
モデルベースセーフガードのようなリスクを軽減するための現在のアプローチは、エージェントの信頼性を高めるが、システムの安全性を保証することはできない。
論文 参考訳(メタデータ) (2026-01-12T21:31:38Z) - TICAL: Trusted and Integrity-protected Compilation of AppLications [0.24919281650930603]
Ticalは信頼できるコンパイルのためのフレームワークで、ソースコードから最終実行ファイルまでのビルドパイプラインの完全性と機密性を提供する。
当社のアプローチでは,TEEをランタイム保護として活用するが,ファイルシステムの保護とバージョン履歴による不変監査ログにより,TEEを充実させ,説明責任を提供します。
評価の結果,TicalはCI/CDパイプライン全体の機密性と整合性を,許容可能なパフォーマンスオーバーヘッドで保護できることがわかった。
論文 参考訳(メタデータ) (2025-11-21T09:19:41Z) - Performance and Storage Analysis of CRYSTALS Kyber as a Post Quantum Replacement for RSA and ECC [45.88028371034407]
CRYSTALS-Kyberは、2022年にNISTによって標準化されたポスト量子暗号ソリューションである。
本研究は,様々な実装方式における性能試験を通じて,Kyberの実用可能性を評価する。
論文 参考訳(メタデータ) (2025-08-03T09:53:45Z) - Security Enclave Architecture for Heterogeneous Security Primitives for Supply-Chain Attacks [7.9837065464150685]
本稿では,複数の攻撃ベクトルに対処可能な統一セキュリティアーキテクチャを構築する際に発生する障害の範囲について検討する。
様々なASIC技術におけるシリコン領域と電力消費への影響を徹底的に評価する。
論文 参考訳(メタデータ) (2025-07-15T04:28:02Z) - VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
CHERIはハードウェアに直接、きめ細かいメモリ保護を提供し、強制する。
VeriCHERIはISA仕様を一切必要としないという点で、従来のものと概念的に異なる。
CHERIの変種を実装したRISC-Vベースのプロセッサ上で,VeriCHERIの有効性とスケーラビリティを示す。
論文 参考訳(メタデータ) (2024-07-26T11:48:55Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳(メタデータ) (2024-01-17T00:56:23Z) - 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) - Systematic Prevention of On-Core Timing Channels by Full Temporal Partitioning [13.313360308792198]
本稿では,脆弱なミクロ構造体をクリアするために必要なメカニズムを提供する,時間的フェンス命令フェンス.tを紹介する。
我々は、seL4マイクロカーネルの実験バージョンに fence.tを実装し、64ビットRISC-VコアであるCVA6を実装した。
すべての非構造コアコンポーネントの完全かつ体系的なISAサポートの消去が、最も効果的な実装であることがわかった。
論文 参考訳(メタデータ) (2022-02-24T11:17:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。