Rust model checking #

Model checking means verifying that a program works correctly for all possible inputs.

Instead of testing with a single value (like with unit testing) or with a set of values (like with property testing), we check all possible values—and hope that smart algorithms will make it possible to finish testing in a reasonable time.

Prusti #

Prusti is based on Viper, a framework for building verification tools. It uses symbolic execution and the Z3 theorem prover.

It is an academic project that seems to be stale. However, it can be used to experiment with this type of testing. For production uses consider other tools like Kani or Verus.

Installation #

The developers recommend using the Visual Studio Code extension. Command-line tools can be downloaded from the Prusti GitHub’s releases page.

Usage #

You can simply run Prusti on your code and it will look for the following:

Absence of reachable panics
Absence of reachable, failing assertions
Absence of integer overflows

Prusti detects all functions in a project (even unreachable ones) and checks them “independently.” It simply assumes that function arguments can take any value—that they are bounded only by their types.

Please note that Prusti does not check testing code.

To restrict values, and to define more code properties for verification, you have to create specifications for functions.

Function specifications #

The main power of Prusti lies in its ability to specify and validate functions’ contracts (or specifications). A function’s specification consists of preconditions and postconditions.

Preconditions
- These conditions are checked before calls.
- Prusti verifies that all calls to the function are done with arguments meeting the preconditions.
- Preconditions limit the set of possible values for postcondition checks.
Postconditions
- These conditions are checked after function returns.
- Prusti verifies that postconditions are met at all exit points of the function.

In the example below, conditions are implemented with Rust attributes: requires (preconditions) and ensures (postconditions). Prusti will check if all calls to prusti_check pass the argument that is less than or equal to 20. Then it will check if possible return values from the prusti_check function are below 10, assuming the input is less than or equal to 20.

use prusti_contracts::*;
fn main() {
    prusti_check(20);
    prusti_check(11);
}

#[requires(x <= 20)]
#[ensures(x < 10)]
fn prusti_check(x: u32) -> u32 {
    if x >= 10 {
        return x / 100;
    }
    return x;
}

If values violating conditions are found, Prusti returns an error and can produce an example set of values that demonstrate the problem.

Prusti does not support loops automatically. You have to specify body_invariants to enable code verification.

Kani #

Kani is a frontend for CBMC (Bounded Model Checker for C and C++).

Installation #

You can simply use Cargo to install it.

cargo install --locked kani-verifier cargo kani setup

Basic usage #

Using Kani is similar to writing normal unit tests. You first write a test and then run this command:

cargo kani

However, instead of using concrete values, use kani::any() to create a “symbolic” (or unbounded or nondeterministic) variable. Such variables can take any value (of their type).

Running the test, Kani will verify the absence of the following conditions for all possible values of the symbolic variables:

Failing assertions
Panics
Memory safety issues
Integer overflows

If the code to test is too complex, Kani may take a long time to finish or may not even terminate at all. To overcome this, you can use three features:

kani::assume: For restricting (bounding) symbolic values. It is a bit similar to Prusti’s preconditions.
kani::unwind: For controlling bounds for loops. Kani will assume that loops can loop only the configured number of times. The greater the number, the slower the execution. But if the number is configured to be too small, Kani will fail too early. This is the mechanism that overcomes Prusti’s limitation with the body_invariant statement.
kani::Arbitrary: For defining per-type limitations for symbolic values

Let’s see an example:

pub struct Book {
    title: String,
    pages: u16
}

fn read_book(r: Book) -> u16 {
    return if r.title == "The Black Book" {
        0
    } else {
        let mut letters = 0;
        for page in 0..r.pages {
            if page == 13 {
                panic!("Bad luck");
            }
            letters += page;
        }
        letters
    }
}

#[cfg(kani)]
mod verification {
    use crate::{Book, read_book};

    impl kani::Arbitrary for Book {
        fn any() -> Self {
            let titles = vec!["The Black Book", "Lord of the ToB",
                              "The White Book"];
            let title_id: usize = kani::any();
            kani::assume(title_id < titles.len());
            Book { title: titles[title_id].to_string(), pages: kani::any() }
        }
    }

    #[kani::proof]
    #[kani::unwind(18)]
    fn verify_book() {
        let book: Book = kani::any();
        kani::assume(book.pages < 4096);
        let y = read_book(book);
        assert!(y < 100);
    }
}

Here we have a simple structure and a function that panics for some inputs.

We define a new verification module under the #cfg(kani) attribute. This lets us disable Kani-specific code when not needed. Then, we implement the kani::Arbitrary trait to tell Kani how to generate symbolic Books: by limiting the set of titles to three possible values and using unbounded numbers in the pages field.

Then, we use the #[kani::proof] attribute and write a test similar to normal unit tests, with three main differences:

Generating a symbolic book variable (using our kani::Arbitrary implementation)
Restricting book.pages to be less than 4096
Limiting the number of loops to 20 with #[kani::unwind(20)]

The Kani documentation recommends setting the #[kani::unwind(X)] attribute experimentally:

Start with a number that is slightly larger than the maximum of the expected numbers of all loops’ repetitions.
If Kani takes too much time to finish, lower the unwind number.
If Kani errors out with FAILURE: unwinding assertion loop X, increase the unwind number.

If Kani finds a FAILURE, then we can generate example values that will trigger the failure with one of two methods:

Generating a normal unit test with cargo kani --concrete-playback print -Z concrete-playback
Generating an HTML report with cargo kani --visualize --enable-unstable

Kani does not scale well for the following:
Strings with unbounded content (i.e., long strings with arbitrary data)
Structures of symbolic sizes that involve heap allocations.