技术详解 | CertiK对蚂蚁集团HyperEnclave先进形式化验证

上周，CertiK宣布已完成了对蚂蚁集团可信原生技术团队开发的创新开放式跨平台可信执行环境（TEE）HyperEnclave的先进形式化验证。

为了实现保护Web3世界的使命，CertiK在审计过程中采用了一系列分析方法。这包括但不限于由人工审计员进行详细严谨的代码评审，通过模糊测试和静态分析发现程序错误、以及使用模型检测为标准协议提供程序正确性的数学证明。其中最强大的方法之一是使用机器验证的证明（即形式化验证）。

形式化验证既包括对标准属性的自动验证，例如使用模型检测，同时也包括更为先进的验证，即为特定项目制定定制化的安全属性并对其进行证明。

如下图所示，Web3应用程序依赖于其软件栈上的所有组件层次。智能合约的业务逻辑使用**编程语言编写，编译为字节码，并由区块链节点上的字节码虚拟机进行运行。链的节点执行其特定的代码来计算诸如质押等配置，以及共识算法。此外，区块链节点运行在物理云基础设施上，其中包括操作系统、虚拟机监视器、可信执行环境等系统软件。

在讨论Web3的安全性时，人们通常关注的焦点是位于其软件栈顶层的智能合约。而位于较低层级的软件组件是由多个不同的Web3应用程序共享的，因此它们经过了更多的测试，可能存在的错误较少。

但与此同时，这也使得它们变得更为重要：在区块链节点代码中的一个错误可能会危及该区块链上的所有应用程序，而系统基础设施中的一个错误则可能会危及整个Web3世界。

CertiK在机器验证证明方面的工作涵盖了Web3软件栈的每一层面。例如：

• 我们使用符号化模型检测自动验证ERC-20合约和其他实现标准接口的Solidity合约

• 我们验证了类似UniSwap的DeFi应用程序的智能合约，形式化验证是我们对Move和Cardano合约审计的一部分，我们为一些Solidity项目验证了定制属性

• 我们的DeepSEA验证编译器旨在排除编译过程中的错误

• 我们形式化验证了Coos SDK的标准银行模块

• 我们形式化验证了TON Chain的主链质押合约

这篇博文介绍了我们在Web3软件栈**层的一项工作：在最近发布的一份形式化验证报告中，我们将先进形式化验证应用在了由蚂蚁集团可信原生技术团队开发的HyperEnclave可信执行环境。

HyperEnclave 可信执行环境

可信执行环境（Trusted Execution Environment，TEE）的设计目的是保护应用程序免受一种**挑战性的攻击类型：那些甚至能够控制计算机操作系统的攻击方式。

一些最**的TEE包括英特尔的SGX、Arm TrustZone和AMD SEV。它们的工作原理是让CPU通过加密的方式证明特定的安全应用程序（enclave）已加载，并防止其他软件干扰它。

TEE已经融入到数字生活的许多方面。像苹果FileVault这样的磁盘加密软件、谷歌Authenticator这样的两步验证应用程序都将密钥存储于TEE中，即使有人**并拆解笔记本电脑或手机，密钥也能得到保护。

同时，在Web3中，TEE也变得越来越重要。数字货币钱包也使用TEE来更安全地存储加密密钥。分布式区块链预言机可以使用TEE来增加数据的真实性可信度。有提议将TEE用于“2-of-3系统”以帮助从零知识证明的实现错误中的恢复。

还有一些区块链项目，如LucidiTEE、SubstraTEE、Oasis Network和AntChain，则提议使用TEE为用户提供数据隐私保护。

目前，大多数TEE都是闭源的，并且与特定的硬件供应商绑定。例如，要使用Intel SGX，应用程序必须在Intel CPU上运行，并经过Intel的批准和白名单验证。但是硬件开发本身较慢，因此TEE的功能集较小，而且安全问题的解决需要对CPU固件进行更新。相比之下，HyperEnclave大部分是使用软件实现的，利用了两个广泛可用的硬件功能。

