論文の概要: Formally-verified Security against Forgery of Remote Attestation using SSProve

• arxiv url: http://arxiv.org/abs/2502.17653v1
• Date: Mon, 24 Feb 2025 21:02:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-26 17:42:45.416487
• Title: Formally-verified Security against Forgery of Remote Attestation using SSProve
• Title（参考訳）: SSProveを用いた遠隔検診の偽造に対する形式的検証
• Authors: Sara Zain, Jannik Mähn, Stefan Köpsell, Sebastian Ertel,
• Abstract要約: 本稿では,RAの基本セキュリティ特性の機械的形式化について述べる。 まずデジタルシグネチャを定義し、強力な存在攻撃モデルにおいて、偽造に対するセキュリティを正式に検証する。 我々の開発は、RAプロトコルが偽造に対して安全であることを示す証拠を提供する。
• 参考スコア（独自算出の注目度）: 0.21427777919040417
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Remote attestation (RA) is the foundation for trusted execution environments in the cloud and trusted device driver onboarding in operating systems. However, RA misses a rigorous mechanized definition of its security properties in one of the strongest models, i.e., the semantic model. Such a mechanization requires the concept of State-Separating Proofs (SSP). However, SSP was only recently implemented as a foundational framework in the Rocq Prover. Based on this framework, this paper presents the first mechanized formalization of the fundamental security properties of RA. Our Rocq Prover development first defines digital signatures and formally verifies security against forgery in the strong existential attack model. Based on these results, we define RA and reduce the security of RA to the security of digital signatures. Our development provides evidence that the RA protocol is secure against forgery. Additionally, we extend our reasoning to the primitives of RA and reduce their security to the security of the primitives of the digital signatures. Finally, we found that proving the security of the primitives for digital signatures was not feasible. This observation contrasts textbook formalizations and sparks a discussion on reasoning about the security of libraries in SSP-based frameworks.
• Abstract（参考訳）: リモートテスト(RA)は、クラウド上での信頼性の高い実行環境と、オペレーティングシステムでオンボードされる信頼性の高いデバイスドライバの基礎である。 しかし、RAは、そのセキュリティ特性の厳密な機械的定義を最も強いモデルの一つ、すなわちセマンティックモデルで見逃している。 このような機械化は国家分離証明(SSP)の概念を必要とする。 しかし、SSPはRocq Proverの基盤フレームワークとして実装されたばかりであった。 本稿では,RAの基本セキュリティ特性の機械的形式化について述べる。 我々のRocq Prover開発は、まずデジタル署名を定義し、強力な存在的攻撃モデルにおける偽造に対するセキュリティを正式に検証します。 これらの結果に基づき、RAを定義し、RAのセキュリティをデジタル署名のセキュリティに還元する。 我々の開発は、RAプロトコルが偽造に対して安全であることを示す証拠を提供する。 さらに、私たちの推論をRAのプリミティブに拡張し、デジタルシグネチャのプリミティブのセキュリティに対するセキュリティを低減します。 最後に、デジタル署名のプリミティブのセキュリティを証明することは不可能であることがわかった。 この観察は、教科書の形式化とは対照的であり、SSPベースのフレームワークにおけるライブラリのセキュリティに関する推論に関する議論を引き起こしている。

関連論文リスト

• Provably Secure Retrieval-Augmented Generation [7.412110686946628]
  本稿では,RAG(Retrieval-Augmented Generation)システムのための,信頼性の高い最初のフレームワークを提案する。 我々のフレームワークは、検索したコンテンツとベクトル埋め込みの両方の二重保護を保証するために、プレストレージのフル暗号化方式を採用している。
  論文  参考訳（メタデータ） (2025-08-01T21:37:16Z)
• ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [49.47193675702453]
  大規模言語モデル(LLM)は、顕著な生成能力を示している。 LLMは、安全上の制約を回避できる悪意のある命令に弱いままである。 推論に基づく安全アライメントフレームワークARMORを提案する。
  論文  参考訳（メタデータ） (2025-07-14T09:05:54Z)
• Towards Provable (In)Secure Model Weight Release Schemes [5.177249919642388]
  最近のセキュアなウェイトリリーススキームは、モデルのオーナシップを保護し、誤用を防止しながら、オープンソースのモデル配布を可能にすると主張している。 これらのアプローチには厳格なセキュリティ基盤がなく、非公式なセキュリティ保証のみを提供する。 暗号の確立された研究に触発されて、いくつかの具体的なセキュリティ定義を導入することで、ウェイトリリーススキームのセキュリティを形式化する。
  論文  参考訳（メタデータ） (2025-06-23T11:57:41Z)
• LLM Agents Should Employ Security Principles [60.03651084139836]
  本稿では,大規模言語モデル(LLM)エージェントを大規模に展開する際には,情報セキュリティの確立した設計原則を採用するべきであることを論じる。 AgentSandboxは、エージェントのライフサイクル全体を通して保護を提供するために、これらのセキュリティ原則を組み込んだ概念的なフレームワークである。
  論文  参考訳（メタデータ） (2025-05-29T21:39:08Z)
