Rust is a globally popular programming language. With the rapid growth of the Rust community, millions of developers are using it, and an increasing number of products and services are beginning to rely on Rust. This language is known for its excellent usability and robust compiler guarantees, making it the preferred choice for many developers.
Particularly when using the <span>unsafe</span> feature, the risks become especially pronounced. The Rust standard library makes extensive use of this feature, but this code has not yet undergone formal verification. Providing formal safety guarantees for these core libraries would greatly enhance the stability and reliability of the entire Rust ecosystem.
What Exactly is Unsafe in Rust?
The design goal of Rust is to create a programming language that is both safe and efficient. Its type system and ownership model provide very strong safety guarantees. However, in certain scenarios (such as pursuing extreme performance, directly manipulating hardware, or interfacing with legacy systems), this mechanism may seem overly strict. To address this, Rust provides the <span>unsafe</span> keyword, allowing developers to bypass some compiler checks and perform low-level operations.
While developers can use <span>unsafe</span> to write efficient and powerful code, it also means they must take on the responsibility for safety themselves. If mishandled, it can lead to undefined behavior (Undefined Behavior, UB). The Rust standard library (including core, alloc, and std, among other key components) heavily utilizes this <span>unsafe</span> code to implement efficient low-level logic. Although they provide safe interfaces externally, the internal implementations lack formal verification.
Statistics show that the current Rust standard library has about 35,000 functions, of which approximately 7,500 use <span>unsafe</span>, and another 3,000 belong to safe abstraction layers. The core library alone has over 21,000 functions, with more than 7,000 involving <span>unsafe</span> operations. In the past three years, the standard library has reported 57 safety issues, with 28% occurring in 2024, indicating that while the standard library is being updated more rapidly, potential vulnerabilities are also increasing.
Moreover, it is noteworthy that over 90% of Rust products and services rely on the standard library, and nearly all Rust applications call the core library. Therefore, ensuring the safety of these foundational libraries is crucial.
The Current Ecosystem of Verification Tools
In recent years, significant progress has been made in research on Rust safety, leading to the emergence of several tools for verifying Rust code. Here are some representative projects:
-
C2Rust: Translates Rust’s intermediate representation into formal verification languages such as Coq, Lean, F*, or HOL4, supporting interactive theorem proving.
-
Creusot: Uses a deductive verification approach suitable for safe code. It also introduces a specification language called Pearlite for describing function and loop contracts. However, it currently requires manual specification, which has a high maintenance cost.
-
Prusti: A hybrid verification tool based on separation logic, combining automatic verification of safe code and semi-automatic verification of unsafe code.
-
Kani: Verifies memory safety properties, partial undefined behavior, and user-specified assertions using bounded model checking techniques. It supports both
<span>unsafe</span>and safe code, but cannot guarantee correctness in unbounded scenarios. -
Miri: A Rust interpreter with built-in undefined behavior checks. Although it can only perform approximate verification, it works well under sufficient test coverage.
-
Viper: Uses SMT techniques to verify Rust code, supporting
<span>unsafe</span>in certain cases, such as raw pointers and RefCell usage.
Despite the strengths of these tools, comprehensive verification of the entire standard library still faces significant challenges:
- Lack of Unified Specifications: Many library functions do not have clearly defined behavioral specifications;
- Lack of Verification Mechanisms in the Ecosystem: The Rust language itself does not have built-in verification processes;
- Large Scale of Verification: The task of verifying tens of thousands of functions is extremely burdensome;
- Unknown Scalability: How to efficiently conduct large-scale verification remains an open question.
Collaborating to Promote Verification Work
In the face of these challenges, we have decided to adopt an open-source collaborative approach, encouraging developers worldwide to participate in this endeavor. We have broken down the entire verification task into multiple challenges, each with clear goals and success criteria. The current focus is on verifying memory safety and partial undefined behavior.
These challenges do not restrict the tools used, aiming to allow different verification solutions to integrate into the Rust core codebase. We are working with the Rust language team to promote the standardization of function and loop contracts and have established a centralized repository for storing solutions and verification results.
The challenges take various forms, including:
-
Writing specification contracts for certain parts of the standard library;
-
Completing specifications and verification for a specific module;
-
Developing new verification tools or improving existing ones to adapt to Rust.
For example, we have set up a challenge regarding the verification of the <span>String</span> type. The goal is to ensure that <span>std::string::String</span> does not trigger undefined behavior in all operations. Although most methods are safe, they often hide <span>unsafe</span> implementations behind them. For instance, the implementation of the <span>insert</span> method is as follows:
pub fn insert(&mut self, idx: usize, ch: char) {
assert!(self.is_char_boundary(idx));
let mut bits = [0; 4];
let bits = ch.encode_utf8(&mut bits).as_bytes();
unsafe {
self.insert_bytes(idx, bits);
}
}
This challenge clearly specifies the criteria for successful verification and requires that submitted solutions can be integrated into the CI pipeline.
「Click 👇 to Follow」
Like + Share + View to Quickly Improve Your Programming Skills👇
Reference link: https://aws.amazon.com/cn/blogs/opensource/verify-the-safety-of-the-rust-standard-library/