Last week, CertiK announced that it has completed advanced formal verification of HyperEnclave, an innovative open cross-platform trusted execution environment (TEE) developed by Ant Group’s trusted native technology team.
In order to fulfill its mission of protecting the Web3 world, CertiK employed a series of analysis methods during the audit 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 the standard protocol. One of the most powerful methods is machine-verified proof (i.e. formal verification).
Formal verification includes automatic verification of standard properties, such as using model checking, as well as more advanced verification, namely customizing security properties for specific projects and proving them.
- Understanding Curve Technology Details and Governance Concepts from Parameter A
- An Explanation of KINE’s Asset Strength and Technical Team
- LianGuaintera Capital’s Perspective on Cosmos Core Advantages, Innovation, and Important Ecosystem
As shown in the diagram below, Web3 applications rely on all layers of 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 compute configurations such as staking, as well as consensus algorithms. In addition, blockchain nodes run on physical cloud infrastructure, which includes system software such as operating systems, virtual machine monitors, and trusted execution environments.
When discussing the security of Web3, the focus is often on smart contracts at the top layer of the software stack. The software components at lower layers are shared by multiple different Web3 applications, so they undergo more testing and may have fewer errors.
However, at the same time, this also makes them more important: a bug in the code of a blockchain node can jeopardize all applications on that blockchain, and a bug in the system infrastructure can jeopardize the entire Web3 world.
CertiK’s work in machine-verified proof covers every aspect of the Web3 software stack. For example:
-
We use symbolic model checking to automatically verify ERC-20 contracts and Solidity contracts that implement other standard interfaces
-
We verify the smart contracts of DeFi applications like UniSwap, formal verification is part of our audit of Move and Cardano contracts, and we verify custom properties for some Solidity projects
-
Our DeepSEA verification compiler aims to eliminate errors in the compilation process
-
We formally verify the standard banking module of Cosmos SDK
-
We formally verify the main chain staking contract of TON Chain
This blog post introduces our work at the bottom layer of the Web3 software stack: in a recently released formal verification report, we applied advanced formal verification to the HyperEnclave trusted execution environment developed by Ant Group’s trusted native technology team.
HyperEnclave Trusted Execution Environment
The design purpose of a Trusted Execution Environment (TEE) is to protect applications from the most challenging types of attacks, including those that can even control the computer 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 through encryption that a specific secure application (enclave) has been loaded and prevent other software from interfering with it.
TEE has been integrated into many aspects of digital life. Disk encryption software like Apple’s FileVault and two-factor authentication applications like Google Authenticator store keys in the TEE, ensuring their protection even if someone steals and disassembles a laptop or mobile phone.
Meanwhile, TEE is becoming increasingly important in Web3. Digital currency wallets also use TEE to securely store encryption keys. Distributed blockchain oracles can use TEE to increase the trustworthiness of data. There are proposals to use TEE in “2-of-3 systems” to help recover from errors in zero-knowledge proofs.
There are also blockchain projects such as LucidiTEE, SubstraTEE, Oasis Network, and AntChain that propose using TEE to provide data privacy protection for users.
Currently, most TEEs are closed source and bound to specific hardware vendors. For example, to use Intel SGX, an application must run on an Intel CPU and go through Intel’s approval and whitelist verification. However, hardware development itself is slow, so TEEs have limited functionality, and addressing security issues requires firmware updates to the CPU. In contrast, HyperEnclave is mostly implemented in software, leveraging two widely available hardware features.
Firstly, the Trusted Platform Module (TPM) of the computer, typically used to implement UEFI secure boot, is used to verify if HyperEnclave and a specific set of secure enclaves are running. Secondly, HyperEnclave uses the CPU’s virtualization extensions to protect enclaves (typically used by virtual machine monitors like VMware, VirtualBox, Hyper-V, KVM, etc.). For computer hardware, HyperEnclave appears as any other virtual machine monitor, but for enclaves, it provides a compatible SGX API, making it easy for SGX-written applications to adapt and run on HyperEnclave. By using standard virtualization techniques, it can easily support high-performance applications that interact closely with the operating system.
The most critical part of HyperEnclave is the monitor called RustMonitor, which protects enclaves from dangers coming from other enclaves and the operating system. Enclaves and the operating system execute in a virtualized “guest” mode, which means that every time they try to access memory, the accessed memory address is first translated through the page table managed by RustMonitor. By placing enclaves in different regions of physical memory, RustMonitor ensures that they can never read or overwrite data owned by other enclaves. But this cannot be a simple static separation: some memory addresses must be allowed to overlap so that enclaves can communicate with the operating system, and the address mapping is updated when handling page faults.
The developers of HyperEnclave have written a set of “invariants that page tables must comply with,” which define how the memory address mapping table is expected to work. For example, this includes properties such as “an address is mapped to a physical page in the EPC only if and only if the virtual address is in the ELRANGE.” For more details, please refer to the formal verification report. Any error that violates these conditions could invalidate the security guarantee 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 – about 3000 lines of platform-independent code, plus a similar size of x86 architecture-specific library code. Second, it is written in the Rust language – a memory-safe language that eliminates most error categories. However, considering its importance, people still want higher security and seek formal verification.
Formal verification of RustMonitor for HyperEnclave
RustMonitor’s page table management code is a good verification target because it is both small and critical to security. Similar to Web3 smart contracts, it is feasible to invest effort in formal verification. In this project, CertiK starts with the invariants that the page table must adhere to and translates them from English to the Coq formal specification language. Then, we produce a machine-checked proof to demonstrate that when RustMonitor code modifies the table, the resulting table still satisfies all the invariants.
In fact, our development work goes further because we also want to ensure that the design of these invariants is correct and that our translation of them 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 the invariants to prove that there is no other information flow (“unrelated theorem”). All these proofs together provide a strong guarantee that page table management is correct in both design and implementation.
However, proving the correctness of the TEE monitoring program is not a simple task. System-level programs like hypervisors and operating system kernels heavily use low-level code that involves pointer-based data structures, type abstractions, and highly optimized performance. To this day, the verification of such programs remains a hot research problem worthy of publication in top computer science journals, requiring significant effort to prove each line of code.
For example, the initial proof of seL4 took 20 person-years, while Komodo spent 2 person-years to verify the assembly code corresponding to about 650 lines of C code. The code in these projects was specially rewritten to simplify verification, which is very different from HyperEnclave – the latter is already in production and adopts Rust’s idiomatic style. It is not economically feasible to verify all the code based on the current level of technology. Another issue is that Rust’s verification toolchain is not as mature as that of other programming languages. The burden of verification can be alleviated by writing manual “model” code instead of actual code. An example is Sanctum TEE, a verification research project. The drawback of this approach is that the mismatch between code and abstract model may weaken any security or correctness properties about the model, or even invalidate them.
CertiK has unique advantages in addressing this issue. Our two founders, Professor Zhong Shao and Professor Ronghui Gu, are the inventors of the Concurrent Certified Abstraction Layer (CCAL) verification method. They used this method to verify the world’s first concurrent certified operating system kernel, CertiKOS, and verified the KVM hypervisor seKVM and the ARM confidential computing architecture. The basic idea of CCAL is to divide all functions in the program into many “layers,” write their abstract models for each layer, and then prove that the actual code implementation of the functions realizes the abstract models, significantly reducing the risk of code and abstract model behavioral mismatches. Compared to attempting to verify the entire program as a single whole, the layered approach is easier to handle code proofs and concurrency issues. Previous work on seKVM and Arm CCA has received attention in terms of verifying industrial-grade system software projects, which were previously too large in scale for formal verification.
The HyperEnclave formal verification team includes personnel 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 use an elastic 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 handle memory page tables). For other functions, we assume that the manual Coq translation of Rust code is correct and only prove the functional 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 its code against the model. When HyperEnclave uses advanced Rust data structures, we directly convert them to Coq, but when it uses byte-based low-level page table formats, we invest more effort in proving their equivalence to the high-level functional model (see the complete formal verification report for details). As for RustMonitor, this means that we have proven the code of the “Memory” module that handles page table representations, used an abstract model for the “Enclave” module that manages enclave states, and then combined all the generated models to prove the invariance theorem and top-level security theorem.
Another interesting part of this verification is how to prove the code. The HyperEnclave code that handles page tables is low-level code that no existing verification tool can handle well. To address this, we have developed a framework to verify Rust code by transforming it into the intermediate language MIR (Mid-level Intermediate Representation), and used it to verify those critical functions. Since MIR is a smaller language, we are able to write precise operational semantics for it and perform precise verification of the MIR code generated by the compiler, which gives our code proofs a more solid foundation instead of relying on an arbitrary translator.
In summary, this is a massive work involving approximately 17,300 lines of manually proven scripts that have passed the Coq proof assistant’s verification. There are also several thousand lines of formal specifications, as well as a large number of Coq files generated for the imported MIR code and layer structure. The main components of the proofs include the proof of non-interference (6,600 lines), code proofs (4,200 lines), page table operation functionality proofs (4,400 lines), and theorems related to the code proof framework. In the end, these proofs are collected into a set of theorems that state the data flow non-interference, or privacy, of the main system calls of HyperEnclave.
Summary
Trusted Execution Environments (TEEs) are a fundamental technology for cloud computing and Web3 applications, making their security crucial. In this project, CertiK applied advanced formal verification techniques to verify its most important components, providing strong guarantees that ensure its code runs as expected and indeed complies with the expected security properties.
This formal verification work is just one part of ensuring the security of privacy computation; it only covers the page table management part of RustMonitor, which in itself is just one component of the entire system. In the future, we will also conduct code audits, testing, and formal verification of other privacy computation components. By verifying the most critical parts, we lay a solid foundation for privacy cloud computing.
Like what you're reading? Subscribe to our top stories.
We will continue to update Gambling Chain; if you have any questions or suggestions, please contact us!
