Technical Explanation: CertiK's Advanced Formal Verification of Ant Group's HyperEnclave (Note: This is the translated version)
Last week, CertiK announced that it has completed advanced formal verification of HyperEnclave, an innovative open cross-platform trusted execution environment (TEE) developed by the Ant Group's trusted native technology team.
In order to fulfill its mission of protecting the Web 3 world, CertiK employed a series of analysis methods during the auditing process. This includes but is not limited to detailed and rigorous code review by human auditors, discovering program errors through fuzz testing and static analysis, and providing mathematical proofs of program correctness using model checking as a standard protocol. One of the most powerful methods is machine-verified proof, also known as formal verification.
Formal verification encompasses automatic verification of standard properties, such as using model checking, as well as more advanced verification by customizing security properties for specific projects and proving them.
As shown in the diagram below, Web 3 applications depend on all the component layers in their software stack. The business logic of smart contracts is written in high-level programming languages, compiled into bytecode, and executed by bytecode virtual machines on blockchain nodes. The nodes of the chain execute their specific code to calculate configurations like staking and consensus algorithms. Additionally, blockchain nodes operate on the physical cloud infrastructure, which includes system software such as operating systems, virtual machine monitors, and trusted execution environments.
When discussing the security of Web 3, the focus is often on smart contracts at the top of the software stack. The software components at lower levels are shared by multiple different Web 3 applications, resulting in more thorough testing and fewer potential errors.
However, this also makes them more important: a bug in the code of a blockchain node can jeopardize all applications on that blockchain, and an error in the system infrastructure can endanger the entire Web 3 world.
CertiK's work in machine-verified proof covers every aspect of the Web 3 software stack. For example:
We use symbolic model checking to automatically verify ERC-20 contracts and other Solidity contracts that implement standard interfaces
We have validated the smart contracts of DeFi applications similar to UniSwap. Formal verification is part of our audit of Move and Cardano contracts, and we have verified custom properties for some Solidity projects.
Our DeepSEA verification compiler aims to eliminate errors during the compilation process.
We have formally verified the standard banking module in the Cosmos SDK.
We have formally verified the main chain staking contract of TON Chain.
This blog post introduces our work at the bottom layer of the Web 3 software stack: in a recently published formal verification report, we applied advanced formal verification to the HyperEnclave trusted execution environment developed by the Ant Group Trusted Native Technology team.
HyperEnclave Trusted Execution Environment
The design purpose of a Trusted Execution Environment (TEE) is to protect applications from one of the most challenging types of attacks: those that can even control the computer's operating system.
Some of the most famous TEEs include Intel's SGX, Arm TrustZone, and AMD SEV. Their working principle is to allow the CPU to prove the presence of a specific secure application (enclave) through encrypted means and prevent other software from interfering with it.
TEE has already been integrated into many aspects of digital life. Disk encryption software like Apple FileVault and two-factor authentication applications like Google Authenticator store their keys in a TEE, even if someone steals and disassembles a laptop or smartphone, the keys remain protected.
At the same time, in Web 3, TEE is becoming increasingly important. Digital currency wallets also use TEE to securely store encryption keys. Distributed blockchain oracles can use TEE to increase the credibility of data. There are proposals to use TEE in "2-of-3 systems" to help recover from implementation errors in zero-knowledge proofs.
There are also some blockchain projects, such as LucidiTEE, SubstraTEE, Oasis Network, and AntChain, which propose using TEE to provide data privacy protection for users.
Currently, most TEEs are closed source and tied to specific hardware vendors. For example, to use Intel SGX, the application must run on Intel CPUs and go through Intel's approval and whitelist verification. However, hardware development itself is slow, so TEE has limited functionality and solving security issues requires firmware updates for CPUs. In contrast, HyperEnclave is mostly implemented using software and leverages two widely available hardware features.
First, the Trusted Platform Module (TPM) of the computer, typically used for UEFI secure boot, is used to verify if HyperEnclave and a set of specific enclaves are running. Secondly, HyperEnclave uses CPU virtualization extensions to protect the enclaves (typically used by virtual machine monitors such as VMware, VirtualBox, Hyper-V, KVM, etc.). For computer hardware, HyperEnclave looks like any other virtual machine monitor, but for enclaves, it provides a compatible API with SGX, making it easy for applications written for SGX to adapt and run on HyperEnclave seamlessly. Using standard virtualization techniques, it can easily support high-performance applications that interact closely with the operating system.
The most critical part in HyperEnclave is the monitor called RustMonitor, which protects the enclave from dangers posed by other enclaves and the operating system. The enclaves and the operating system run in a virtualization's "guest" mode, which means that every time they attempt to access memory, the memory address they're accessing is first translated through the page tables managed by RustMonitor. By placing the enclaves in different regions of the physical memory, RustMonitor ensures they can never read or overwrite the data owned by other enclaves. But this cannot be just a simple static separation: some memory addresses must be allowed to overlap for communication between enclaves and the operating system, and the address mappings are updated when handling page faults.
The developers of HyperEnclave have written a set of "invariants that must be upheld by page tables," which define the expected behavior of the memory address mapping table. For example, this includes properties such as "the address will only be mapped to a physical page in EPC if and only if the virtual address is within ELRANGE." For more detailed information, please refer to the formal verification report. Any errors that violate these conditions could invalidate the security guarantees of the entire HyperEnclave system.
The design of RustMonitor takes the following steps to ensure the trustworthiness of the code. First, it maintains a small scale – approximately 3000 lines of platform-independent code, plus a similar-sized x86 architecture-specific library code. Second, it is written in the Rust language - a memory-safe language that can eliminate most categories of errors. However, considering its importance, people still want to obtain higher security and resort to formal verification.
Formal verification of HyperEnclave's RustMonitor
The page table management code of RustMonitor is a good target for verification because it is both compact and crucial for security. Similar to the case of Web 3 smart contracts, it is feasible to invest effort in formal verification. In this project, CertiK starts with the invariants that must be upheld by the page tables and translates them from English into the Coq formal specification language. Then, we generate a machine-checkable proof to demonstrate that when the RustMonitor code modifies the tables, the resulting tables still satisfy all the invariants.
In fact, our development work goes further as we also want to ensure that the design of these invariants is correct and that our translation into the Coq language is correct. To do this, we further specify the information that client code should be able to observe in Coq and use invariants to prove there is no other information flow (the "non-interference theorem"). All of these proofs together provide a strong guarantee that the page table management is correct in both design and implementation.
However, proving the correctness of TEE monitoring programs is not a simple task. System-level programs like virtualization monitors and operating system kernels heavily rely on low-level code, involving pointer-based data structures, bypassing type abstractions, and highly optimized for performance. Even today, the verification of such programs remains a hot research topic published in top computer science journals, requiring tremendous effort to prove each line of code.
For example, the initial proof of seL^4 took 20 person-years, while Komodo required 2 person-years to verify the assembly code corresponding to approximately 650 lines of C code. The code in these projects was specifically written to simplify the verification, unlike HyperEnclave, which is already in production and adopts Rust's idiomatic style. Given the current level of technology, it is not economically feasible to verify all the code. Another issue is that compared to other programming languages, Rust's verification toolchain is not yet mature. Verification burden can be alleviated by writing manually crafted "model" code instead of actual code. An example of this approach is the Sanctum TEE, a verification research project. The downside of this approach is that the mismatch between the code and the abstract model may weaken any security or correctness properties of the model, or even invalidate them.
CertiK is uniquely positioned to address this problem. Our two founders, Professor Zhong Shao and Professor Ronghui Gu, are the inventors of the Concurrent Certified Abstraction Layer (CCAL) verification method. They have used this method to verify the world's first concurrent certified operating system kernel, CertiKOS, and have verified the KVM virtualization monitor seKVM and the ARM confidential computing architecture. The basic idea of CCAL is to divide all functions in the program into many "layers," write abstract models for each layer, and then prove that the actual code of the functions implements the abstract models, significantly reducing the risk of code-behavior mismatch with the abstract model. Compared to attempting to verify the entire program as a single whole, the layered approach is easier to handle code proof and concurrency issues. The work on seKVM and Arm CCA has received attention in terms of verifying industrial-grade system software projects, which previously were considered too large for formal verification.
HyperEnclave's formal verification team includes members who have previously participated in the verification of CertiKOS and seKVM. We attempt to strike a good balance between security assurance and resource investment by leveraging these experiences. To do so, we employ a flexible verification approach based on the CCAL specification: our framework supports verifying whether the code of verification functions complies with the model, but we choose to only verify a subset of functions (49 functions that directly manipulate memory page tables). For other functions, we assume that the manual Coq translation of the Rust code is correct and only prove the correctness of these Coq models. The level of abstraction of the accessed data structures in the source code determines whether each function needs to verify the compliance of its code with the model. When HyperEnclave uses advanced Rust data structures, we directly translate them into Coq. However, when it uses byte-based low-level page table formats, we spend more effort proving their equivalence to high-level functional models (see the complete formal verification report). As for RustMonitor, this means that we have proven the code of the "Memory" module that handles the representation of page tables, used an abstract model for the "Enclave" module that manages enclave states, and then combined all generated models to prove invariance theorems and top-level security theorems.
Another interesting part of this verification is how the code proof is carried out. The HyperEnclave code that handles page tables is low-level code that no existing verification tool can handle well. To address this, we developed a framework to verify Rust code by transforming it into an intermediate language called MIR (Mid-level Intermediate Representation) and used it to verify those crucial functions. Since MIR is a smaller language, we were able to write precise operational semantics for it and perform precise verification of the MIR code generated by the compiler. This gives our code proof a more solid foundation, rather than relying on any arbitrary translator.
In general, this is a massive task involving approximately 17,300 lines of manually proven scripts verified by the Coq proof assistant. There are also several thousand lines of formal specifications and a significant number of Coq files generated for the imported MIR code and layer structure. The main components of the proofs include the non-interference proofs (6600 lines), code proofs (4200 lines), page table operation proofs (4400 lines), and theorems related to the code proof framework. Ultimately, these proofs culminate in a set of theorems that state the data flow non-interference of the main system calls of HyperEnclave, namely privacy.
Summary
Trusted Execution Environment (TEE) is a fundamental technology for cloud computing and Web 3 applications, making its security crucial. In this project, CertiK applied advanced formal verification techniques to verify its most critical components, providing strong assurance that its code operates as expected and indeed complies with the desired security properties.
This formal verification work is only one part of ensuring privacy in computing security; it only covers the page table management portion of RustMonitor, which itself is just one component of the entire system. In the future, we will also conduct code audits, testing, and formal verification for other privacy computing components. By verifying the core parts, we establish a solid foundation for privacy cloud computing.
