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

1、Rust Monitor!#$%!#$%&()*$+*仅限内部交流使用，如果需要公开，请联系文档作者目录1、Motivation2、Background3、Formal verification of Rust Monitor4、Proving Functional Correctness of Rust Code5.Summary*仅限内部交流使用，如果需要公开，请联系文档作者MotivationHypervisors and operating systems play a central role in system isolation,but their growing complex

2、ity poses security risks to vulnerabilities.To alleviate the problem,there is a growing trend of applying Rust,a memory-safe language,insystems software development.However,memory safety alone does not guarantee the security or functional correctness of the system.In this work we present the verific

3、ation 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 Abstr

4、action Layers(CCAL)to make the proof modular.We show that the safety guarantees provided by Rust could in return ease verification.*仅限内部交流使用，如果需要公开，请联系文档作者目录1、Motivation2、Background3、Formal verification of Rust Monitor4、Proving Functional Correctness of Rust Code5.Summary!#$%&()*+,-.!#$%&()*+,-.?At-

5、RestIn-TransitIn-Use机密计算(Confidential Computing)：The protection of data in use by performing computations in a hardware-based Trusted Execution Environment(TEE).可信执行环境(Trusted Execution Environment)：A TEE is an environment that enforces execution of only authorized code.Any data in the TEE cant be r

6、ead or tampered with by any code outside that environment.应用飞地(App Enclave)Application enclaves are isolated environments that protect specific code and data.威胁模型(Threat model)：aims at removing or reducing the ability for a cloud provider operator and other actors in the tenants domain to access cod