Automatically Certifying Memory Safety of Safe Rust Programs in RustBelt
external page Rust is a modern system programming language with a strong focus on safety. One of the core benefits of using Rust instead of C and C++ is that the Rust compiler automatically ensures the absence of memory errors such as dangling references and double-free. As a result, Rust looks like an appealing language for writing safety-critical software such as controllers in plains, cars, and medical devices. However, the Rust compiler is complex and is likely to contain bugs that can undermine its strong guarantees.
One way of ensuring that the properties checked by the Rust compiler actually hold would be to verify the correctness of the compiler. Unfortunately, this would be a very expensive endeavour and thus unreachable in the near future. Therefore, we take a different approach here: we automatically generate a certificate for the program being compiled that shows that the checked properties actually hold. This certificate then can be checked by a much simpler tool significantly reducing the size of the trusted codebase. In our case, the certificate is proof that a given program is memory safe and the checker is a verifier that is capable of checking that proof.
external page RustBelt is a program logic designed for proving the memory safety of intricate Rust code. It is fully mechanized in the external page Coq proof assistant, which gives high confidence that it is sound. Therefore, it is a good fit for writing the certification proofs. In this project, we would aim to evaluate the feasibility of automatically generating RustBelt proofs from the information available in the compiler. For checking the proofs we would use the Viper verification infrastructure because of its automation capabilities.
Goals
The goal of this project is to develop a methodology that enables the automatic generation of a RustBelt memory-safety proof for an arbitrary Rust program that contains only safe Rust code.
The core milestones of this project are:
- Encode the RustBelt rules into the Viper intermediate verification language.
- Design a methodology for how to use the information available in the Rust compiler to automatically generate a RustBelt proof.
- Implement the methodology in a prototype tool.
- Evaluate the tool on a large number of Rust projects.
Useful Prerequisites
Knowing Rust is highly recommended. Experience with Viper or Coq is a plus.
Opportunities
The project offers the following opportunities:
- Make an important contribution to the Rust community.
- Gain experience with the Rust programming language and formal verification.