Verify Rust Standard Library Effort

The Verify Rust Standard Library effort is an ongoing investment that targets the verification of the Rust standard library. The goal of this is to provide automated verification that can be used to verify that a given Rust standard library implementation is safe.

Efforts are largely classified in the following areas:

1. Contributing to the core mechanism of verifying the rust standard library
2. Creating new techniques to perform scalable verification
3. Apply techniques to verify previously unverified parts of the standard library.

We encourage everyone to watch this repository to be notified of any changes.

General Rules

Terms / Concepts

Verification Target: Our repository is a fork of the original Rust repository, and we kept a copy of the Rust standard library inside the library/ folder that shall be used as the verification target for all our challenges. We will periodically update the library/ folder to track newer versions of the official Rust standard library. NOTE: This work is not officially affiliated, or endorsed by the Rust project or Rust Foundation. Challenges: Each individual verification effort will have a tracking issue where contributors can add comments and ask clarification questions. You can find the list of open challenges here.

Solutions: Solutions to a problem should be submitted as a single Pull Request (PR) to this repository. The solution should run as part of the CI. See more details about minimum requirements for each solution.

Basic Workflow

1. A verification effort will be published in the repository with appropriate details, and a tracking issue labeled with “Challenge” will be opened, so it can be used for clarifications and questions, as well as to track the status of the challenge.

2. Participants should create a fork of the repository where they will implement their proposed solution.

3. Once they submit their solution for analysis, participants should create a PR against the repository for analysis. Please make sure your solution meets the minimum requirements described here.

4. Each contribution will be reviewed on a first come, first served basis. Acceptance will be based on a review by a committee.

5. Once approved by the review committee, the change will be merged into the repository.

Solution Requirements

A proposed solution to a verification problem will only be reviewed if all the minimum requirements below are met:

• Each contribution or attempt should be submitted via a pull request to be analyzed by reviewers.
• By submitting the solution, participants confirm that they can use, modify, copy, and redistribute their contribution, under the terms of their choice.
• The contribution must be automated and should be checked and pass as part of the PR checks.
• All tools used by the solution must be in the list of accepted tools, and previously integrated in the repository. If that is not the case, please submit a separate tool application first.
• There is no restriction on the number of contributors for a solution. Make sure you have the rights to submit your solution and that all contributors are properly mentioned.
• The solution cannot impact the runtime logic of the standard library unless the change is proposed and incorporated into the Rust standard library.

Any exception to these requirements will only be considered if it is specified as part of the acceptance criteria of the challenged being solved.

Call for Challenges

The goal of the effort is to enable the verification of the entire Rust standard library. The type of obstacles users face may depend on which part of the standard library you would like to verify. Thus, our challenges are developed with the target of verifying a specific section of the standard library or strengthening existing verification.

Everyone is welcome to submit new challenge proposals for review by our committee. Follow the following steps to create a new proposal:

1. Create a tracking issue using the Issue template Challenge Proposal for your challenge.
2. In your fork of this repository do the following:
   1. Copy the template file (book/src/challenge_template.md) to book/src/challenges/<ID_NUMBER>-<challenge-name>.md.
   2. Fill in the details according to the template instructions.
   3. Add a link to the new challenge inside book/src/SUMMARY.md
   4. Submit a pull request.
3. Address any feedback in the pull request.
4. If approved, we will publish your challenge and add the “Challenge” label to the tracking issue.

Tool Applications

Solutions must be automated using one of the tools previously approved and listed here:

• Any new tool that participants want to enable will require an application using the Issue template Tool application.
• The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
• A new tool application should clearly specify the differences to existing techniques and provide sufficient background of why this is needed.
• The tool application should also include mechanisms to audit its implementation and correctness.
• Once the tool is approved, the participant needs to create a PR that creates a new action that runs the std library verification using the new tool, as well as an entry to the “Approved Tools” section of this book.
• Once the PR is merged, the tool is considered integrated.
• The repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository. I.e., the action may no longer pass after an update. This will not impact the approval status of the tool, however, new solutions that want to employ the tool may need to ensure the action is passing first.

