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.

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

该项目针对软件系统中最长久且最基本的内存安全问题进行研究，尽管内存安全已经在计算机科学领域被广泛关注长达几十年，但是仍然没有有效的解决方法。本课题基于最新的内存安全语言Rust，提出一种可以被重用的抽象内存管理模型。在抽象层面证明该内存管理模型可以保证程序运行过程中不会出现数据竞争，读未初始化变量和悬空指针的内存安全问题。在此基础之上，我们规约了Rust系统的ownership系统实现，并证明了该系统实现与抽象内存管理模型的一致性，从而为Rust语言开发环境提供了数学基础。最后我们将抽象的内存管理模型应用于C语言的内存安全保证并成功检测出C语言程序中的内存漏洞。该课题的研究通过数学方法证明了Rust系统的安全性，抽象精化出可以被重用的内存模型，并将其应用于C语言的验证。该研究将对安全关键软件的安全性提供更强的支撑。