• SVAFD: A Secure and Verifiable Co-Aggregation Protocol for Federated Distillation [10.234754822281774]
  フェデレート蒸留(FD)用に設計された最初のプロトコルであるSVAFDを提案する。 クライアントとサーバの責務を再定義する。 SVAFDはストラグラーやクライアントの衝突に耐性があり、現実世界のアプリケーションにおける動的ネットワークに適している。
  論文  参考訳（メタデータ） (2025-05-19T16:30:27Z)
• Privacy-Aware RAG: Secure and Isolated Knowledge Retrieval [7.412110686946628]
  本稿では,RAGシステムを不正アクセスやデータ漏洩から保護するための高度な暗号化手法を提案する。 当社のアプローチでは、ストレージに先立ってテキストコンテンツとそれに対応する埋め込みの両方を暗号化し、すべてのデータがセキュアに暗号化されていることを保証します。 以上の結果から,RAGシステムの設計と展開に高度な暗号化技術を統合することにより,プライバシー保護を効果的に強化できることが示唆された。
  論文  参考訳（メタデータ） (2025-03-17T07:45:05Z)
• 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)
• On the Design and Security of Collective Remote Attestation Protocols [5.01030444913319]
  Collective Remote Attestation (CRA)は、(異種)ネットワークにおいて、侵入されたデバイスを効率的に識別することを目的としたセキュリティサービスである。 ここ数年、CRAプロトコルの提案が大幅に増加し、様々なネットワークトポロジによってガイドされた様々な設計が示されている。 CRAプロトコルを体系的に比較可能な統合フレームワークであるCatを提示する。
  論文  参考訳（メタデータ） (2024-07-12T12:06:49Z)
• Generalized Quantum-assisted Digital Signature [2.187441808562386]
  本稿では,デジタル署名のためにQKDキーを採用することで,情報理論のセキュリティを継承する手法の改良版を提案する。 偽造に対するセキュリティは、悪意のある偽造者によって取られた試行錯誤アプローチを考慮して計算され、GQaDSパラメータは偽造と鑑定確率のバランスをとる分析的アプローチによって最適化される。
  論文  参考訳（メタデータ） (2024-06-28T15:04:38Z)
• Towards Credential-based Device Registration in DApps for DePINs with ZKPs [46.08150780379237]
  ブロックチェーン上のデバイス認証を検証するクレデンシャルベースのデバイス登録(CDR)機構を提案する。 本稿では,Groth16 と Marlin を用いた zkSNARK を用いた汎用システムモデルを提案し,CDR を技術的に評価する。
  論文  参考訳（メタデータ） (2024-06-27T09:50:10Z)
• Poisoning Prevention in Federated Learning and Differential Privacy via Stateful Proofs of Execution [8.92716309877259]
  フェデレートラーニング(FL)とローカルディファレンシャルプライバシ(LDP)は、ここ数年で多くの注目を集めています。 彼らは毒殺攻撃に弱いという共通の制限を共有している。 本稿では,国家執行の証明という新たなセキュリティ概念に基づいて,この問題を是正するシステムレベルのアプローチを提案する。
  論文  参考訳（メタデータ） (2024-04-10T04:18:26Z)
• A Zero Trust Framework for Realization and Defense Against Generative AI Attacks in Power Grid [62.91192307098067]
  本稿では電力グリッドサプライチェーン(PGSC)のための新しいゼロ信頼フレームワークを提案する。 潜在的なGenAIによる攻撃ベクターの早期発見、テールリスクに基づく安定性の評価、そしてそのような脅威の緩和を容易にする。 実験の結果,ゼロ信頼フレームワークは攻撃ベクトル生成に95.7%の精度,95%安定PGSCに9.61%のリスク尺度,GenAIによる攻撃に対する防御に99%の信頼性が得られた。
  論文  参考訳（メタデータ） (2024-03-11T02:47:21Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Tamper-Evident Pairing [55.2480439325792]
  Tamper-Evident Pairing (TEP)はPush-ButtonConfiguration (PBC)標準の改良である。 TEP は Tamper-Evident Announcement (TEA) に依存しており、相手が送信されたメッセージを検出せずに改ざんしたり、メッセージが送信された事実を隠蔽したりすることを保証している。 本稿では,その動作を理解するために必要なすべての情報を含む,TEPプロトコルの概要について概説する。
  論文  参考訳（メタデータ） (2023-11-24T18:54:00Z)
• Ring-A-Bell! How Reliable are Concept Removal Methods for Diffusion Models? [52.238883592674696]
  Ring-A-Bellは、T2I拡散モデルのためのモデルに依存しないレッドチームツールである。 これは、不適切なコンテンツの生成に対応する拡散モデルに対する問題的プロンプトを特定する。 この結果から,安全プロンプトベンチマークの操作により,既存の安全メカニズムを回避できると考えられるプロンプトを変換できることが示唆された。
  論文  参考訳（メタデータ） (2023-10-16T02:11:20Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。