論文の概要: Security Verification of Low-Trust Architectures
- arxiv url: http://arxiv.org/abs/2309.00181v1
- Date: Fri, 1 Sep 2023 00:22:24 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-19 07:03:01.479335
- Title: Security Verification of Low-Trust Architectures
- Title（参考訳）: 低トラストアーキテクチャのセキュリティ検証
- Authors: Qinhan Tan, Yonathan Fisseha, Shibo Chen, Lauren Biernacki, Jean-Baptiste Jeannin, Sharad Malik, Todd Austin,
- Abstract要約: 我々は、特定の低信頼アーキテクチャであるSequestered Encryption (SE)アーキテクチャの完全な形式検証を行う。
まず、SE低信頼アーキテクチャのISAのセキュリティ要件を定義します。
本稿では,これらの証明義務を商用の形式的検証ツールを用いてうまく解約できることを示す。
- 参考スコア（独自算出の注目度）: 2.7080187684202968
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Low-trust architectures work on, from the viewpoint of software, always-encrypted data, and significantly reduce the amount of hardware trust to a small software-free enclave component. In this paper, we perform a complete formal verification of a specific low-trust architecture, the Sequestered Encryption (SE) architecture, to show that the design is secure against direct data disclosures and digital side channels for all possible programs. We first define the security requirements of the ISA of SE low-trust architecture. Looking upwards, this ISA serves as an abstraction of the hardware for the software, and is used to show how any program comprising these instructions cannot leak information, including through digital side channels. Looking downwards this ISA is a specification for the hardware, and is used to define the proof obligations for any RTL implementation arising from the ISA-level security requirements. These cover both functional and digital side-channel leakage. Next, we show how these proof obligations can be successfully discharged using commercial formal verification tools. We demonstrate the efficacy of our RTL security verification technique for seven different correct and buggy implementations of the SE architecture.
- Abstract（参考訳）: 低信頼アーキテクチャは、ソフトウェアの観点からは、常に暗号化されたデータを使用し、ハードウェア信頼の量を小さなソフトウェアフリーなエンクレーブコンポーネントに大幅に削減する。
本稿では,特定の低信頼アーキテクチャであるSequestered Encryption (SE) アーキテクチャの完全検証を行い,その設計が全てのプログラムに対して直接データ開示やデジタルサイドチャネルに対して安全であることを示す。
まず、SE低信頼アーキテクチャのISAのセキュリティ要件を定義します。
上向きに見ると、このISAはソフトウェアのためのハードウェアの抽象化として機能し、これらの命令を構成するプログラムが、どのように情報を漏らすことができないかを示すために使用される。
下向きに見ると、このISAはハードウェアの仕様であり、ISAレベルのセキュリティ要件から生じるRTL実装の証明義務を定義するために使用される。
これらは、機能的およびデジタル的なサイドチャネルリークの両方をカバーする。
次に,これらの証明義務を,商用の形式的検証ツールを用いてうまく解約できることを示す。
我々は,SEアーキテクチャの7つの異なる正バグ実装に対するRTLセキュリティ検証手法の有効性を実証する。
関連論文リスト
- Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
認証サイクル冗長性チェック(ACRIC)を提案する。
ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。
ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
論文 参考訳（メタデータ） (2024-11-21T18:26:05Z) - VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL [4.652188875442064]
CHERIはハードウェアに直接、きめ細かいメモリ保護を提供し、強制する。
VeriCHERIはISA仕様を一切必要としないという点で、従来のものと概念的に異なる。
CHERIの変種を実装したRISC-Vベースのプロセッサ上で,VeriCHERIの有効性とスケーラビリティを示す。
論文 参考訳（メタデータ） (2024-07-26T11:48:55Z) - Stop Stealing My Data: Sanitizing Stego Channels in 3D Printing Design Files [56.96539046813698]
ステガノグラフィーチャネルは、印刷されたモデルを変更することなく、追加のデータをSTLファイル内に埋め込むことができる。
本稿では,ステガノグラフィーチャネルが存在する可能性のある隠されたコンテンツを消去するアンフェニタイザーを設計し,評価することで,このセキュリティ上の脅威に対処する。
論文 参考訳（メタデータ） (2024-04-07T23:28:35Z) - SISSA: Real-time Monitoring of Hardware Functional Safety and
Cybersecurity with In-vehicle SOME/IP Ethernet Traffic [49.549771439609046]
本稿では,車内機能安全とサイバーセキュリティをモデル化・解析するためのSOME/IP通信トラフィックベースアプローチであるSISSAを提案する。
具体的には、SISSAはWeibullディストリビューションでハードウェア障害をモデル化し、SOME/IP通信に対する5つの潜在的な攻撃に対処する。
広範囲な実験結果から,SISSAの有効性と有効性が確認された。
論文 参考訳（メタデータ） (2024-02-21T03:31:40Z) - Synthesizing Hardware-Software Leakage Contracts for RISC-V Open-Source Processors [6.061386291375516]
本稿では,オープンソースマイクロアーキテクチャのためのハードウェア・ソフトウェアリーク契約を合成する半自動手法を提案する。
我々はRISC-V ISAのためにこの手法をインスタンス化し、IbexおよびCVA6オープンソースプロセッサに適用した。
論文 参考訳（メタデータ） (2024-01-17T17:54:53Z) - 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) - Towards Remotely Verifiable Software Integrity in Resource-Constrained IoT Devices [18.163077388258618]
低コストのセキュリティアーキテクチャは、完全性証明を通じてソフトウェア状態のリモート検証のために提案されている。
この記事では、このアーキテクチャーファミリーの全体的かつ体系的な扱いについて述べます。
また、ソフトウェア完全性証明のタイプ、それぞれのアーキテクチャサポート、関連するコストを(適度かつ定量的に)比較します。
論文 参考訳（メタデータ） (2024-01-09T01:50:21Z) - Secure Instruction and Data-Level Information Flow Tracking Model for RISC-V [0.0]
不正アクセス、障害注入、およびプライバシー侵害は、信頼できないアクターによる潜在的な脅威である。
本稿では,実行時セキュリティがシステム完全性を保護するために,IFT(Information Flow Tracking)技術を提案する。
本研究では,ハードウェアベース IFT 技術とゲートレベル IFT (GLIFT) 技術を統合したマルチレベル IFT モデルを提案する。
論文 参考訳（メタデータ） (2023-11-17T02:04:07Z) - A Novel Approach to Identify Security Controls in Source Code [4.598579706242066]
本稿では,一般的なセキュリティ制御の包括的リストを列挙し,それぞれにデータセットを作成する。
最新のNLP技術であるBERT(Bidirectional Representations from Transformers)とTactic Detector(Tactic Detector)を使って、セキュリティコントロールを高い信頼性で識別できることを示しています。
論文 参考訳（メタデータ） (2023-07-10T21:14:39Z) - Safe RAN control: A Symbolic Reinforcement Learning Approach [62.997667081978825]
本稿では,無線アクセスネットワーク(RAN)アプリケーションの安全管理のためのシンボル強化学習(SRL)アーキテクチャを提案する。
我々は、ユーザが所定のセルネットワークトポロジに対して高レベルの論理的安全性仕様を指定できる純粋に自動化された手順を提供する。
ユーザがシステムに意図仕様を設定するのを支援するために開発されたユーザインターフェース(UI)を導入し、提案するエージェントの動作の違いを検査する。
論文 参考訳（メタデータ） (2021-06-03T16:45:40Z) - Symbolic Reinforcement Learning for Safe RAN Control [62.997667081978825]
無線アクセスネットワーク(RAN)アプリケーションにおける安全な制御のためのシンボリック強化学習(SRL)アーキテクチャを紹介します。
本ツールでは,LTL(Linear Temporal Logic)で表現された高レベルの安全仕様を選択して,所定のセルネットワーク上で動作しているRLエージェントをシールドする。
ユーザインタフェース(ui)を用いて,ユーザがインテントの仕様をアーキテクチャに設定し,許可されたアクションとブロックされたアクションの違いを検査する。
論文 参考訳（メタデータ） (2021-03-11T10:56:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。