Rust Monitor 形式化验证-刘双-V2

1 .Rust Monitor !"#$% !"#$ %&'()*$+ 

2 . 目录 1、Motivation 2、Background 3、Formal verification of Rust Monitor 4、Proving Functional Correctness of Rust Code 5. Summary * 仅限内部交流使用，如果需要公开，请联系文档作者 

3 . Motivation • Hypervisors and operating systems play a central role in system isolation, but their growing complexity poses security risks to vulnerabilities. • To alleviate the problem, there is a growing trend of applying Rust, a memory-safe language, in systems software development. However, memory safety alone does not guarantee the security or functional correctness of the system. • In this work we present the verification of Rust Monitor, a hypervisor-based TEE (trusted execution environment) which is implemented (mostly) in Rust. • For this purpose, we introduce MIRVerif, a framework for Rust verification at the Rust MIR (mid-level intermediate representation) level, and it is integrated with the Certified Concurrent Abstraction Layers(CCAL) to make the proof modular. • We show that the safety guarantees provided by Rust could in return ease verification. * 仅限内部交流使用，如果需要公开，请联系文档作者 

4 . 目录 1、Motivation 2、Background 3、Formal verification of Rust Monitor 4、Proving Functional Correctness of Rust Code 5. Summary * 仅限内部交流使用，如果需要公开，请联系文档作者 

5 .!"#$%&'()*+,-.? 机密计算(Confidential Computing)： The protection of data in use by performing computations in a hardware-based Trusted Execution Environment (TEE). At-Rest In-Transit 可信执行环境 (Trusted Execution Environment)： A TEE is an environment that enforces execution of only authorized code. Any data in the TEE can't be read or tampered with by any code outside that environment. 应用飞地(App Enclave) Application enclaves are isolated environments that protect specific code and data. In-Use 威胁模型(Threat model)： aims at removing or reducing the ability for a cloud provider Protect/encrypt data that in use, while operator and other actors in the tenant's domain to access code in RAM, and during computation and data while being executed. 

6 .!"#$%&&'()*+,- TEEs Company or Where isolation is Root Open Source Academia implemented? of trust TrustZone ARM Processor N/A No SGX Intel HW + XuCode CPU No SEV AMD HW + Co- CPU No processor TDX Intel HW + Firmware CPU Partial. CCA ARM HW + Firmware CPU Not Yet. !"#$%& '(()*+,-./01 • 234567897:;1<=>?@A=BCDEFG67DE@;HDEI • JKLM$%&NO1PJLQ$%&RSTU • 67VW1XY>Z[\] 

7 .Hyper Enclave Design Philosophy • 用高特权级软件(micro hypervisor)替代uCode/FW. • 用通用硬件功能替代特殊安全硬件. • 通过模拟TEE 指令集(ISA)兼容已有TEE生态. 机密运行时 机密容器 机密虚拟机 SGX 机密容器 TD 机密虚拟机 Occlum LibOS Occlum TEEOS Occlum LibOS Occlum TEEOS SGX ISA VM ISA SGX ISA TD ISA SEAM ISA 操作系统 Primary OS (Linux / KVM) Seam Mode Linux / KVM (Micro hypervisor) 虚拟化层 TEE硬件抽象层 Rust Monitor (Micro hypervisor) 硬件功能 虚拟化(VT-x/VT-d) 内存加密引擎(可选) 可信根 uCode Intel CPU 硬件平台 海光 Intel AMD 兆芯 飞腾 鲲鹏 TPM SGX HW 可信根 TDX HW * 仅限内部交流使用，如果需要公开，请联系文档作者 

8 . Rust Monitor • HyperEnclave consists of the following software components: a trusted software layer running in the host mode, e.g. VMX- root mode for X86 processors, referred to as the the Rust Monitor, is responsible for enforcing memory isolation. • Similar to Intel SGX, user applications are split into the untrusted part (App) and the trusted part (Enclave). • Rust Monitor creates a separate virtual machine (i.e the normal VM) which runs the untrusted OS referred to as the primary OS and the untrusted part of applications while the trusted part (i.e. the enclave) runs in another dedicated VM. • Rust Monitor is also responsible for the management of the enclave life cycle. Transitioning between the trusted and untrusted parts of applications is handled securely by Rust Monitor. • Rust Monitor switches the virtual CPU (vCPU) mode by restoring the vCPU state switching the GPT and NPT, and flushing the corresponding TLB entries. * 仅限内部交流使用，如果需要公开，请联系文档作者 

