Code Verification and Formal Methods

Recipe	Crates	Categories
Verify Your Rust Code with kani
Concurrent Code Verification
loom
shuttle

Rust formal methods⮳.

Formal methods are a collection of mathematically rigorous techniques used to specify, design, and verify software and hardware systems. These methods employ formal logic and mathematical proofs to ensure the correctness and reliability of systems, especially those that are safety-critical or security-critical.

Program verification is the process of formally proving the correctness of a program. This involves analyzing the code and ensuring that it meets specific properties, such as:

• Memory safety: The program does not have memory leaks, buffer overflows, or other memory-related errors.
• Thread safety: The program can be executed concurrently without causing data races or other concurrency issues.
• Functional correctness: The program produces the correct output for all valid inputs.
• Performance: The program meets specific performance requirements, such as execution time or memory usage.

There are two main approaches to Rust program verification:

1. Static verification: This involves analyzing the code at compile time to identify potential errors and prove the correctness of certain properties. Rust's type system and ownership model already provide a strong foundation for static verification. Additionally, tools like miri⮳ and kani⮳ can be used to perform more advanced static analysis.

2. Dynamic verification: This involves running the program with different inputs and checking its behavior against expected results. Techniques like fuzz testing can be used to identify potential issues.

Verify Your Rust Code with kani

kani⮳ is a Rust verifier / model checker. A model checker formally verifies that a system like a software program meets a given specification, using mathematical techniques (automated reasoning) to prove that a system satisfies a property for all possible states and behaviors. Model checkers explore the entire state space of the system, as opposed to approaches like fuzzing and property testing.

Model checking is a valuable technique for verifying the correctness of critical systems, such as safety-critical software and communication protocols. Kani is particularly useful for verifying unsafe code blocks. Some example properties you can prove with Kani include memory safety (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), the absence of some types of unexpected behavior (e.g., arithmetic overflows), in addition to user-specified assertions.

At present, Kani does not support verifying concurrent code.

Kani offers an easy installation option on three platforms:

• x86_64-unknown-linux-gnu (Most Linux distributions).
• x86_64-apple-darwin (Intel Mac OS).
• aarch64-apple-darwin (Apple Silicon Mac OS).

Python version 3.7 or newer and the package installer pip must be installed.

Install with:

cargo install --locked kani-verifier

Then download the Kani compiler and other necessary dependencies, and place them under ~/.kani/ by default:

cargo kani setup

Run kani:

cargo kani [OPTIONS]

Kani works like cargo test except that it will analyze "proof harnesses" instead of running test harnesses.

#![allow(unexpected_cfgs)]
#![allow(dead_code)]

// Define a very simple function to verify
fn add(a: i32, b: i32) -> i32 {
    // For testing purposes, we make it fail for only 1 in billions of possible
    // inputs
    if a == 42 {
        panic!("Oh no, a failing corner case!");
    }
    a + b // Note the possibility of overflow as well
}

// When Kani builds your code (using `cargo kani`), it
// - sets `cfg(kani)` for target crate compilation (including dependencies).
// - injects the kani crate.
// - sets `cfg(kani_host)` for host build targets, such as any build script and
//   procedural macro crates.
//
// The following Kani verification code is isolated in its own module and only
// compiled when Kani is in use.
#[cfg(kani)]
mod verification {

    use super::*;

    // Add a #[kani::proof] attributes to verification functions.
    // It can only be added to functions without parameters.
    //
    // Proof that adding zero to any number returns the same number
    #[kani::proof]
    fn add_zero_identity() {
        // We use `kani::any()` to represent all possible i32 values
        let a = kani::any();
        let result = add(a, 0);
        // State the property that should be true:
        kani::assert(result == a, "Adding zero should not change the value");
    }

    // Proof that addition is indeed commutative (a + b = b + a)
    #[kani::proof]
    fn addition_is_commutative() {
        let a = kani::any();
        let b = kani::any();

        let result1 = add(a, b);
        let result2 = add(b, a);

        kani::assert(result1 == result2, "Addition should be commutative");
    }

    // Proof that adding two non-negative numbers results in a non-negative
    // number
    #[kani::proof]
    fn add_is_non_negative() {
        let a = kani::any();
        // We set preconditions:
        // We assume that 'a' is non-negative
        kani::assume(a >= 0);

        let b = kani::any();
        // Same for 'b'
        kani::assume(b >= 0);

        let result = add(a, b);

        kani::assert(
            result >= 0,
            "Sum of two non-negative numbers should be non-negative",
        );
    }

    // Kani reports a number of failures, associated with overflows and
    // with the corner-case, which would be hard to detect via unit or property
    // testing alone, result in a failure:
    // Check 1: kani::estimate_size.assertion.1
    //          - Status: FAILURE
    //          - Description: "Oh no, a failing corner case!"
    //          - Location: crates/cats/development_tools/src/kani.rs:41:13 in
    //            function kani::estimate_size

    // By default, Kani only reports failures, not how the failure happened.
    // Kani offers an (experimental) concrete playback feature that provides
    // a concrete example of a value of x that triggers the failure.
}

fn main() {
    println!("2 + 3 = {}", add(2, 3));
}
// Examples adapted from the tutorial: https://model-checking.github.io/kani/tutorial-first-steps.html

Concurrent Code Verification

Loom attempts to check all possible interleavings, while Shuttle chooses interleavings randomly. The former is sound (like Kani), but the latter is more scalable to large problem spaces (like property testing).

shuttle

shuttle⮳ is a library for testing concurrent Rust code.

loom

loom⮳ allows permutation testing for concurrent code.

Other Tools

• MIRAI⮳.
• prusti⮳ is an automated program verifier for Rust, based on the Viper infrastructure. It leverages Rust's strong type guarantees to simplify the specification and verification of Rust programs.
• Creusot⮳ helps you prove your code is correct in an automated fashion.
• crucible (symbolic execution).

Related Topics

References

• Model_checking⮳.
• Kani Rust Verifier⮳.
• Announcing the Kani Rust Verifier Project⮳.
• Using the Kani Rust Verifier on a Firecracker Example⮳.
• Using the Kani Rust Verifier on a Rust Standard Library CVE⮳.