上周，CertiK 宣布已完成了对蚂蚁集团可信原生技术团队开发的创新开放式跨平台可信执行环境（TEE）HyperEnclave 的先进形式化验证。
为了实现保护 Web 3 世界的使命，CertiK 在审计过程中采用了一系列分析方法。这包括但不限于由人工审计员进行详细严谨的代码评审，通过模糊测试和静态分析发现程序错误、以及使用模型检测为标准协议提供程序正确性的数学证明。其中最强大的方法之一是使用机器验证的证明（即形式化验证）。
形式化验证既包括对标准属性的自动验证，例如使用模型检测，同时也包括更为先进的验证，即为特定项目制定定制化的安全属性并对其进行证明。
如下图所示，Web 3 应用程序依赖于其软件栈上的所有组件层次。智能合约的业务逻辑使用高级编程语言编写，编译为字节码，并由区块链节点上的字节码虚拟机进行运行。链的节点执行其特定的代码来计算诸如质押等配置，以及共识算法。此外，区块链节点运行在物理云基础设施上，其中包括操作系统、虚拟机监视器、可信执行环境等系统软件。
在讨论 Web 3 的安全性时，人们通常关注的焦点是位于其软件栈顶层的智能合约。而位于较低层级的软件组件是由多个不同的 Web 3 应用程序共享的，因此它们经过了更多的测试，可能存在的错误较少。
但与此同时，这也使得它们变得更为重要：在区块链节点代码中的一个错误可能会危及该区块链上的所有应用程序，而系统基础设施中的一个错误则可能会危及整个 Web 3 世界。
CertiK 在机器验证证明方面的工作涵盖了 Web 3 软件栈的每一层面。例如：
我们使用符号化模型检测自动验证 ERC-20 合约和其他实现标准接口的 Solidity 合约
我们验证了类似 UniSwap 的 DeFi 应用程序的智能合约，形式化验证是我们对 Move 和 Cardano 合约审计的一部分，我们为一些 Solidity 项目验证了定制属性
我们的 DeepSEA 验证编译器旨在排除编译过程中的错误
我们形式化验证了 Cosmos SDK 的标准银行模块
我们形式化验证了 TON Chain 的主链质押合约
这篇博文介绍了我们在 Web 3 软件栈最底层的一项工作：在最近发布的一份形式化验证报告中，我们将先进形式化验证应用在了由蚂蚁集团可信原生技术团队开发的 HyperEnclave 可信执行环境。
HyperEnclave 可信执行环境
可信执行环境（Trusted Execution Environment，TEE）的设计目的是保护应用程序免受一种最具挑战性的攻击类型：那些甚至能够控制计算机操作系统的攻击方式。
一些最著名的 TEE 包括英特尔的 SGX、Arm TrustZone 和 AMD SEV。它们的工作原理是让 CPU 通过加密的方式证明特定的安全应用程序（enclave）已加载，并防止其他软件干扰它。
TEE 已经融入到数字生活的许多方面。像苹果 FileVault 这样的磁盘加密软件、谷歌 Authenticator 这样的两步验证应用程序都将密钥存储于 TEE 中，即使有人盗窃并拆解笔记本电脑或手机，密钥也能得到保护。
同时，在 Web 3 中，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 行独立于平台的代码，再加上差不多大小的 x 86 架构特定的库代码。其次，它使用 Rust 语言编写——这是一种内存安全的语言，可以排除大部分的错误类别。然而，考虑到其重要性，人们仍然希望获得更高的安全性，并求助于形式化验证。
对 HyperEnclave 的 RustMonitor 进行形式化验证
RustMonitor 的页表管理代码是一个很好的验证目标，因为它既小巧、其安全性又很关键。类似于 Web 3 智能合约的情况，对其投入精力进行形式化验证是可行的。在这个项目中，CertiK 从页表必须遵守的不变性质入手，将它们从英语翻译成 Coq 形式化规范语言。然后，我们产生一份机器检查的证明，以证明当 RustMonitor 代码修改表格时，所得到的表格仍满足所有的不变性质。
事实上，我们的开发工作还要更进一步，因为我们还希望确保这些不变性质的设计是正确的、而且我们对其的 Coq 语言翻译是正确的。为此，我们在 Coq 中进一步指定了客户代码所应该能观察到的信息，并利用不变性质证明不会有其它的信息流（"不相干定理"）。所有这些证明放在一起，共同提供了一个强有力的保证，即页表管理在设计上和实现上都是正确的。
然而，证明 TEE 监控程序的正确性并不是一项简单的任务。像虚拟化监视器和操作系统内核这样的系统级程序大量使用低级代码，其涉及带有指针的数据结构、跳过类型抽象、以及为性能高度优化。直至今日，对此类程序的验证仍然是值得发表在顶级计算机科学期刊上的论文中的热门研究问题，对其每一行代码进行证明需要巨大的努力。
例如，seL 4 的初始证明用了 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）是云计算和 Web 3 应用程序的一项基础技术，因此构建其安全性至关重要。在这个项目中，CertiK 应用了先进形式化验证技术来验证其最重要的组件，从而提供了强有力的保证，确保其代码按照预期运行，并确实符合所期望的安全属性。
这项形式化验证工作只是确保隐私计算安全性的一环；它只涵盖了 RustMonitor 的页表管理部分，而 RustMonitor 又仅是整个系统中的一个组件。在未来，我们也将对其他隐私计算组件进行代码审核、测试和形式化验证。通过验证最核心的部分，我们为隐私云计算奠定了坚实的基础。
