Rust is one of the fastest growing languages around the world. The Rust community has grown into millions of developers, with more products and servic

Verify the Safety of the Rust Standard Library

submited by
Style Pass
2024-11-21 07:30:05

Rust is one of the fastest growing languages around the world. The Rust community has grown into millions of developers, with more products and services relying on Rust. The ergonomics and strong compiler guarantees make Rust an ideal choice for developers. With this growth though, the Rust community has also recognized the unsafety of Rust (if used incorrectly). Specifically, when developers leave the walled garden of the compiler to implement their solutions, the Rust compiler places the onus of safety on the developer. The core libraries of Rust make use of this unsafe feature significantly, which is unverified. We believe that providing formal guarantees for these libraries will improve the Rust ecosystem for everyone.

In this post, we are pleased to announce a community wide effort to verify the Rust standard libraries for safety. The effort is structured as a challenge-based contest where each challenge describes a verification goal for a subset of the Rust libraries. Each challenge is created with a financial reward, which is awarded upon successful completion of the challenge. The Rust Foundation has reviewed our plans and agreed to host this endeavor.

Rust aims at being a safe and performant language. Its type system and ownership model provide strong safety guarantees; however, this model can be too restrictive (for efficiency, hardware access, legacy etc.). To overcome that, Rust provides a mechanism to perform unsafe operations that escape the guarantees of the compiler. Developers can create and use safe abstractions over unsafe code by delimiting the specific code that requires extra functionality. The Rust standard library, composed of a few crates such as core, alloc, and std, provides efficient implementations and safe abstractions for the most common general purpose programming data structures and operations. By doing so, they perform unsafe operations internally, which have not been formally verified or proven safe. The onus is placed on the developer to understand and evaluate the usage of unsafe operations. If done incorrectly, this can result in undefined behavior (UB).

Leave a Comment