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.

翻译：可信执行环境（TEE）为使用中的数据与代码提供安全环境，确保其机密性与完整性得到保护。基于虚拟机（VM）的TEE利用虚拟化技术创建隔离执行空间，可支持完整的操作系统或特定应用程序。AMD安全加密虚拟化（SEV）是云计算机密计算中的关键技术，通过基于硬件的内存加密保护虚拟机内的敏感数据。然而，AMD SEV通常缺乏对其安全保证的形式化验证手段。本研究提出用于表示与验证AMD SEV机密虚拟机的形式化框架。具体而言，我们对AMD SEV规范进行设计级与属性级抽象，并在模型上执行属性检查以确保机密性、完整性和可用性。该方法为定义和验证保护执行环境的关键安全属性提供了严谨基础。