AMD Secure Encrypted Virtualization technologies enable confidential computing by protecting virtual machines from highly privileged software such as hypervisors. In this work, we develop the first, comprehensive symbolic model of the software interface of the latest SEV iteration called SEV Secure Nested Paging (SEV-SNP). Our model covers remote attestation, key derivation, page swap and live migration. We analyze the security of the software interface of SEV-SNP by verifying critical secrecy, authentication, attestation and freshness properties, and find that the platform-agnostic nature of messages exchanged between SNP guests and the AMD Secure Processor firmware presents a weakness of the design. We show multiple ways of exploiting this weakness, including the compromise of attestation report integrity, and suggest slight modifications to the design which let third parties detect guest migrations to vulnerable platforms

翻译：AMD安全加密虚拟化技术通过保护虚拟机免受诸如虚拟机监控程序等高特权软件的攻击，实现了机密计算。在本工作中，我们为最新迭代版本SEV安全嵌套分页（SEV-SNP）的软件接口构建了首个全面的符号模型。我们的模型涵盖了远程证明、密钥派生、页面交换和实时迁移。我们通过验证关键的安全性、认证性、证明性和新鲜性属性来分析SEV-SNP软件接口的安全性，发现SNP客户机与AMD安全处理器固件之间交换的消息的平台无关性构成了该设计的一个弱点。我们展示了利用此弱点的多种方式，包括破坏证明报告完整性，并提出了对设计的细微修改建议，以使第三方能够检测客户机是否迁移至易受攻击的平台。