Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor

Zhenyang Dai, Shuang Liu, Vilhelm Sjöberg, Xupeng Li, Yu Chen, Wenhao Wang and 9 others

Secure enclaves are supposed to seal off sensitive code from an untrusted operating system, and many are now built in software and written in Rust so the compiler rules out memory bugs — but Rust cannot rule out a subtler flaw, a page table set up wrong so the isolation silently leaks; this paper (Ant Group, Columbia, Tsinghua) machine-checks the paging code of HyperEnclave, a production Rust enclave hypervisor, by giving Rust's intermediate form a formal meaning and proving in Coq, in about three person-years, that no untrusted domain can read or corrupt enclave memory.

The argument in one glance

Problem

A memory-safe enclave can still leak, if its page tables are configured wrong

Trusted execution environments create an enclave — a sealed region where sensitive code and data run, protected from the privileged but untrusted operating system a cloud vendor controls. The guarantee that matters most is spatial isolation: the untrusted world must not be able to read or overwrite the enclave's private memory. Increasingly these enclaves are built not in hardware but as software hypervisors, for flexibility and auditability, and written in Rust, whose ownership and lifetime checks eliminate whole classes of memory bugs at compile time. But memory safety is not security. Rust can guarantee you never dereference a dangling pointer, yet it says nothing about whether the enclave's memory subsystem is configured correctly. The isolation is enforced by page tables — the data structures that decide which physical memory each domain can reach — and a single semantic error, a page table entry set to map the wrong region, silently breaks the isolation without any memory bug at all. These mistakes are subtle, hard to find by testing, and catastrophic.
What people did

Rely on Rust's safety, and on existing Rust verification tools

One line of defense is the language itself: write the enclave in Rust so the compiler rules out memory-corruption bugs. For deeper guarantees, a growing set of Rust verification tools — deductive verifiers, symbolic executors, model checkers — can prove properties of Rust code, checking that functions meet their specifications.
Why it fell short

Safety is not correctness, and existing tools do not scale to a whole system

Rust's guarantees stop at memory safety; they cannot express, let alone prove, that the paging subsystem actually isolates the enclave, because that is a semantic property of how the code configures hardware, not a property of pointer discipline. And the existing Rust verification tools are built mainly to handle the language soundly for individual functions, not to scale a proof across a real system. HyperEnclave, the production enclave hypervisor at issue, is a multi-component codebase — physical memory allocation, page-table-entry manipulation, address-space management — written in idiomatic Rust, using pointers pervasively, not code contorted to be easy to verify. A monolithic proof of such a system does not compose and does not scale, and rewriting it into a verification-friendly form would mean abandoning the very code that runs in production. What is missing is a way to prove a real, idiomatic-Rust system correct, modularly.
This paper's idea

Give Rust's intermediate form a formal meaning, and prove isolation in layers

This work verifies the paging subsystem of HyperEnclave by building MIRVerif. Rather than model the sprawling surface language, it gives a lightweight formal semantics to Rust's Mid-level intermediate representation — the simpler internal form the compiler already produces, which still preserves memory safety — and imports the real code into the Coq proof assistant through it. To make the proof scale, it is structured as fifteen layers from frame allocation up to address-space isolation, each layer seeing only the specification of the one below. Idiomatic pointers, which would break that layering, are modeled as opaque handles usable only in their owning layer, and Rust's no-aliasing guarantee licenses a clean object-view of memory. On this foundation the paper proves both functional correctness of the page-table code and a noninterference property: the untrusted world can neither read nor corrupt enclave memory.

Why this problem is worth solving

The security of the whole enclave reduces to one subsystem being configured exactly right, and that is precisely what a memory-safe language cannot guarantee.