9 . Marshalling buffer • Unlike SGX, the enclave is not allowed to access the entire address of the application. To support passing data between the enclave and the application, a marshalling buffer is the application’s address space is allocated and shared with the enclave. • All data exchange between the enclave and application must be done through the marshalling buffer. • The mapping of the marshalling buffer are fixed during the entire enclave life cycle. * 仅限内部交流使用，如果需要公开，请联系文档作者 

10 . Memory Isolation • Rust Monitor enforces memory isolation with the virtualization hardware. • During system boot, a porting of physical memory is reserved, which is used by Rust Monitor and used as the enclave’s secure memory. The reserved memory is managed by Rust monitor, which other part of memory is managed and used by the Primary OS. • Rust Monitor creates separate nested page tables (NPTs) for each enclave and the normal VM hosting the Primary OS. These page tables must be set up correctly to enforce isolation. • The Enclave can only access its own protected memory and a share memory with the untrusted application. • The untrusted application and the primary OS are not allowed to access the physical memory reserved the Rust monitor and enclaves. • Furthermore, to prevent mapping attacks by the primary OS through manipulating the enclave’s page table, all enclave’s guest page table (GPTs) are managed by Rust Monitor, while the page tables in the normal MV are still managed by the primary OS. * 仅限内部交流使用，如果需要公开，请联系文档作者 

11 . 目录 1、Motivation 2、Background 3、Formal verification of Rust Monitor 4、Proving Functional Correctness of Rust Code 5. Summary * 仅限内部交流使用，如果需要公开，请联系文档作者 

12 . Formal verification of Rust Monitor • Rust Monitor must provide proper spatial isolation between enclaves and the untrusted OS, so that private data are not leaked or tampered with. • The Rust Monitor assures this by setting up the memory mappings so no virtual address in one guest is ever mapped to a physical address holding private data from another guest. • We first formalize the intended invariants about the mapping and prove that these indeed hold during execution. • We then use these invariants to prove that Rust Monitor satisfies a noninterference property. • Noninterference is formalized by modelling the system on which HyperEnclave is running as a set of principals, which in this case are Rust Monitor itself, the primary OS and possible malicious user programs, and the enclaves that may also be malicious to each other. • Noninterference ensures that whatever a principal does, it cannot affect other principal’s execution except on allowed communication channels, i.e. marshalling buffer. • Malicious principals may not exploit Rust Monitor to peek into or to overwrite others’ data. * 仅限内部交流使用，如果需要公开，请联系文档作者 

13 . Page table Invariants • The most subtle part of the Rust Monitor design the invariant that the page table mapping must satisfy. • These guard against two types of attack • First, if two different enclaves could address the same EPC page they could interfere with each other (alias attack). • if a virtual address which appears to not be part of the enclave were actually mapped to a physical EPC address, an enclave could be fooled into writing into each own EPC page when it believes it is accessing normal memory (remapping attack). * 仅限内部交流使用，如果需要公开，请联系文档作者 

14 . Page table Invariants • We formulate the following invariants to facilitate the verification of security properties: • ELRANGE(enclave linear range) memory isolation. • Given two virtual addresses va1 and va2 that are respectively in the ELRANGE (i.e. accessible virtual memory) of two different enclave e1 and e2, if they are translated to physical memory regions pm1 and pm2 by corresponding page tables, then pm1 and pm2 do not overlap • Marshalling buffer invariant. • Given two virtual addresses va1 and va2 that are translated to the same physical memory region by an enclave page table and the page table of the primary OS, then va1 and va2 are in the marshalling buffer. • NPT invariant. • The NPTs used by the enclaves and the primary OS are identity map. • EPCM(enclave page cache map) invariant. • All the ELRANGE mapping in the page tables of enclaves correspond to an entry in the EPCM, which is a list of mapping information. This rules out covert mappings. • Enclave invariants. Each enclave satisfies the following properties: • a virtual address in mapped to a physical page in the EPC if and only if the virtual address is in the ELRANGE; • The ELRANGE and the range of marshalling buffer are disjoint; • Theorem 1: if the system state s satisfies the invariant, and makes a transition to s’ via init(), and_page(), or enclave memory load/store, then s’ also satisfies the invariants. * 仅限内部交流使用，如果需要公开，请联系文档作者 

