{"ID":2921823,"CreatedAt":"2026-06-02T02:42:49.606572591Z","UpdatedAt":"2026-06-03T05:56:00.181519634Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2606.01381","arxiv_id":"2606.01381","title":"Formal Verification of Secure Encrypted Virtualization","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.","short_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...","url_abs":"https://arxiv.org/abs/2606.01381","url_pdf":"https://arxiv.org/pdf/2606.01381v1","authors":"[\"Hansika Weerasena\",\"Amitabh Das\",\"Prabhat Mishra\"]","published":"2026-05-31T18:10:47Z","proceeding":"cs.CR","tasks":"[\"cs.CR\",\"cs.AR\"]","methods":"[]","has_code":false}