首先，计算机的可信平台模块（TPM，通常用于实现UEFI安全引导）用于验证HyperEnclave和一组特定的安全飞地（enclave）是否正在运行。其次，HyperEnclave使用CPU的虚拟化扩展来保护enclave（通常由虚拟机监视器如VMware、VirtualBox、Hyper-V、KVM等使用）。对于计算机硬件而言，HyperEnclave看起来就像任何其他的虚拟机监视器，但对于enclave来说，它提供了一个兼容SGX的API，使得针对SGX编写的应用程序可以轻松适应在HyperEnclave上运行。通过使用标准虚拟化技术，它可以轻松支持与操作系统紧密交互的高性能应用程序。

HyperEnclave中最关键的部分是称为RustMonitor的监视器，用于保护enclave免受来自其它enclave和来自操作系统的危险。enclave和操作系统在虚拟化的”guest”模式下执行，这意味着它们每次尝试访问内存时，所访问的内存地址首先通过由RustMonitor所管理的页表进行转换。通过将enclave放置在物理内存的不同区域中，RustMonitor可以确保它们永远无法读取或覆盖其他enclave所拥有的数据。但这不能仅仅是简单的静态分离：一些内存地址必须被允许重叠，以便enclave与操作系统进行通信，并且地址映射在处理页面中断时会被更新。

HyperEnclave的开发者编写了一组“页表必须遵守的不变性质”，其中定义了内存地址映射表的预期工作方式。例如，这包括诸如“如果且仅当虚拟地址位于ELRANGE中，该地址才会被映射到EPC中的物理页”等属性。详细性质请参阅形式化验证报告。任何违反了这些条件的错误都可能使整个HyperEnclave系统的安全保证无效化。

RustMonitor的设计采取了以下步骤来确保代码的可信性。首先，它保持了较小的规模——大约3000行独立于平台的代码，再加上差不多大小的x86架构特定的库代码。其次，它使用Rust语言编写——这是一种内存安全的语言，可以排除大部分的错误类别。然而，考虑到其重要性，人们仍然希望获得更高的安全性，并求助于形式化验证。

对HyperEnclave的RustMonitor 进行形式化验证

RustMonitor的页表管理代码是一个很好的验证目标，因为它既小巧、其安全性又很关键。类似于Web3智能合约的情况，对其投入精力进行形式化验证是可行的。在这个项目中，CertiK从页表必须遵守的不变性质入手，将它们从英语翻译成Coq形式化规范语言。然后，我们产生一份机器检查的证明，以证明当RustMonitor代码修改表格时，所得到的表格仍满足所有的不变性质。

事实上，我们的开发工作还要更进一步，因为我们还希望确保这些不变性质的设计是正确的、而且我们对其的Coq语言翻译是正确的。为此，我们在Coq中进一步指定了客户代码所应该能观察到的信息，并利用不变性质证明不会有其它的信息流（”不相干定理”）。所有这些证明放在一起，共同提供了一个强有力的保证，即页表管理在设计上和实现上都是正确的。

然而，证明TEE监控程序的正确性并不是一项简单的任务。像虚拟化监视器和操作系统内核这样的系统级程序大量使用低级代码，其涉及带有指针的数据结构、跳过类型抽象、以及为性能高度优化。直至今日，对此类程序的验证仍然是值得发表在**计算机科学期刊上的论文中的热门研究问题，对其每一行代码进行证明需要巨大的努力。

例如，seL4的初始证明用了20个人年，而Komodo花费了2个人年来验证与约650行C代码对应的汇编代码。这些项目中的代码是为了简化验证而重新专门编写的，与HyperEnclave很不同——后者已经投入生产并采用了Rust的惯用写法。基于现有技术水平，对所有代码进行验证在经济上并不切实际。另一个问题是，与其他编程语言相比，Rust的验证工具链并不成熟。通过编写手工的“模型”代码而不是实际代码，可以减轻验证的负担。一个例子是Sanctum TEE，一个验证研究项目。这种方法的缺点是，代码与抽象模型之间的不匹配可能会削弱任何关于模型的安全性或正确性属性，甚至使其无效化。