A trusted execution environment protects an enclave by ensuring spatial isolation: no untrusted domain may peek into or overwrite the enclave’s private memory. In a hypervisor-based, software TEE this is achieved with nested paging. A guest operating system manages its own page tables, translating its virtual addresses to what it thinks are physical addresses — but the hypervisor interposes a second translation layer, the extended page tables, which it alone controls. Every access from a guest is re-translated through the hypervisor’s tables, so however a malicious operating system rewrites its own page tables, the hypervisor can guarantee that any address coming from an untrusted domain lands outside enclave memory. The entire isolation guarantee therefore rests on the hypervisor building and maintaining those extended page tables correctly. A single wrong entry, mapping an untrusted domain onto a page it should never see, breaks isolation completely — and it does so with no memory error, no crash, nothing that testing or a memory-safe language would catch. That is why the correctness of the paging subsystem is the crux of TEE security.

The obstacle to proving it is that the real system is written to run, not to be verified.

Rust is attractive for systems software because its ownership and lifetime rules eliminate memory-corruption bugs at compile time, and production enclave hypervisors are now written in it. But proving a semantic property like isolation requires formal verification on top of the language, and that runs into two walls. First, the system is large and multi-component, so any proof must compose: a monolithic argument over thousands of lines does not scale, and existing Rust verifiers are aimed at soundly handling the language for individual functions rather than at scaling proofs across a system. Second, the code is idiomatic — written the way a systems programmer would write it, with pervasive pointers, self-references, and pointers into page-table entries — not the pointer-free, array-indexed style that verification projects usually adopt to make proofs tractable. Rewriting the production code into a verification-friendly form would defeat the purpose, since the point is to verify what actually runs. So the challenge is to prove a realistic, idiomatic-Rust system correct and secure, modularly, while changing as little of the code as possible.

What people did before, and where it broke

Write the enclave in Rust for memory safety. Use the compiler’s ownership and lifetime checks to rule out memory-corruption bugs. Where it broke. Memory safety does not imply the memory subsystem is configured correctly; a semantically wrong page table breaks isolation with no memory bug for Rust to catch.
Apply existing Rust verification tools. Use deductive verifiers, symbolic executors, or model checkers to prove properties of Rust functions. Where it broke. They focus on handling the language soundly for individual functions, not on scaling a composable proof across a large, multi-component system.
Verify in a pointer-free, verification-friendly style. Follow projects like CertiKOS that were written for verification from the start, avoiding pointers by using array indices. Where it broke. HyperEnclave already exists and runs in production in idiomatic Rust; rewriting it into that style would abandon the code that actually ships.
Trust the hardware TEE instead. Rely on hardware and firmware enclaves rather than a software hypervisor. Where it broke. Hardware and firmware TEEs are difficult to evolve and audit, which is exactly why flexible software hypervisor TEEs are attractive and worth verifying.
The gap. No approach could prove spatial isolation for a real, industrially-deployed, idiomatic-Rust enclave hypervisor, modularly and without rewriting it away. Doing so by formalizing Rust’s intermediate representation and layering the proof is what this paper contributes.

How the verification works

From production Rust to a machine-checked isolation proof

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Verify the language’s intermediate form, and reason in layers so the proof scales. The core methodological choice is not to model Rust’s large surface language at all, but its Mid-level intermediate representation — the simpler internal form the compiler emits, which still carries memory safety — and to give that a formal operational semantics in Coq so the actual code can be imported and reasoned about. On top of this, MIRVerif borrows the layered-proof discipline of certified abstraction layers: the system is cut into fifteen layers, each proved correct against only the specification of the layer below, never its code, so complexity never accumulates into one monolithic argument and each layer can be checked in isolation. Building a modular verification framework that proves a low-level system correct piece by piece, against layer specifications rather than a whole-program model, is the same scaling discipline the work on lightweight modular verification of WebAssembly-to-native translation covered elsewhere on this site relies on, decomposing an otherwise intractable proof into local, composable obligations.

