Formal Verification of Secure Encrypted Virtualization

• URL: http://arxiv.org/abs/2606.01381v1
• Date: Sun, 31 May 2026 18:10:47 GMT
• Title: Formal Verification of Secure Encrypted Virtualization
• Abstract summary: AMD secure encrypted virtualization (SEV) is a key technology used in confidential computing in the cloud.<n>Our research introduces a formal framework for representing and verifying AMD SEV confidential and integrity.<n>This approach provides a rigorous foundation for defining and verifying key security attributes for safeguarding execution environments.
• Score: 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.

Related papers

• RAMSES: Secure high-performance computing for sensitive data [0.0]
  We present RAMSES, an HPC system designed from the ground up to deliver high performance within a robust security framework.<n> RAMSES integrates hardware-based memory of AMD processors with state-of-the-art file encryption from IBM Storage Scale.<n>In addition, we implemented advanced operating system hardening, a multi-layered security architecture, and mandatory multi-factor authentication to adapt the HPC environment to increased security demands.
  arXiv  Detail & Related papers  (2026-06-26T10:10:27Z)
• Contextual Safety Reasoning and Grounding for Open-World Robots [79.98924225712668]
  CORE is a safety framework that enables online contextual reasoning, grounding, and enforcement without prior knowledge of the environment.<n>We provide probabilistic safety guarantees for CORE that account for perceptual uncertainty.<n>We demonstrate through simulation and real-world experiments that CORE enforces contextually appropriate behavior in unseen environments.
  arXiv  Detail & Related papers  (2026-02-23T15:51:23Z)
• Confidential Computing for Cloud Security: Exploring Hardware based Encryption Using Trusted Execution Environments [0.0]
  Cloud computing has created a huge challenge of security, especially in terms of safeguarding sensitive data.<n>In response to this problem, Confidential Computing has been a tool seeking to secure data in processing by usage of hardware-based Trusted Execution Environments (TEEs)
  arXiv  Detail & Related papers  (2025-11-06T17:03:33Z)
• OS-Sentinel: Towards Safety-Enhanced Mobile GUI Agents via Hybrid Validation in Realistic Workflows [77.95511352806261]
  Computer-using agents powered by Vision-Language Models (VLMs) have demonstrated human-like capabilities in operating digital environments like mobile platforms.<n>We propose OS-Sentinel, a novel hybrid safety detection framework that combines a Formal Verifier for detecting explicit system-level violations with a Contextual Judge for assessing contextual risks and agent actions.
  arXiv  Detail & Related papers  (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 (ZTFMs) embed zero-trust security principles into the lifecycle of foundation models (FMs) for Internet of Things (IoT) systems.<n>ZTFMs can enable secure, privacy-preserving AI across distributed, heterogeneous, and potentially adversarial IoT environments.
  arXiv  Detail & Related papers  (2025-05-26T06:44:31Z)
• ACE: Confidential Computing for Embedded RISC-V Systems [1.545844275209198]
  We introduce the Assured Confidential Execution (ACE), an open-source and royalty-free confidential computing technology.<n>We present a set of principles and a methodology that we used to build ACE and that might be applied for developing other embedded systems.
  arXiv  Detail & Related papers  (2025-05-19T11:32:43Z)
• A performance analysis of VM-based Trusted Execution Environments for Confidential Federated Learning [0.0]
  Federated Learning (FL) is a distributed machine learning approach that has emerged as an effective way to address recent privacy concerns.<n>FL introduces the need for additional security measures as FL alone is still subject to vulnerabilities such as model and data poisoning and inference attacks.<n> Confidential Computing (CC) is a paradigm that, by leveraging hardware-based trusted execution environments (TEEs), protects the confidentiality and integrity of ML models and data.
  arXiv  Detail & Related papers  (2025-01-20T15:58:48Z)
• VMGuard: Reputation-Based Incentive Mechanism for Poisoning Attack Detection in Vehicular Metaverse [52.57251742991769]
  vehicular Metaverse guard (VMGuard) protects vehicular Metaverse systems from data poisoning attacks.<n>VMGuard implements a reputation-based incentive mechanism to assess the trustworthiness of participating SIoT devices.<n>Our system ensures that reliable SIoT devices, previously missclassified, are not barred from participating in future rounds of the market.
  arXiv  Detail & Related papers  (2024-12-05T17:08:20Z)
• Formal Security Analysis of the AMD SEV-SNP Software Interface [0.0]
  AMD Secure Encrypted technologies enable confidential computing by protecting virtual machines from highly privileged software such as hypervisors.<n>We develop the first, comprehensive symbolic model of the software interface of the latest SEV iteration called SEV Secure Nested Paging (SEV-SNP)
  arXiv  Detail & Related papers  (2024-03-15T13:39:55Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• The Security and Privacy of Mobile Edge Computing: An Artificial Intelligence Perspective [64.36680481458868]
  Mobile Edge Computing (MEC) is a new computing paradigm that enables cloud computing and information technology (IT) services to be delivered at the network's edge. This paper provides a survey of security and privacy in MEC from the perspective of Artificial Intelligence (AI) We focus on new security and privacy issues, as well as potential solutions from the viewpoints of AI.
  arXiv  Detail & Related papers  (2024-01-03T07:47:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.