論文の概要: Formal Verification of Secure Encrypted Virtualization

• arxiv url: http://arxiv.org/abs/2606.01381v1
• Date: Sun, 31 May 2026 18:10:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-02 21:34:29.674825
• Title: Formal Verification of Secure Encrypted Virtualization
• Title（参考訳）: セキュア暗号化仮想化の形式的検証
• Authors: Hansika Weerasena, Amitabh Das, Prabhat Mishra,
• Abstract要約: AMDセキュア暗号化仮想化(SEV)は、クラウドの機密コンピューティングで使用される鍵となる技術である。 本研究は,AMD SEVの秘密と完全性を表現するための公式な枠組みを紹介する。 このアプローチは、実行環境を保護するための重要なセキュリティ属性を定義し検証するための厳格な基盤を提供する。
• 参考スコア（独自算出の注目度）: 2.595331128138709
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Trusted execution environments (TEEs) provide a secure environment for data and code in use, ensuring that they are protected with respect to confidentiality and integrity. Virtual machine (VM)-based TEEs utilize virtualization technology to create isolated execution spaces that can support a complete operating system or specific applications. AMD secure encrypted virtualization (SEV) is a key technology used in confidential computing in the cloud enabling hardware-based memory encryption to protect sensitive data within VMs. However, AMD SEV often operate without formal assurances of their security guarantees. Our research introduces a formal framework for representing and verifying AMD SEV confidential VMs. Specifically, we conduct design-level and property-level abstraction on AMD SEV specification and conduct property checking on the model to ensure confidentiality, integrity and availability. This approach provides a rigorous foundation for defining and verifying key security attributes for safeguarding execution environments.
• Abstract（参考訳）: 信頼された実行環境(TEE)は、使用中のデータとコードのセキュアな環境を提供し、機密性と整合性に関して保護されていることを保証する。 仮想マシン(VM)ベースのTEEは仮想化技術を利用して、完全なオペレーティングシステムや特定のアプリケーションをサポートする独立した実行スペースを作成する。 AMD安全な暗号化仮想化(SEV)は、ハードウェアベースのメモリ暗号化がVM内の機密データを保護できるようにするクラウドの機密コンピューティングで使われる重要な技術である。 しかし、AMD SEVはセキュリティ保証の正式な保証なしに運用されることが多い。 本研究は,AMD SEV機密VMの表現と検証を行うための公式なフレームワークを紹介する。 具体的には、AMD SEV仕様に設計レベルとプロパティレベルを抽象化し、モデルのプロパティチェックを行い、機密性、完全性、可用性を確保する。 このアプローチは、実行環境を保護するための重要なセキュリティ属性を定義し検証するための厳格な基盤を提供する。

関連論文リスト

• Contextual Safety Reasoning and Grounding for Open-World Robots [79.98924225712668]
  COREは、環境に関する事前の知識なしに、オンラインのコンテキスト推論、接地、執行を可能にする安全フレームワークである。 知覚の不確実性を考慮したCOREの確率論的安全性保証を提供する。 シミュレーションと実世界の実験を通じて、COREは目に見えない環境において、文脈的に適切な振る舞いを強制することを示した。
  論文  参考訳（メタデータ） (2026-02-23T15:51:23Z)
• Confidential Computing for Cloud Security: Exploring Hardware based Encryption Using Trusted Execution Environments [0.0]
  クラウドコンピューティングは、特に機密データの保護に関して、セキュリティの大きな課題を生み出しました。 この問題に対して、Confidential Computingは、ハードウェアベースのTrusted Execution Environments(TEEs)を使用して、処理中のデータをセキュアにするためのツールである。
  論文  参考訳（メタデータ） (2025-11-06T17:03:33Z)
• OS-Sentinel: Towards Safety-Enhanced Mobile GUI Agents via Hybrid Validation in Realistic Workflows [77.95511352806261]
  VLM(Vision-Language Models)を利用したコンピュータ利用エージェントは、モバイルプラットフォームのようなデジタル環境を操作する上で、人間のような能力を実証している。 我々は,明示的なシステムレベルの違反を検出するための形式検証器と,文脈的リスクとエージェント行動を評価するコンテキスト判断器を組み合わせた,新しいハイブリッド安全検出フレームワークOS-Sentinelを提案する。
  論文  参考訳（メタデータ） (2025-10-28T13:22:39Z)
• Zero-Trust Foundation Models: A New Paradigm for Secure and Collaborative Artificial Intelligence for Internet of Things [61.43014629640404]
  Zero-Trust Foundation Models (ZTFM)は、ゼロトラストセキュリティの原則をIoT(Internet of Things)システムの基盤モデル(FM)のライフサイクルに組み込む。 ZTFMは、分散、異質、潜在的に敵対的なIoT環境にわたって、セキュアでプライバシ保護のAIを可能にする。
  論文  参考訳（メタデータ） (2025-05-26T06:44:31Z)
• ACE: Confidential Computing for Embedded RISC-V Systems [1.545844275209198]
  本稿では,オープンソースのロイヤリティフリーな秘密計算技術である Assured Confidential Execution (ACE) を紹介する。 我々は、ACEの構築に使用した原則と方法論を提示し、他の組み込みシステムの開発にも適用できるかもしれない。
  論文  参考訳（メタデータ） (2025-05-19T11:32:43Z)
• VMGuard: Reputation-Based Incentive Mechanism for Poisoning Attack Detection in Vehicular Metaverse [52.57251742991769]
  車両メタバースガード(VMGuard)は、車両メタバースシステムをデータ中毒攻撃から保護する。 VMGuardは、参加するSIoTデバイスの信頼性を評価するために、評判に基づくインセンティブメカニズムを実装している。 当社のシステムは,従来は誤分類されていた信頼性の高いSIoTデバイスが,今後の市場ラウンドへの参加を禁止していないことを保証します。
  論文  参考訳（メタデータ） (2024-12-05T17:08:20Z)
• Formal Security Analysis of the AMD SEV-SNP Software Interface [0.0]
  AMD Secure Encrypted 技術は、仮想マシンをハイパーバイザのような特権の高いソフトウェアから保護することによって、機密計算を可能にする。 我々は、SEV Secure Nested Paging (SEV-SNP) と呼ばれる、最新のSEVイテレーションにおけるソフトウェアインターフェースの最初の包括的シンボリックモデルを開発する。
  論文  参考訳（メタデータ） (2024-03-15T13:39:55Z)
• 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)
• The Security and Privacy of Mobile Edge Computing: An Artificial Intelligence Perspective [64.36680481458868]
  Mobile Edge Computing (MEC)は、クラウドコンピューティングと情報技術(IT)サービスをネットワークのエッジで配信できるようにする新しいコンピューティングパラダイムである。 本稿では,人工知能(AI)の観点からMECのセキュリティとプライバシに関する調査を行う。 新たなセキュリティとプライバシの問題に加えて、AIの観点からの潜在的なソリューションにも重点を置いています。
  論文  参考訳（メタデータ） (2024-01-03T07:47:22Z)

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

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