Formalize just enough of a memory-safe language, and let its guarantees pay for simpler proofs. The difficulty of verifying real Rust is that the semantics must be faithful yet workable, and the code uses pointers everywhere. The paper’s answer leans on Rust’s own guarantees. Because safe Rust forbids aliasing, memory can be modeled in an object-view — collections of non-overlapping objects located by symbolic paths rather than a flat array of bytes indexed by integers — which spares the proofs from ever reasoning about memory layout, pointer validity, or aliased updates. And the pointers that would otherwise leak data across proof layers are wrapped as opaque handles, usable only inside the layer that owns the underlying data, so encapsulation survives even though the code passes pointers freely. Writing a precise mechanized semantics for a low-level, memory-safety-oriented language so that rigorous proofs about real programs become possible is the same enabling move the work on formal mechanized semantics of CHERI-C covered elsewhere on this site makes, pinning down the exact meaning of a language’s memory model as the ground for everything built above it.

Prove not just correctness but isolation, as an information-flow property. Functional correctness — that the page-table code does what its specification says — is necessary but not the real prize; the prize is that the untrusted world learns and changes nothing about the enclave. So the paper proves noninterference: it defines what each principal is allowed to observe, and shows that two states differing only in an enclave’s secrets are indistinguishable to the untrusted operating system and stay indistinguishable as the system runs, which is confidentiality, while the dual statement gives integrity. Shared communication through marshalling buffers, which would appear to violate this, is handled by a data-oracle model that treats those bytes as declassified. Proving that a hardware-enforced boundary genuinely seals sensitive computation away from an untrusted host is the same assurance the work on a practical trusted execution environment covered elsewhere on this site aims to deliver, and this paper supplies the machine-checked evidence that the boundary actually holds.

Following an untrusted access through the proof

Why a malicious OS cannot reach enclave memory

A trace, following the paper's structure, of how the verified paging subsystem stops an untrusted access and how the proof establishes it.

Step 1 of 5

An untrusted domain attempts to reach enclave memory

The primary operating system, assumed to be adversarial, tries to read or overwrite an enclave's private memory — directly, or by rewriting its own guest page tables to point at the enclave's pages, the classic page-table attack.

The threat model grants the attacker arbitrary memory access and the ability to fire hypercall sequences to probe the monitor.

Why it works

Verifying the intermediate representation avoids the surface language’s complexity. Surface Rust is too intricate to model faithfully for proof → but its Mid-level intermediate representation is far simpler while still preserving memory safety → so a lightweight formal semantics of it is tractable yet still describes the real code the compiler produces.
Layering keeps a whole-system proof from collapsing under its own weight. A monolithic proof over a multi-component system does not scale → but dividing it into fifteen layers, each verified against only the specification below, bounds every step’s complexity → so the proof composes and stays manageable across the whole subsystem.
Rust’s no-aliasing guarantee licenses a simpler memory model. Pointer-heavy code normally forces proving validity, type-matching, and aliasing on every access → but because safe Rust forbids aliasing, memory can be modeled as non-overlapping objects located by paths → so the proofs never reason about byte layout or aliased updates.
Opaque handles preserve encapsulation despite pervasive pointers. Idiomatic pointers passed across layers would share memory and break the layered discipline → but modeling them as handles usable only in their owning layer keeps data encapsulated → so the code stays idiomatic and unmodified while the layering still holds.
Noninterference turns correctness into a real isolation guarantee. Functional correctness alone does not say the untrusted world is blind to the enclave → but proving observations depend only on permitted state, and are preserved under execution, establishes confidentiality and integrity together → so the proof certifies isolation, not merely that the code matches a spec.

What it costs (trade-offs and scope)

