論文の概要: PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
- arxiv url: http://arxiv.org/abs/2209.07936v2
- Date: Thu, 25 Apr 2024 03:04:32 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-27 00:37:16.468049
- Title: PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
- Title（参考訳）: PA-Boot: マルチプロセッサセキュアブートのための形式的に検証された認証プロトコル
- Authors: Zhuoruo Zhang, Chenyang Yu, Rui Chang, Mingshuai Chen, Bo Feng, He Huang, Qinming Dai, Wenbo Shen, Yongwang Zhao,
- Abstract要約: ハードウェアサプライチェーン攻撃は、マルチプロセッサ安全なブートをバイパスすることができる。
本稿では,マルチプロセッサシステムにおけるセキュアブートのためのプロセッサ認証プロトコルとして,PA-Bootを提案する。
- 参考スコア（独自算出の注目度）: 10.385759249667942
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. This paper identifies a new, prevalent hardware supply-chain attack surface that can bypass multiprocessor secure boot due to the absence of processor-authentication mechanisms. To defend against such attacks, we present PA-Boot, the first formally verified processor-authentication protocol for secure boot in multiprocessor systems. PA-Boot is proved functionally correct and is guaranteed to detect multiple adversarial behaviors, e.g., processor replacements, man-in-the-middle attacks, and tampering with certificates. The fine-grained formalization of PA-Boot and its fully mechanized security proofs are carried out in the Isabelle/HOL theorem prover with 306 lemmas/theorems and ~7,100 LoC. Experiments on a proof-of-concept implementation indicate that PA-Boot can effectively identify boot-process attacks with a considerably minor overhead and thereby improve the security of multiprocessor systems.
- Abstract（参考訳）: ハードウェアサプライチェーン攻撃は、マルチプロセッサシステムのブートプロセスに重大なセキュリティ脅威を引き起こしている。
本稿では,プロセッサ認証機構の欠如により,マルチプロセッサのセキュアブートを回避可能なハードウェアサプライチェーンアタックサーフェスを提案する。
このような攻撃に対する防御として,マルチプロセッサシステムにおけるセキュアブートのためのプロセッサ認証プロトコルとして,PA-Bootを提案する。
PA-Bootは機能的に正しいことが証明され、例えば、プロセッサ置換、man-in-the-middle攻撃、証明書の改ざんなど、複数の敵動作を検出することが保証されている。
PA-Bootの微細な形式化とその完全に機械化されたセキュリティ証明は、306 lemmas/theorems および ~7,100 LoC のIsabelle/HOL定理証明器で実行される。
概念実証実装の実験は、PA-Bootがブートプロセス攻撃をかなり小さなオーバーヘッドで効果的に識別でき、それによってマルチプロセッサシステムのセキュリティが向上することを示している。
関連論文リスト
- Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
認証サイクル冗長性チェック(ACRIC)を提案する。
ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。
ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
論文 参考訳（メタデータ） (2024-11-21T18:26:05Z) - A Scheduling-Aware Defense Against Prefetching-Based Side-Channel Attacks [16.896693436047137]
プリフェッチと呼ばれるメモリの投機的ロードは、現実世界のCPUでは一般的である。
プリフェッチは、RSA、AES、ECDH実装で使用されるキーなど、プロセス分離やリークシークレットをバイパスするために利用することができる。
我々はx86_64とARMプロセッサに対する対策を実装した。
論文 参考訳（メタデータ） (2024-10-01T07:12:23Z) - PACCOR4ESP: Embedded Device Security Attestation using Platform Attribute Certificates [0.3474871319204387]
本稿では、NSAサイバーセキュリティ局のプラットフォーム属性認証作成者(ESP32)の拡張を提案する。
このツールキットはファームウェアハッシュなどのESP32-S3からセキュリティ関連情報を抽出し、自動的にプラットフォーム属性証明書に埋め込む。
論文 参考訳（メタデータ） (2024-07-19T13:17:00Z) - A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。
本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。
実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
論文 参考訳（メタデータ） (2024-01-19T14:52:04Z) - ALPC Is In Danger: ALPChecker Detects Spoofing and Blinding [2.5782420501870296]
本研究は、カーネルを介してWindowsオペレーティングシステムにおけるALPC接続に対する攻撃を実装する可能性を評価することを目的とする。
ALPCは、アンチウイルスシステム(AV)や検出・応答システム(EDR)など、様々なWindows情報保護システムで使用されている。
論文 参考訳（メタデータ） (2023-12-30T16:58:28Z) - Tamper-Evident Pairing [55.2480439325792]
Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。
TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。
本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
論文 参考訳（メタデータ） (2023-11-24T18:54:00Z) - A Lightweight and Secure PUF-Based Authentication and Key-exchange Protocol for IoT Devices [0.0]
デバイス認証とキー交換はモノのインターネットにとって大きな課題である。
PUFは、PKIやIBEのような典型的な高度な暗号システムの代わりに、実用的で経済的なセキュリティメカニズムを提供するようだ。
認証を行うために,IoTデバイスがサーバと通信するための連続的なアクティブインターネット接続を必要としないシステムを提案する。
論文 参考訳（メタデータ） (2023-11-07T15:42:14Z) - Citadel: Real-World Hardware-Software Contracts for Secure Enclaves Through Microarchitectural Isolation and Controlled Speculation [8.414722884952525]
セキュアなエンクレーブのようなハードウェアアイソレーションプリミティブは、プログラムを保護することを目的としているが、一時的な実行攻撃には弱いままである。
本稿では,マイクロアーキテクチャの分離プリミティブと制御された投機機構をプロセッサに組み込むことを提唱する。
命令外プロセッサにおいて、エンクレーブと信頼できないOS間でメモリを安全に共有する2つのメカニズムを導入する。
論文 参考訳（メタデータ） (2023-06-26T17:51:23Z) - Practical quantum secure direct communication with squeezed states [55.41644538483948]
CV-QSDCシステムの最初の実験実験を行い,その安全性について報告する。
この実現は、将来的な脅威のない量子大都市圏ネットワークへの道を歩み、既存の高度な波長分割多重化(WDM)システムと互換性がある。
論文 参考訳（メタデータ） (2023-06-25T19:23:42Z) - When Authentication Is Not Enough: On the Security of Behavioral-Based Driver Authentication Systems [53.2306792009435]
我々はランダムフォレストとリカレントニューラルネットワークアーキテクチャに基づく2つの軽量ドライバ認証システムを開発した。
我々は,SMARTCANとGANCANという2つの新しいエスケープアタックを開発することで,これらのシステムに対する攻撃を最初に提案する。
コントリビューションを通じて、これらのシステムを安全に採用する実践者を支援し、車の盗難を軽減し、ドライバーのセキュリティを高める。
論文 参考訳（メタデータ） (2023-06-09T14:33:26Z) - Preprocessors Matter! Realistic Decision-Based Attacks on Machine
Learning Systems [56.64374584117259]
決定に基づく攻撃は、ハードラベルクエリのみを作成することによって、機械学習(ML)モデルに対する逆例を構築する。
我々は,(i)プリプロセッサをリバースエンジニアリングし,(ii)この抽出した情報を用いてエンド・ツー・エンド・システムを攻撃する手法を開発した。
我々のプリプロセッサ抽出法は数百のクエリしか必要とせず、我々のプリプロセッサ・アウェア・アタックはモデルのみを攻撃する場合と同じ効果を回復する。
論文 参考訳（メタデータ） (2022-10-07T03:10:34Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。