Rust是一种支持内存安全的新兴程序设计语言，可以在编译阶段排除内存安全隐患，其安全性保证的关键在于其引入了两种内存安全机制：Ownership类型系统和安全接口标准库。这两种机制作为Rust实现内存安全的基础，其编译实现的正确性是Rust内存安全的前提，需要经过严格的验证。因此本课题拟针对Rust内存安全机制的形式化验证展开研究，首先，面向Ownership类型系统，证明其理论模型与编译器中该类型系统实现的一致性。该研究涉及规约Ownership 理论模型，构建Ownership系统编译实现的形式语义。并基于该语义证明Ownership系统理论与实现的一致性。其次，针对安全接口标准库，分类和规约标准库需满足的内存安全属性，并对库中核心数据类型操作接口的安全性进行验证。本课题研究目标是构建可信的Rust开发环境，研究成果进一步可以为其他语言提供内存安全的技术支撑。

Rust is a new programming language designed for memory safety. It can detect memory unsafe risks during the compilation procedure. The key of the memory safety in Rust is that it introduces two mechanisms: the ownership type system and the standard library that supports safe memory operations. The two mechanisms are the bases of Rust’s memory safety and they should be rigorously verified. In this project, we aim at addressing the verification problems of the two mechanisms. Firstly, we focus on the verification of the consistency between the theoretical model and the implementation of the ownership type system. This involves building the theorem model of the ownership type system, constructing the formal semantics of the implementation of the ownership type system, and proving the consistency between them. Secondly, classifying and specifying memory safety properties and verifying the implementation of the safe interfaces of the standard library against these properties. The objective of this project is to build a verified Rust development environment. In addition, the project can provide a theoretical basis for the memory safety of other programming languages.