Only the memory subsystem is verified. The proof covers the paging code; other unverified parts, such as hypercall handling, are the main threat, and could in principle break the page-table invariants — mitigated by Rust’s memory safety, which encapsulates the tables, and by a manual audit of all 105 unsafe blocks (none of the raw-pointer-dereference blocks touch page-table memory), but not itself proved.
The trusted computing base is nontrivial. The result trusts the Rust compiler and its memory-safety guarantees, the Coq proof assistant, the tool that imports the intermediate representation and the layering scripts, and the hardware; an unsoundness in the lightweight intermediate-representation semantics, or a transcription error in a hand-written abstract model, would invalidate the proofs.
It required substantial expert effort. The verification took about three person-years and roughly fifteen thousand lines of Coq proof plus specifications, for around 2130 lines of Rust; this is described as a practical budget for an industrial system, but it is far from push-button and demands proof-engineering expertise.
Some parts are informal or unproven. The rely-guarantee argument tying the concurrency lemmas to full noninterference is left informal, and the soundness of lifting local variables out of memory is future work, assumed rather than proved.
The scope excludes important attack classes. Remote attestation, denial of service, side channels, and a buggy enclave voluntarily leaking its own data through the marshalling buffer are all out of scope, and the verified version is an early prototype, not identical to the later open-source release.

The evaluation

Assuring spatial isolation for a software enclave

Property	Rust memory safety alone	Function-level Rust verifiers	MIRVerif (this work)
What is guaranteed
Catches a mis-set page table
Scales to a whole subsystem
Handles idiomatic pointers	n/a
Applies to production code

From the paper. MIRVerif proves both functional correctness and a noninterference security property for the paging subsystem of HyperEnclave, an industrially deployed Rust enclave hypervisor, verifying about 2130 lines of idiomatic Rust with roughly 15,100 lines of Coq proof in about three person-years — a guarantee neither Rust's memory safety nor function-level verifiers provide.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The contribution is the first machine-checked proof that the memory subsystem of a real, industrially-deployed Rust enclave hypervisor actually enforces isolation. The insight is to verify Rust’s intermediate representation rather than its surface language, to structure the proof in fifteen layers so it scales, and to exploit Rust’s own no-aliasing guarantee for a clean object-view of memory with opaque handles for idiomatic pointers — all without rewriting the production code into a verification-friendly form. On this the paper proves both functional correctness of the page-table code and a noninterference property giving confidentiality and integrity. Read it within scope. Only the paging subsystem is verified, so unverified components (hypercall handling, the 105 unsafe blocks) are a residual threat, mitigated by Rust safety and a manual audit but not proved; the trusted base includes the Rust compiler, Coq, the import toolchain, and the lightweight intermediate-representation semantics, whose soundness the whole result rests on; it cost about three person-years of expert effort; parts of the concurrency argument and the local-variable lifting are informal or assumed; and attestation, denial of service, and side channels are out of scope. Within those bounds it is a landmark in verifying idiomatic systems Rust that actually ships.

Background

Why confidential computing needs proofs, not just safe languages

It helps to see why this matters now. So much computation has moved to the cloud that the operating system and hypervisor beneath an application are run by someone else, with more privilege than the application itself — and if that infrastructure is compromised, it can read or tamper with everything above it. Confidential computing answers this by carving out enclaves that even the privileged host cannot enter, and the mechanism is memory translation: a second, host-controlled layer of address translation that re-maps every access so untrusted code physically cannot name enclave memory. Interposing an extra translation stage on top of the one a guest already controls, precisely to constrain what memory a domain can reach, is the same architectural lever the work on parallel virtualized memory translation with nested paging covered elsewhere on this site studies, where that second layer is the price and the point of virtualization. But a mechanism is only as trustworthy as its implementation, and here the implementation is thousands of lines of pointer-heavy systems code whose one job is to never make a mistake. A memory-safe language removes one category of mistake; it cannot remove the category that matters most here, a table set up wrong. That is why isolation this important is worth not just writing carefully but proving — turning “we believe it isolates” into “we have machine-checked that it does.”

If you remember only three things

