一句话：为 Rust MIR 提出轻量形式语义与分层证明框架，验证 HyperEnclave 页表配置并证明安全飞地的空间隔离。
可信执行环境（TEE）是安全云计算的重要基石，其空间隔离依赖内存子系统的正确配置。即使 TEE 用内存安全语言 Rust 实现，页表等配置仍可能存在语义错误，从而破坏隔离。本文对软件 TEE HyperEnclave 的内存子系统进行形式验证，针对其早期原型证明安全飞地的页表配置满足空间隔离。为建模 Rust 代码，作者提出面向 Rust 中级中间表示（MIR）的轻量形式语义，并将其与分层证明框架结合，以提升复杂系统验证的可扩展性。该工作展示了在 Rust 实现的软件飞地 Hypervisor 中验证底层内存配置的可行路径。
As trusted execution environments (TEE) have become the corner stone for secure cloud computing, it is critical that they are reliable and enforce proper isolation, of which a key ingredient is spatial isolation. Many TEEs are implemented in software such as hypervisors for flexibility, and in a memory-safe language, namely Rust to alleviate potential memory bugs. Still, even if memory bugs are absent from the TEE, it may contain semantic errors such as mis-configurations in its memory subsystem which breaks spatial isolation. In this paper, we present the verification of the memory subsystem of a software TEE in Rust, namely HyperEnclave. We prove spatial isolation for the secure enclave though correct configuration of page tables for an early prototype of HyperEnclave. To formally model Rust code, we introduce a lightweight formal semantics for the Mid-level intermediate representation (MIR) of Rust. To make verification scalable for such a complex system, we incorporate the MIR semantics with a layered proof framework.
@inproceedings{DaiLSL0WJAESZNY24,
title = {Verifying Rust Implementation of Page Tables in a Software Enclave Hypervisor},
author = {Zhenyang Dai and Shuang Liu and Vilhelm Sjoberg and Xupeng Li and Yu Chen and Wenhao Wang and Yuekai Jia and Sean Noble Anderson and Laila Elbeheiry and Shubham Sondhi and Yu Zhang and Zhaozhong Ni and Shoumeng Yan and Ronghui Gu and Zhengyu He},
booktitle = {ASPLOS},
year = {2024},
doi = {10.1145/3620665.3640398}
}