論文の概要: VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL
- arxiv url: http://arxiv.org/abs/2407.18679v1
- Date: Fri, 26 Jul 2024 11:48:55 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-29 13:40:43.541623
- Title: VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL
- Title(参考訳): VeriCHERI: RTLにおけるCHERIの暴露形式的セキュリティ検証
- Authors: Anna Lena Duque Antón, Johannes Müller, Philipp Schmitz, Tobias Jauch, Alex Wezel, Lucas Deutschmann, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz,
- Abstract要約: CHERIはハードウェアに直接、きめ細かいメモリ保護を提供し、強制する。
VeriCHERIはISA仕様を一切必要としないという点で、従来のものと概念的に異なる。
CHERIの変種を実装したRISC-Vベースのプロセッサ上で,VeriCHERIの有効性とスケーラビリティを示す。
- 参考スコア(独自算出の注目度): 4.652188875442064
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, requires a gap-free verification of CHERI's hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts. This paper presents VeriCHERI, a novel approach to security verification. It is conceptionally different from previous works in that it does not require any ISA specification. Instead of checking compliance with a golden ISA model, we check against well-established global security objectives of confidentiality and integrity. Fully covering these objectives, VeriCHERI uses as few as four unbounded properties to exhaustively prove or disprove any vulnerability. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant.
- Abstract(参考訳): 攻撃者からメモリ内のデータを保護することは、現在もコンピューティングシステムにおいて懸念されている。
CHERIは、ハードウェアに直接きめ細かいメモリ保護を提供することによって、そのような保護を達成するための有望なアプローチである。
しかし、システムスタック全体の信頼を作るには、CHERIのハードウェアベースの保護メカニズムのギャップのない検証が必要である。
CHERIの既存の検証方法は、基盤となるハードウェア実装ではなく抽象ISAモデルをターゲットにしている。
具体的なRTL実装に対するCHERIのセキュリティ保証を完全に保証することは、以前のフローにおける課題であり、高い手作業を要求する。
本稿では,セキュリティ検証の新しいアプローチであるVeriCHERIを提案する。
ISA仕様を必要としないという点で、以前のものと概念的に異なる。
黄金のISAモデルでコンプライアンスをチェックする代わりに、機密性と完全性という、確立したグローバルなセキュリティ目標をチェックします。
これらの目的を完全にカバーし、VeriCHERIは脆弱性を徹底的に証明または反証するために、わずか4つの無制限プロパティを使用する。
CHERIの変種を実装したRISC-Vベースのプロセッサ上で,VeriCHERIの有効性とスケーラビリティを示す。
関連論文リスト
- A False Sense of Safety: Unsafe Information Leakage in 'Safe' AI Responses [42.136793654338106]
大きな言語モデル(LLM)は、x2013$x2013$methodsのリークに対して脆弱である。
我々は、悪意ある目標を達成するために不寛容な情報を利用する推論敵と呼ばれる推論脅威モデルを導入する。
私たちの研究は、安全なジェイルブレイクを解放するための要件と、関連するユーティリティコストに関する、理論上は初めての理解を提供する。
論文 参考訳(メタデータ) (2024-07-02T16:19:25Z) - Securing the Open RAN Infrastructure: Exploring Vulnerabilities in Kubernetes Deployments [60.51751612363882]
ソフトウェアベースのオープン無線アクセスネットワーク(RAN)システムのセキュリティへの影響について検討する。
我々は、Near Real-Time RAN Controller(RIC)クラスタをサポートするインフラストラクチャに潜在的な脆弱性と設定ミスがあることを強調します。
論文 参考訳(メタデータ) (2024-05-03T07:18:45Z) - Poisoning Prevention in Federated Learning and Differential Privacy via Stateful Proofs of Execution [8.92716309877259]
フェデレートラーニング(FL)とローカルディファレンシャルプライバシ(LDP)は、ここ数年で多くの注目を集めています。
彼らは毒殺攻撃に弱いという共通の制限を共有している。
本稿では,国家執行の証明という新たなセキュリティ概念に基づいて,この問題を是正するシステムレベルのアプローチを提案する。
論文 参考訳(メタデータ) (2024-04-10T04:18:26Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳(メタデータ) (2024-01-19T14:52:04Z) - 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) - Blockchain-based Zero Trust on the Edge [5.323279718522213]
本稿では,ブロックチェーンに拡張されたゼロトラストアーキテクチャ(ZTA)に基づく新たなアプローチを提案し,セキュリティをさらに強化する。
ブロックチェーンコンポーネントは、ユーザの要求を格納するための不変データベースとして機能し、潜在的に悪意のあるユーザアクティビティを分析して識別することで、信頼性を検証するために使用される。
スマートシティにおけるその実現可能性と適用性を検証するために,テストベッド上で実施したフレームワーク,アプローチのプロセス,実験について論じる。
論文 参考訳(メタデータ) (2023-11-28T12:43:21Z) - Security Verification of Low-Trust Architectures [2.7080187684202968]
我々は、特定の低信頼アーキテクチャであるSequestered Encryption (SE)アーキテクチャの完全な形式検証を行う。
まず、SE低信頼アーキテクチャのISAのセキュリティ要件を定義します。
本稿では,これらの証明義務を商用の形式的検証ツールを用いてうまく解約できることを示す。
論文 参考訳(メタデータ) (2023-09-01T00:22:24Z) - Safety Margins for Reinforcement Learning [74.13100479426424]
安全マージンを生成するためにプロキシ臨界度メトリクスをどのように活用するかを示す。
Atari 環境での APE-X と A3C からの学習方針に対するアプローチを評価する。
論文 参考訳(メタデータ) (2023-07-25T16:49:54Z) - A security framework for quantum key distribution implementations [1.2815904071470707]
我々は、コヒーレント攻撃に対する有限鍵方式のセキュリティ証明を示す。
本証明では, 実環境実装への適用を容易にするため, 状態特性の最小化が要求される。
論文 参考訳(メタデータ) (2023-05-10T07:02:32Z) - Recursively Feasible Probabilistic Safe Online Learning with Control
Barrier Functions [63.18590014127461]
本稿では,CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
本研究では,ロバストな安全クリティカルコントローラの実現可能性について検討する。
次に、これらの条件を使って、イベントトリガーによるオンラインデータ収集戦略を考案します。
論文 参考訳(メタデータ) (2022-08-23T05:02:09Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳(メタデータ) (2021-06-03T16:45:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。