15 . System transitions • We need to define in Coq our model for how the system evolves. • This is done in terms of steps that the primary OS or enclave can do, either through local computation or by making a hypercall into Rust Monitor. • Each of the steps are defined as a Coq function which takes some abstraction system state as input and produces a new one. • The local computation of the primary OS and the enclaves are considered nondeterministic, that is, we do not model the code that is executing within the guest VM (either the normal VM or the enclave VM) at all. Instead we have two specification, mem_load and mem_store, which model what happens for an access to an arbitrary virtual address. • It is resolved using the current installed page table of either the primary OS or the enclaves, and if the page table succeeds, the physical memory and the current register state is updated. • The hypercalls are more interesting since they trap into the Rust Monitor for system transitions. • In HyperEnclave, this work is divided into several functions: init and add_page are called from the primary OS to create a new enclave, and enter and exit transfer control into and out of a particular enclave. • In our proofs we model the first 2 hypercalls, by inspecting the safe part of the Rust Code and updating the abstract data. The other 2 hypercalls (enter/exit ) do not manipulate the page table entries. * 仅限内部交流使用，如果需要公开，请联系文档作者 

16 . Noninterference • We use the invariants to prove an information flow noninterference theorem. We prove that no matter what an enclave or the primary OS does, it cannot affect other enclaves in any way, except by explicit communication using the marshalling buffers. • Noninterference says that, starting from any two state that A observes to be equivalent, any sequence of system transitions (hypercalls or memory operations) will take the system to a pair of state s1’ and s2’ which are still observably equivalent to A. • This holds even if initially other non-visible parts of the state can be different as other principals have their own data, and it holds even if other principals in the system simultaneously make their own transitions. • whatever other principals do they cannot affect A’s execution, which means they must not overwrite A’s memory. So integrity of A is ensured. • In a dual way, A may not peek into other principal's data, so confidentiality of them is ensured. • Because noninterference holds for every principal, consequently we have integrity and confidentiality for the whole system. * 仅限内部交流使用，如果需要公开，请联系文档作者 

17 . 目录 1、Motivation 2、Background 3、Formal verification of Rust Monitor 4、Proving Functional Correctness of Rust Code 5. Summary * 仅限内部交流使用，如果需要公开，请联系文档作者 

18 . Threat Model • The goal of HyperEnclave is to protect code and data of enclaves from the potentially malicious primary OS. • Specifically, Rust Monitor and the enclave code are Trusted, and we do not consider the buggy enclave voluntarily leaks data. • The primary OS is untrusted and could be under the control of an adversary, which can use • Arbitrary memory access or malicious DMA to peek into or overwrite enclave memory • Hypercalls to try to temper with the metadata within Rust Monitor • In both HyperEnclave and our verification, the Rust compiler is trusted. Also, we trust the verification tools, including Coq and the translator which converts MIR to Coq representations. • We consider the underlying hardware as trusted. Similar to many other TEEs, denial of service attack and side channel attacks are out of scope. * 仅限内部交流使用，如果需要公开，请联系文档作者 

19 . Methodology: CCAL • To verify Rust Monitor we use the Certified Concurrent Abstraction Layers (CCAL) approach, developed at Yale and Columbia for the CertiKOS and SeKVM projects. • Divide the set of functions into layers based on the call graph (calls go into a lower layer) • For each layers, define a type of abstract state, and manually write a set of functional models for the function in it • Prove high-level security property based on the model • Prove that the code of the function satisfy the function model (more abstract). Hypercall SGX ISA emulation Enclave Management Context Memory I/O vcpu page table arch/x86 Intel AMD * 仅限内部交流使用，如果需要公开，请联系文档作者 

