The Rust community has launched a standard library verification competition aimed at fully utilizing the vast resources of the community to deeply validate the security of the Rust standard library.
In the world of the Rust programming language, the reliability and security of the standard library are crucial. Today, we will delve into the fascinating realm of verifying the Rust standard library and explore the highlights and challenges it presents.
This initiative primarily aims to provide automatic verification for the Rust standard library to ensure its safety. The goal is to verify whether the given implementation of the Rust standard library is secure.
Introduction
However, verifying the Rust standard library is a challenging task, with the main challenges being:
- Lack of specifications
- Absence of existing verification mechanisms in the Rust ecosystem
- Large scale of the verification problem
- Unknowns in scalable verification
Given the scale and scope of this work, the foundation believes it should be a community-led effort. To this end, they have launched a competition that includes a series of challenges, focusing on verifying memory safety and subsets of undefined behavior in the Rust standard library.
The main efforts are divided into the following areas:
- Contributing to the core mechanisms for verifying the Rust standard library
- Creating new technologies to perform scalable verification
- Applying these technologies to verify previously unverified parts of the standard library
Each challenge comes with financial rewards based on its specifications and is awarded upon successful completion.
Challenge Rules
Verification Target
The official target for the challenge is a forked branch verify-rust which contains a copy of the Rust standard library in its library/ folder.
Challenge Content
Each individual verification task will have a tracking issue where contributors can add comments and ask for clarifications. Challengers can find a list of open challenges here.
Solutions
Solutions to the challenges should be submitted as a single pull request (PR) to this repository. The solution should run as part of CI. For more details on the minimum requirements for each solution, see here.
In fact, this work is not formally affiliated with the Rust project or the Rust Foundation and has not been endorsed by them.
They have also published more detailed workflows, solution requirements, etc. For those interested, you can click here for more information.