Challenge XXXX1: Challenge Title

• Status: One of the following: [Open | Resolved | Expired]
• Solution: Option field to point to the PR that solved this challenge.
• Tracking Issue: Link to issue
• Start date: YY/MM/DD
• End date: YY/MM/DD

Goal

Describe the goal of this challenge with 1-2 sentences.

Motivation

Explain why this is a challenge that should be prioritized. Consider using a motivating example.

Description

Describe the challenge in more details.

Assumptions

Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".

Success Criteria

Here are some examples of possible criteria:

All the following unsafe functions must be annotated with safety contracts and the contracts have been verified:

At least N of the following usages were proven safe:

All proofs must automatically ensure the absence of the following undefined behaviors ref:

List of UBs

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.

🚧 Under Construction 🚧

This section is still under construction. Please check it back again soon and we’ll have more details for you.

Verification Tools

The verification tool ecosystem for Rust is rapidly growing, and we welcome the usage of different tools to solve our challenges. In this chapter, you can find a list of tools that have already been approved for new solutions, what is their CI current status, as well as more details on how to use them.

If the tool you would like to add a new tool to the list of tool applications, please see the Tool Application section.

Approved tools:

Tool	CI Status
Kani Rust Verifier

Kani Rust Verifier

The Kani Rust Verifier is a bit-precise model checker for Rust. Kani is designed to prove safety properties in your code as well as the absence of some forms of undefined behavior. It uses model checking under the hood to ensure that Rust programs adhere to user specified properties.

You can find more information about how to install in this section of the Kani book.

Usage

Consider a Rust function that takes an integer and returns its absolute value and a Kani proof that invokes the function that you want to verify

fn abs_diff(a: i32, b: i32) -> i32 {
    if a > b {
        a - b
    } else {
        b - a
    }
}

#[cfg(kani)]
#[kani::proof]
fn harness() {
    let a = kani::any::<i32>();
    let b = kani::any::<i32>();
    let result = abs_diff(a, b);
    kani::assert(result >= 0, "Result should always be more than 0");}

Running the command cargo kani in your cargo crate will give the result

RESULTS:
Check 1: abs_diff.assertion.1
         - Status: FAILURE
         - Description: "attempt to subtract with overflow"
         - Location: src/main.rs:5:9 in function abs_diff

... Other properties that might have failed or succeeded.

Summary:
Verification failed for - harness
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

Using Kani to verify the Rust Standard Library

To aid the Rust Standard Library verification effort, Kani provides a sub-command out of the box to help you get started.

Step 1

Modify your local copy of the Rust Standard Library by writing proofs for the functions/methods that you want to verify.

For example, insert this short blob into your copy of the library. This blob imports the building-block APIs such as assert, assume, proof and function-contracts such as proof_for_contract and fake_function.

#[cfg(kani)]
kani_core::kani_lib!(core);

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
pub mod verify {
    use crate::kani;

    #[kani::proof]
    pub fn harness() {
        kani::assert(true, "yay");
    }

    #[kani::proof_for_contract(trivial_function)]
    fn dummy_proof() {
        trivial_function(true);
    }

    #[kani::requires(x == true)]
    fn trivial_function(x: bool) -> bool {
        x
    }
}

Step 2

Run the following command in your local terminal:

kani verify-std -Z unstable-options "path/to/library" --target-dir "/path/to/target" -Z function-contracts -Z stubbing.

The command kani verify-std is a sub-command of the kani. This specific sub-command is used to verify the Rust Standard Library with the following arguments.

• "path/to/library": This argument specifies the path to the modified Rust Standard Library that was prepared earlier in the script.
• --target-dir "path/to/target": This optional argument sets the target directory where Kani will store its output and intermediate files.

Apart from these, you can use your regular kani-args such as -Z function-contracts and -Z stubbing depending on your verification needs. For more details on Kani's features, refer to the features section in the Kani Book