20 . Rust Monitor Code Refactor • Refactor Rust mode to be more amenable to verification • Remove debug statement and assertions • Avoid lambda expression (which are clumsy when they are defunctionalized at the MIR level • Move loop-bodies to separate helper functions • Replace Enums with constants (which generate less code at MIR level) • In total, this rewrite 160 lines of code across 8 files. (as compared to the in-scope part of the code is 27 files and 3923 lines. ) * 仅限内部交流使用，如果需要公开，请联系文档作者 

21 . Model Rust Semantics (MIRVerif) • To verify Rust Monitor code, we developed a new framework for Rust verification MIRVerif which is composed of three pieces: • a formal semantics for the Rust language at the MIR level. • a tool to convert Rust programs to Coq representation and • an associated proof library. • MIR is a mid-level intermediate representation (IR) used in Rust compilation which bridges Rust source code and LLVM IR. • Since high-level Rust is a large and complex language and LLVM IR discards much important language-specific information like memory lifetimes. • we take advantage of Rust-specific language guarantees to provide assistance to our proof. * 仅限内部交流使用，如果需要公开，请联系文档作者 

22 . Functional Models: Whole Systems • To show isolation and non-interference we must define in Coq our model for how the system evolves. • Each of these are defined as a Coq function which takes some abstract system state (Rdata) and produces a new one. • Mem load/store by the guest • Hypercalls for einit(), add_page, eenter(), eexit() * 仅限内部交流使用，如果需要公开，请联系文档作者 

23 . Formalized statements of mapping invariants Informally: • Virtual address va1 and va2 in the ELRANGE of two different enclaves e1 and e2, map to non- overlapping regions. • If va1 and va2 are translated to the same physical memory region by an enclave page table and the page table of the host VM, then va1 and va2 are in marshalling buffer • The NPTs used by the enclaves and the host VM are identity map. • All page mapping for enclaves correspond to an entry in the EPCM • Each enclave satisfies the following properties: • a virtual address is mapped to a physical page in the EPC part if the only if the virtual address is in the ELRANGE; • the ELRANGE and the range of the marshalling buffer are disjoint; • no huge pages in the page table. * 仅限内部交流使用，如果需要公开，请联系文档作者 

24 . Formalized statement of memory isolation Prove page table invariants: no matter what an enclave or the linux guest does, it cannot affect the other enclaves in any way, except by explicit communication using the marshalling buffer. • Define observational equivalence • Each transition preserves observational equivalence • The statement of the theorem is standard (similar to SeKVM) • use a ‘data oracle’ to deal with declassification for the marshalling buffer. * 仅限内部交流使用，如果需要公开，请联系文档作者 

25 . Proofs: Invariant preservation and noninterference • There are 6 transitions in total: memory load/store, einit()/add_page(), and eenter()/exit(). • The enter()/exit() do not change the page tables, so we omit them. • For the other ones, we prove invariant preservation and observational equivalence preservation. • 6800 lines of Coq proofs. * 仅限内部交流使用，如果需要公开，请联系文档作者 

26 . Coq verification The Rust Monitor verification comprises ~17,300 lines of proof. The main components of the proofs are noninterference (6600 lines), code proofs (4200 lines) and code refinement proofs (4400 line), in addition to various code in the MIRVerif framework. For the code proofs using new MIR semantics, we verified the code of 49 functions from the Memory module. * 仅限内部交流使用，如果需要公开，请联系文档作者 

27 . Verification Result * 仅限内部交流使用，如果需要公开，请联系文档作者 

28 . 目录 1、Motivation 2、Background 3、Formal verification of Rust Monitor 4、Proving Functional Correctness of Rust Code 5. Summary * 仅限内部交流使用，如果需要公开，请联系文档作者 

29 . Summary • !"#$%%&'()*+,-./012&'3456712 操作系统(OS) &'893:;<=>#$%%12?@ AB+CDE=>FG HIJK %LMNOPQR 应用1 应用2 Enclave1 Enclave2 • STUVW+VXY5ZS[\]3B+^_`aSb124 cde 中国金融认证中心 • $%% ?@fg+hijH3klmn3opqr3stuv 模拟TEE指令集 CFCA • w'xyfg+z{|}$%%~•€•‚73ƒ„…†‡ˆ‰ 统一的TEE 硬件抽象层 RustTEE安全功能实现 Monitor • 12Vm+Š‹Œ•Ž••‘’mn•“”•–—˜ 授信 硬件安全原语 • ™š›œ•žŸ C¡!¢£¤¥ ¦I%§¨K ©$ª«¬¬ 虚拟化 内存加密 可信根 • |-®’¯°±²3•g`a³´¯°µ¶ 硬件 引擎(可选) (TPM)