Formal Security Analysis of the AMD SEV-SNP Software Interface

AMD安全加密虚拟化技术可以通过保护虚拟机免受如超级管理程序等高特权软件的攻击，实现保密计算。本文开发了最新SEV迭代版本SEV Secure Nested Paging（SEV-SNP）软件接口的第一个全面的符号模型，包括远程证明、密钥派生、页面交换和实时迁移。我们通过验证关键的保密性、认证、证明和新鲜度属性来分析SEV-SNP软件接口的安全性，并发现在SNP guest和AMD安全处理器固件之间交换消息时，平台无关性设计存在弱点。我们展示了多种利用此弱点的方法，包括破坏证明报告完整性，并建议对设计进行轻微修改，以便第三方检测到Guest迁移到易受攻击的平台。

分析AMD安全加密虚拟化技术SEV-SNP的软件接口的安全性，发现其中存在弱点，提出了改进建议。

使用符号模型分析SEV-SNP的软件接口，验证其机密性、认证性、证明性和新鲜性等关键安全属性，发现消息的平台无关性存在弱点，提出了改进建议。

论文使用符号模型进行分析，提出了多种利用平台无关性弱点的攻击方式，包括破坏证明报告的完整性，提出了改进建议以便第三方检测到客户机迁移到易受攻击的平台。

最近在这个领域中，还有一些相关的研究，例如“SEVered: Subverting AMD's Virtual Machine Encryption”，“SEVurity: A Comprehensive Study of AMD Secure Encrypted Virtualization”，“A Formal Security Analysis of AMD's Secure Encrypted Virtualization”等。