Annotating the Rust Standard Library with Specifications for Use in a Rust Verifier
external page Rust is a modern system programming language with a strong focus on speed, safety, and concurrency. Its strong type system prevents most memory-related errors such as dangling references without the need to have a garbage collector. In our group we are developing Prusti, a verifier for Rust programs, that leverages the strong type system to significantly reduce the effort required for proving properties that go beyond simple memory safety. For example, with Prusti one can specify and get automatically checked by the tool that the result of a sorting function is actually sorted. Internally, Prusti translates Rust programs to the Viper intermediate verification language.
When verifying real-world codebases, a large part of the code relies on correct implementations of the standard library or third-party libraries in general. Although Prusti has a mechanism for adding specifications to external methods and types, the users still need to manually include these specifications in their projects. This is both impractical and error-prone. The goal of this project is to develop a library of specifications that can be easily imported and used with Prusti.
Goals
- Implement a mechanism for exporting and importing specifications across Rust crates (libraries). This mechanism should allow for different specifications across different versions of external library.
- Compile specifications for the most commonly used standard library methods.
- Deploy the standard library of specifications as a crate in Rust's crates.io package repository.
Prerequisites
Since the Prusti verifier, the internals of the Rust compiler, and the Rust standard library are all written in Rust, previous knowledge of Rust is strongly preferred to make progress in reasonable time. Experience with Viper or program verification in general is helpful.
Opportunities
The project offers the following opportunities:
- Make an important contribution to the Rust community.
- Gain experience with the Rust programming language.