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

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

CertiK完成对蚂蚁集团可信执行环境HyperEnclave的形式化验证

上周,CertiK宣布已完成了对蚂蚁集团可信原生技术团队开发的创新开放式跨平台可信执行环境(TEE)HyperEnclave的先进形式化验证。为了实现保护Web3世界的使命,CertiK在审计过程中采用了一系列分析方法,包括了形式化验证。

形式化验证是一种强大的验证方法,不仅可以对标准属性进行自动验证,还可以为特定项目制定定制化的安全属性并对其进行证明。在Web3应用程序中,不同层次的软件组件共同构成了整个系统。智能合约的业务逻辑使用高级编程语言编写,并通过字节码虚拟机在区块链节点上运行。区块链节点运行在物理云基础设施上,包括操作系统、虚拟机监视器和可信执行环境等系统软件。在这个系统中,不同层级的软件组件都需要经过验证,因为一个错误可能会危及整个Web3世界。

CertiK在形式化验证方面的工作涵盖了Web3软件栈的各个层面。它们在验证ERC-20合约和其他实现标准接口的Solidity合约时使用符号化模型检测自动验证。对类似UniSwap的DeFi应用程序的智能合约进行验证时,形式化验证是他们对Move和Cardano合约审计的一部分。对于一些Solidity项目,CertiK验证了定制属性。此外,他们还开发了DeepSEA验证编译器用于排除编译过程中的错误,并形式化验证了Cosmos SDK的标准银行模块和TON Chain的主链质押合约。

本篇文章将着重介绍CertiK在Web3软件栈最底层的工作。最近,CertiK完成了对由蚂蚁集团可信原生技术团队开发的HyperEnclave可信执行环境的形式化验证。HyperEnclave是一种可信执行环境(TEE),旨在保护应用程序免受控制计算机操作系统的攻击。

可信执行环境在数字生活的许多方面都得到了应用。例如,诸如苹果FileVault的磁盘加密软件和谷歌Authenticator的两步验证应用程序都使用了TEE来存储密钥,有效保护了用户的数据安全。在Web3中,可信执行环境也变得越来越重要。数字货币钱包使用TEE来更安全地存储加密密钥,分布式区块链预言机使用TEE来增加数据的真实性可信度,一些区块链项目还将TEE用于数据隐私保护。

目前,大多数TEE都是闭源的,并与特定的硬件供应商绑定。然而,HyperEnclave主要是通过软件实现的,并利用了广泛可用的硬件功能。它使用计算机的可信平台模块(TPM)验证HyperEnclave和一组特定的安全飞地是否正在运行,并使用CPU的虚拟化扩展保护飞地。其中最关键的部分是RustMonitor监视器,用于保护飞地免受其他飞地和操作系统的危险。

CertiK对HyperEnclave的RustMonitor进行了形式化验证。RustMonitor的页表管理代码是一个关键但小巧的验证目标。他们使用了基于CCAL规范的弹性验证方法,将必须遵守的不变性质从英语翻译成Coq形式化规范语言,并生成了机器检查的证明,证明了RustMonitor代码修改页表后仍满足所有的不变性质。这项验证工作涉及到大量的人工证明脚本和形式化规范,以及代码证明框架和MIR中间语言的开发。

总的来说,CertiK的形式化验证工作为保护Web3世界提供了强有力的保证。他们在Web3软件栈的各个层面进行了验证工作,包括智能合约、DeFi应用程序、编译器和区块链模块等。通过对可信执行环境HyperEnclave的形式化验证,CertiK为Web3应用程序的开发提供了更高的安全性和保护性。这项工作将为隐私云计算的实施奠定坚实的基础,同时也为其他隐私计算组件的代码审核和形式化验证提供了借鉴和参考。