1. Trusted execution environments enforce spatial isolation — keeping an untrusted operating system out of an enclave's private memory — and many are now software hypervisors written in Rust for memory safety, but memory safety does not imply the memory subsystem is configured correctly: a single mis-set page table breaks isolation with no memory bug for Rust to catch, and existing Rust verifiers handle the language soundly for individual functions rather than scaling a composable proof across a real, idiomatic, multi-component system.
2. This work verifies the paging subsystem of HyperEnclave, a production Rust enclave hypervisor, by building MIRVerif: it gives a lightweight formal semantics to Rust's Mid-level intermediate representation (simpler than surface Rust but still memory-safe) and imports the real compiled code into Coq; it structures the proof as fifteen layers from frame allocation to address-space isolation, each verified against only the specification below; and it keeps the code idiomatic by modeling pervasive pointers as opaque handles usable only in their owning layer and by exploiting Rust's no-aliasing guarantee for an object-view of memory that avoids flat-byte-array reasoning.
3. On this foundation the paper proves both functional correctness of the page-table code and a noninterference property — the untrusted principal's observations depend only on state it is permitted to see and are preserved under execution, giving confidentiality and its dual integrity, with shared marshalling buffers handled by a data-oracle declassification model — machine-checking about 2130 lines of idiomatic Rust with roughly 15,100 lines of Coq proof in about three person-years; the scope is the memory subsystem only, the trusted base includes the Rust compiler, Coq, and the intermediate-representation semantics, and attestation, denial of service, and side channels are excluded.

Check yourself

Check your understanding

1. Why is writing a software enclave in Rust not enough to guarantee its isolation?
2. What are the two central techniques MIRVerif uses to make verifying idiomatic Rust tractable?
3. What security property does the paper prove, beyond functional correctness, and what does it mean?
4. What did the verification achieve, and what are its main limitations?

Sources

The paper is “Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor” by Zhenyang Dai, Shuang Liu, Vilhelm Sjoberg, Xupeng Li, Yu Chen, Wenhao Wang, Yuekai Jia, Sean Noble Anderson, Laila Elbeheiry, Shubham Sondhi, Yu Zhang, Zhaozhong Ni, Shoumeng Yan, Ronghui Gu, and Zhengyu He (Tsinghua University, Ant Group, CertiK, Columbia University, Institute of Information Engineering of the Chinese Academy of Sciences, Portland State University, Max Planck Institute for Software Systems, and Yale University), published at ASPLOS 2024 (Volume 2), DOI 10.1145/3620665.3640398.

This explainer is written from the full text of the authors’ version. Everything above comes from the paper’s own sections: the introduction on Rust for systems software and why memory safety does not imply functional correctness or security; trusted execution environments and how hypervisor-based software TEEs enforce spatial isolation through nested paging and extended page tables, with the correctness of the paging subsystem as the crux; the overview of HyperEnclave (its RustMonitor, normal VM and primary OS, enclaves, extended and guest page tables, marshalling buffers, and emulation of privileged SGX instructions) and the threat model (an untrusted primary OS with arbitrary memory access and hypercall sequences, trusting the Rust compiler, Coq, the import transpiler, and hardware, and excluding denial of service and side channels); the challenges of verifying idiomatic Rust and the solutions — the MIRVerif framework with a lightweight Coq semantics of the Mid-level intermediate representation (a small-step operational semantics with 28 expression types and 11 statements and terminators, imported via a modified compiler in the mirlightgen tool), the fifteen-layer proof structure following certified abstraction layers, the object-view memory model licensed by Rust’s no-aliasing guarantee, the opaque-handle treatment of cross-layer pointers, and the lifting of local variables; the functional-correctness and information-flow-security results, including the noninterference theorem, its confidentiality and integrity readings, the observation and indistinguishability formalization, the rely-guarantee lemmas (left informal for the full argument), and the data-oracle model for declassifying the marshalling buffer; and the evaluation reporting about 2130 lines of verified Rust, roughly 15,100 lines of Coq proof plus about 4,500 lines of specification, about three person-years of effort (20 percent framework, 30 percent invariants and noninterference, 10 percent page-table refinement, 40 percent code proofs, with 6,600 lines for the noninterference proofs), 49 of 77 memory-module functions verified, and the threats-to-validity discussion including the manual audit of 105 unsafe blocks.