CertiK在解决这个问题上具备得天独厚的条件。我们的两位创始人，邵中教授和顾荣辉教授，是并发认证抽象层（CCAL）验证方法的发明者，他们用这种方法验证了世界上第一个并发认证操作系统内核CertiKOS，并验证了KVM虚拟化监视器seKVM和ARM机密计算架构。CCAL的基本思想是将程序中的所有函数划分为很多“层”，为每层编写其抽象模型，然后证明函数的实际代码实现了抽象模型，这显著降低了代码与抽象模型行为不匹配的风险。同试图将整个程序作为单个整体进行验证相比，分层方法更容易处理代码证明和并发问题。此前对seKVM和Arm CCA的工作在验证工业级系统软件项目方面受到了关注，而在这之前这类项目的规模对于形式化验证来说过于庞大。

HyperEnclave形式化验证团队包括之前参与CertiKOS和seKVM验证的人员，我们试图利用这些经验在安全保证和验证的资源投入之间取得良好的平衡。为此，我们使用了一种基于CCAL规范的弹性验证方法：我们的框架支持验证函数代码是否符合模型，但我们选择仅对一部分函数进行这项验证（49个直接处理内存页表的函数）。对于其他函数，我们则假定对Rust代码的手工Coq翻译是正确的，仅证明这些Coq模型的功能正确性。这里源码中所访问数据结构的抽象程度决定了每个函数是否需要验证其代码符合模型。当HyperEnclave使用**Rust数据结构时，我们直接将其转换到Coq，但当其使用基于字节的低级页表格式时，我们则花更多精力来证明其等效于**功能模型（详见完整形式化验证报告）。就RustMonitor而言，这意味着我们对处理页表表示的“Memory”模块进行了代码证明，对管理enclave状态的“Enclave”模块使用了抽象模型，然后结合所有产生的模型证明了不变性定理和顶层安全定理。

这个验证的另一个有趣的部分是如何进行代码证明。处理页表的HyperEnclave代码是低级代码，没有任何现有的验证工具能够很好地处理它。为此，我们开发了一个框架，通过转换为中间语言 MIR（Mid-level Intermediate Representation）来验证 Rust 代码，并用它来验证那些关键函数。由于MIR是一种较小的语言，我们能够为其编写精确的操作语义，并对编译器生成的 MIR 代码进行精确的验证，这使得我们的代码证明具有更坚实的基础，而不是依赖于任意的一个翻译器。

总的来说，这是一项庞大的工作，涉及到大约17,300行通过了Coq证明器验证的人工证明脚本。另有几千行的形式化规范，以及大量用于所导入的MIR代码和层结构而自动生成的Coq文件。证明的主要组成部分包括不相干性证明（6600行）、代码证明（4200行）和页表操作功能证明（4400行），以及与代码证明框架相关的定理。最终，这些证明汇集成一组定理，陈述了HyperEnclave主要系统调用的数据流不相干性，亦即私密性。

总结

可信执行环境（TEE）是云计算和Web3应用程序的一项基础技术，因此构建其安全性至关重要。在这个项目中，CertiK应用了先进形式化验证技术来验证其最重要的组件，从而提供了强有力的保证，确保其代码按照预期运行，并确实符合所期望的安全属性。

这项形式化验证工作只是确保隐私计算安全性的一环；它只涵盖了RustMonitor的页表管理部分，而RustMonitor又仅是整个系统中的一个组件。在未来，我们也将对其他隐私计算组件进行代码审核、测试和形式化验证。通过验证最核心的部分，我们为隐私云计算奠定了坚实的基础。