Amazon and the Rust Foundation have introduced an initiative aimed at enhancing the security of the Rust programming language's standard library. The goal is to assess the reliability and safety of functions that use the 'unsafe' keyword, which permits operations that can be unsafe with memory, such as dereferencing pointers, modifying static variables, and accessing external libraries in C/C++. It is noted that the current Rust standard library contains about 35,000 functions, 7,500 of which include code blocks executed in an 'unsafe' context. Over the past three years, 57 correctness issues have been identified in the library, 20 of which were marked as vulnerabilities.
The library verification work is organized in the form of a competition, where participants are presented with various tasks related to performing specific checks to confirm safe memory handling with Rust libraries or developing tools for automating such checks. Successful completion of the verification goal (providing formal proof of reliability) involves a reward. A repository has been created for conducting experiments and publishing work results, acting as a branch from the official Rust repository.
Currently, 13 tasks have been proposed. For instance, one task involves verifying the safety of working with raw pointers in functions from the module core::ptr and providing formal proof of the correctness of pointer operations. Existing tools such as Aeneas, Kani, Gillian, Verus, and Creusot can be used for verification, or new tools can be suggested. Examples of completed tasks.
Source: opennet.ru
