01 简介

在TEE（即可信执行环境）的使用场景下，习以为常的系统服务不再被认为是“可信的”，并且由于TEE软件本身对安全的需求远高于普通在云部署的软件，因而在为TEE提供服务时往往需要考虑更多的安全因素。

VeriSMo利用形式化方法，为TEE提供了经严格证明可靠的安全服务，采取以准确的数学语言描述TEE所需考虑的安全因素和相应保护机制的方法，为TEE软件设计和TEE安全研究提供了一种新的解决思路。

02

TEE的应用场景和威胁模型

当前，TEE的应用场景主要集中在提供可信的云上机密计算服务。相VeriSMo如何保证TEE安全

TEE在运行时除了依赖于CPU，不可避免地需要用到内存，因此内存加密是TEE安全机制非常关键的组成部分。TEE在内存条上存放的数据通常经过CPU加密，这使得云服务提供商无法直接物理读取内存信息。

为了帮助TEE操作系统正确地管理加密内存和确保其完整性，VeriSMo基于AMD SEV-SNP提供的反向映射表提供了一套内存页管理的接口，在TEE操作系统需要与外界共享内存时，能够保证内存页在共享前清除机密数据。

VeriSMo还利用了AMD SEV-SNP特别引入的虚拟机特权级，将TEE内的操作系统和普通软件隔离，保证自身的正确运行（如下图所示）。此外，VeriSMo还采用了安全中断、加密通信等机制，为TEE内的安全保护提供支持。

利用以上机制，VeriSMo能够保证自身的机密性和完整性。除此之外：

• VeriSMo能保证正确地完成TEE操作系统启动时的初始化；

• VeriSMo能帮助TEE操作系统与外界之间的内存共享；

• VeriSMo保证TEE操作系统代码的完整性；

• VeriSMo维持加密通信机制的有效性；

• VeriSMo给云服务部署方提供TEE运行时环境的完整性报告。

04

Rust与形式化证明

VeriSMo在源码层面完整验证了一个系统软件，这项工作的独特之处不仅在于其发掘了TEE的secure monitor这一非常适合形式化方法的使用场景，而且在于其对Rust这一现代系统编程语言的特性和相关推理工具的应用。

借助Verus的帮助，VeriSMo巧妙地将一些安全需求编码进Rust的类型系统，这使得许多推理可以依赖于Rust的类型检查来完成。VeriSMo和Verus能做到这一点，是因为Rust的类型系统和其支撑的内存模型在某种意义上是分离逻辑的一种形式，不少分离逻辑中的推理方法得以较好地融入到Rust代码的推理和验证当中。

Rust是一门现代的系统编程语言，具有严格的强类型系统和基于所有权的内存模型。得益于这些设计及其衍生的引用机制，Rust能够在不需要手动管理内存的情况下，在编译时就确定内存回收的方法，从而保证内存安全。

然而，Rust的类型系统和内存模型也限制了它的表达能力，系统软件往往需要使用Rust语言的unsafe机制来突破这些限制，进而破坏Rust的内存安全保障。

形式化方法，指的是通过准确的数学语言来描述程序的执行环境、要求以及行为。这一方法使我们可以通过逻辑推理，对程序的性质及其在各种环境下运行情况进行验证，弥补了Rust内存安全方面的不足。这些验证基于严格逻辑推导得来，由逻辑和数学模型支撑，因此这些验证的结果可以被认为是准确可靠的。

需要注意的是，在保证内存安全的前提下TEE软件仍可能存在安全漏洞。形式化方法能够对TEE软件实现的正确性进行验证，基于此，我们能够对TEE软件实现的一些安全性质有更加准确清晰的认识。

05 丨VeriSMo 的贡献与不足丨

• VeriSMo准确描述了前文以自然语言描述的TEE威胁模型，明确定义了攻击者的攻击能力，并将这些数学描述用于VeriSMo的安全性质证明。在此基础上，VeriSMo建立了“机器层”模型，严格证明了其在硬件上运行时的机密性和完整性；

• VeriSMo结合Rust机制建立了“实现层”的模型，严格证明了其能够正确地提供服务。通过这两个模型的结合，VeriSMo证明了其能够正确地保证整个TEE的机密性和完整性等安全性质；

• 在论文给出的性能测试当中，VeriSMo作为安全模块几乎没有给TEE操作系统的运行带来额外开销。

然而，VeriSMo为TEE提供的服务较为底层，主要面向在TEE中运行的操作系统。尽管VeriSMo能在一定程度上保证TEE中的操作系统可靠性，但TEE操作系统在TEE中的可靠性和安全性问题仍有待进一步探索。