論文の概要: 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の有効性とスケーラビリティを示す。
関連論文リスト
- Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
認証サイクル冗長性チェック(ACRIC)を提案する。
ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。
ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
論文 参考訳（メタデータ） (2024-11-21T18:26:05Z) - Nothing in Excess: Mitigating the Exaggerated Safety for LLMs via Safety-Conscious Activation Steering [56.92068213969036]
重大言語モデル(LLM)が悪意のある命令から脅威を守るためには、安全性の調整が不可欠である。
近年の研究では、過大な安全性の問題により、安全性に配慮したLCMは、良質な問い合わせを拒否する傾向にあることが明らかになっている。
過大な安全性の懸念を和らげるために,SCANS法を提案する。
論文 参考訳（メタデータ） (2024-08-21T10:01:34Z) - 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) - 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 [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳（メタデータ） (2021-06-03T16:45:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。