Step 3

After running the command, you can expect an output that looks like this:

SUMMARY:
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.017101772s

Complete - 2 successfully verified harnesses, 0 failures, 2 total.

More details

You can find more information about how to install and how you can customize your use of Kani in the Kani book.

This chapter contains all existing challenges, including the ones that have already been solved or expired.

For the most up-to-date information on a challenge status, please check their tracking issue linked in the challenge description.

If you would like to submit a new challenge, please see "Call for Challenges" section.

Challenge 1: Verify core transmuting methods

• Status: Open
• Tracking Issue: Link to issue
• Start date: 2024-06-12
• End date: 2024-12-10

Goal

Confirm the soundness of value transmutations performed by libcore, including those transmutations exposed as public methods provided by libcore. A value-to-value transmutation is sound if:

1. the source value is a bit-valid instance of the destination type;
2. violations of library safety invariants (e.g., invariants on a field's value) of the destination type are not violated by subsequent use of the transmuted value.

If the context of the transmute is safe, these conditions should be proven with local reasoning. If the context of the transmute is unsafe, they may be discharged with a safety obligation on the caller.

To keep the goal somewhat manageable, it excludes some classes of code (e.g., UTF8-validation, async tasks, and others); see the assumptions listed below for the full list of excluded categories.

Details

Motivating Example

There are several calls to unsafe methods using transmute within the code of safe methods exported by libcore itself, so having clear and verifiable safety contracts is critical for verifying the safety of the safe methods that invoke them.

For example, std::slice::align_to (which unsafely converts any slice &[T] into a tuple (&[T], &[U], &[T]) composed of a prefix, a maximal sequence of values of type U, and a suffix) just says for its safety that “all the usual caveats pertaining to transmute::<T, U> also apply here”, which might be an under specification. For more details, see the documentation for transmute.

Breaking-down the verification

We lay out the verification challenge from the bottom up. Starting with the core implementation of transmute moving up to all unsafe and safe APIs that rely on it.

Part I - The Two Intrinsics

The public unsafe intrinsic transmute<T, U> takes a value of type T and reinterprets it to have type U, with the sole (statically-enforced) restriction being that the types T and U must have the same size. The unstable intrinsic transmute_unchecked<T, U> is similar, except that it removes the static size restriction, treating violations of it as undefined behavior.

What is the right way to encode the preconditions of the two transmutation intrinsics?

If one is solely concerned about safety: The Rustonomicon lists several ways that transmutation can yield undefined behavior. Encoding a safety contract for transmute that captures all the relevant criteria laid out in the documentation is crucial.

If one is concerned about proving functional correctness, then reasoning about transmutation will require reasoning about the byte representation of values to justify that the reinterpretation of the value’s bytes for satisfying the pending proof obligation associated with the output value.

Part II - unsafe APIs with Validity Constraints

There are unsafe methods (which are defined by libcore and reexported by libstd) that have the effect of a transmutation between a (sequence of) T and a (sequence of) U. Come up with an appropriate safety contract for each of them.

Part III - unsafe APIs with Richer Constraints

Similar to part 2, there are also unsafe methods, but now the safety condition is more complicated, such as “is valid ascii character” or "is valid unicode scalar value."

Part IV - safe APIs

These are safe APIs that call into the unsafe API's from parts 1 through 3 above. Now our final goal is to prove that they actually are safe, despite calling transmute or transmute-related methods in their implementations.

Assumptions

For this challenge, the following assumptions are acceptable:

We are not attempting to validate all details of the memory model for this challenge; for example, you do not need to worry about whether we are using the Stacked Borrows or Tree Borrows aliasing models. Likewise, you do not need to validate the provenance-related API in std::ptr.

You are allowed, but not required, to leverage the unstable Transmutability trait under development as part of your solution. This is a libstd-internal feature for auditing whether a given transmutation is safe. (It seems like something tools should try to leverage in some way; but it is also experimental.) Note that if you need to add new impls of Transmutability, then those new impl’s need to be accepted by (and landed in) the upstream Rust project before your solution can be considered completed. See also https://github.com/rust-lang/rust/issues/99571

You do not need to verify the correctness of the transmute calls in the unit tests embedded in libcore, though it would be great to do so!

To keep the goal somewhat manageable, we are omitting the following classes of code from the acceptance criteria for this challenge:

• utf8-validation (such as str::from_utf8_unchecked)
• the provenance-related API in std::ptr (such as addr, or without_provenance)
• the num methods (from modules like core::num::f64, core::num::i32, etc)
• pointer-metadata and vtable APIs (from modules like core::ptr::metadata)
• async rust runtime/task API (from core::task)
• core-internal specialization methods (such as traits like RangeIteratorImpl with methods prefixed with "spec_")
• core-internal __iterator_get_unchecked calls
• value output formatting machinery (from std::fmt::rt) You do not need to verify those (potentially indirect) uses of transmute, unless you need to establish the safety/correctness of some of those methods in order to verify some other type in this list. (That is, you cannot assume them to be safe nor correct in your verification of other methods listed here.) We expect to issue future challenges tailored to each of the categories of transmutation uses listed above.

Success Criteria

A new entry to the specification book is created explaining the relevant patterns for verifying code that calls transmute.

At least 35 of the following 47 intrinsics and functions (i.e. approximately 75%) have been annotated with contracts, and, for non-intrinsics, had their bodies verified.

For the safe functions, you do not need to provide a full-functional correctness specification; it will suffice to add pre- and post-conditions (i.e. assumptions and assertions) around the relevant part of the code that calls the transmutation-related unsafe function or intrinsic.

• All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed below

Appendix A: The list construction

The list of methods and intrinsics was gathered by surveying the call-graph (solely within the libcore source) of function bodies that could eventually invoke transmute or transmute_unchecked. For each caller: if the caller was itself unsafe, then its callers were then surveyed; if the caller was not unsafe, then it was treated as an end point for the survey.

As mentioned in the assumptions, some (large) classes of methods were omitted from the challenge, either because 1. they encompassed a large API surface (e.g. core::num) that deserved separate treatment, 2. they had an enormous number of callers that would deserve separate treatment (e.g. core::str::from_utf8_unchecked), or 3. they interact with aspects of the Rust memory model that still need to be better understood by reasoning tools (e.g. the provenance APIs).

You can see the call graph produced by the survey here.

Challenge 2: Verify the memory safery of core intrinsics using raw pointers

• Status: Open
• Tracking Issue: Link to issue
• Start date: 24/06/12
• End date: 24/12/10

Goal

Annotate Rust core::intrinsics functions that manipulate raw pointers with their safety contract. Verify their usage in the standard library is in fact safe.

Success Criteria

1. All the following intrinsic functions must be annotated with safety contracts.
2. Any fallback intrinsic implementation must be verified.
3. For intrinsics modeled in the tool of choice, explain how their implementation matches the intrinsics definition. This can either be done in the PR description or as an entry to the contest book as part of the “Tools” chapter.
4. For each function, contestants must state clearly the list of assumptions for each proof, how the proofs can be audited, and the list of (implicit and explicit) properties that are guaranteed.
5. The verification of each intrinsic should ensure all the documented safety conditions are met, and that meeting them is enough to guarantee safe usage.

Intrinsic functions to be annotated with safety contracts

All the following usages of intrinsics were proven safe:

Annotate and verify all the functions that below that expose intrinsics with safety contracts

List of UBs

All proofs must automatically ensure the absence of the following undefined behaviors ref:

• Invoking undefined behavior via compiler intrinsics.
• Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
• Reading from uninitialized memory except for padding or unions.
• Mutating immutable bytes.
• Producing an invalid value

Note: All solutions to verification challenges need to satisfy the criteria established in the challenge book in addition to the ones listed above.