该论文针对AMD SEV（安全加密虚拟化）技术缺乏形式化安全保证的问题，提出了一套形式化验证框架。AMD SEV是机密计算中的关键技术，通过硬件内存加密保护虚拟机内敏感数据。然而，现有实现缺乏对安全性属性的严格证明。研究首先对AMD SEV规范进行设计级和属性级抽象，建立精确的模型，然后通过属性检查（property checking）验证机密性、完整性和可用性（CIA三元组）。该方法为定义和验证执行环境的关键安全属性提供了严谨的数学基础。实验表明，该框架能够有效捕获规范中的安全约束，并发现潜在的安全缺口。该工作适用于安全架构师、云服务提供商和形式化方法研究人员，有助于提升对AMD SEV安全性的信任度。