Today we’re going to talk about how you can use fuzzing and verification in a unified framework, which is enabled by the integration of the Kani Rust Verifier in Bolero. Bolero is a property-testing framework that makes it easy for users to test a piece of Rust code with multiple fuzzing engines, and Kani is a verification tool that allows users to prove certain properties about their Rust code. By integrating Kani in Bolero, we enable users to apply multiple testing methods, namely fuzzing and proofs, to the same harness.

Why Bolero?

Suppose we want to test a function update_account_balance that takes the current balance and the amount we want to deposit or withdraw, and returns the new balance:

fn update_account_balance(current_balance: i32, amount: i32) -> i32 {
    // compute the new balance ...
}

A property-based test harness would look as follows:

#[test]
fn test_update_account_balance() {
    let current_balance = /* some value */;
    let amount = /* some value */;
    let new_balance = update_account_balance(current_balance, amount);
    assert!(balance_update_is_correct(current_balance, amount, new_balance));
}

where balance_update_is_correct checks that the transaction was carried out correctly, and may include other properties as well, for example that no overflow occurred, there was enough balance for a withdrawal, etc.

The question then is: how do we generate values for current_balance and amount for this property-based test harness? The answer depends on the testing technique we want to use. For example, if we were to use random testing, we would inject random values for current_balance and amount. If we do so using the rand crate, the harness would be as follows:

fn test_update_account_balance_random() {
    let current_balance = rand::random();
    let amount = rand::random();
    let result = update_account_balance(current_balance, amount);
    assert!(balance_update_is_correct(current_balance, amount, result));
}

We can then either repeatedly call the program to test it with different values, or call this function inside a loop.

This form of random testing typically has limited effectiveness. We can improve the effectiveness of our randomized testing with grey-box fuzzers, which use metrics such as code coverage to trigger unique behavior. There are a number of fuzzing engines for Rust, such as libFuzzer and AFL, that use different heuristics/metrics for exploring the input space.

To use libFuzzer, we would write a harness that looks as follows:

libfuzzer_sys::fuzz_target!(|(current_balance: i32, amount: i32)| {
    let result = update_account_balance(current_balance, amount);
    assert!(balance_update_is_correct(current_balance, amount, result));
}

When we run the fuzzer (e.g. using cargo fuzz), it will repeatedly call the body of the macro with values generated by libFuzzer.

If we were to use the AFL fuzzer instead, the harness would be in terms of AFL’s fuzz! macro:

afl::fuzz!(|(current_balance: i32, amount: i32)| {
    let result = update_account_balance(current_balance, amount);
    assert!(balance_update_is_correct(current_balance, amount, result));
}

What if we want to apply all the testing techniques described above to leverage their unique strengths? In this case, we end up having to write multiple harnesses in our code to test the same function. In addition, in order to run those harnesses, we would need a number of different commands, e.g. cargo test for running the random test, cargo fuzz to run the libfuzzer test, and cargo afl to run the AFL test! This quickly goes out of hand and becomes difficult to manage. This is where Bolero comes to the rescue!

The key idea of Bolero is to allow using multiple test engines on the same test harness. For example, to test function update_account_balance, one can write a Bolero harness that looks like the following:

#[test]
fn test_update_account_balance_bolero() {
    bolero::check!().with_type::<(i32, i32)>().cloned().for_each(|(current_balance, amount)| {
        let result = update_account_balance(current_balance, amount);
        assert!(balance_update_is_correct(current_balance, amount, result));
    });
}

Let’s break this up a bit to understand what it’s doing. First, the harness calls the check macro, which is Bolero’s main API for creating a test target. The test target can be configured to generate values of specific types via the with_type method. In our case, we configure it to generate a pair of i32’s. Next, cloned clones the generated values, and the for_each method calls the supplied closure for each generated value. In the case above, the closure passes the values on to update_account_balance and balance_update_is_correct.

So, what is the benefit of writing a Bolero harness? Bolero allows us to apply all the previous testing techniques on this same harness! To understand how, let’s look at Bolero’s main CLI command:

$ cargo bolero test --help
cargo-bolero-test 0.8.0
Run an engine for a target

USAGE:
    cargo-bolero test [FLAGS] [OPTIONS] <test>
<snip>
    -e, --engine <engine>   Run the test with a specific engine [default: libfuzzer]

We can find the list of engines that Bolero supports in its documentation: libfuzzer, afl, and honggfuzz. With this command, selecting a particular testing technique just becomes a matter of specifying the engine to Bolero’s cargo bolero test command! For example, we can run AFL on the harness above using:

cargo bolero test test_update_account_balance_bolero --engine afl

Bolero then takes care of all the details of calling that engine’s APIs under the hood to generate values, and executing that engine’s fuzzer! Neat! In addition, Bolero allows us to apply random testing on a harness. We can do so by executing the Bolero harness with cargo test.

Adding Proofs to the Mix with Kani!

Suppose we would like to verify the same function update_account_balance with Kani. In this case, we would write a proof harness similar to the ones we wrote above, but we would assign current_balance and amount to kani::any:

#[cfg(kani)]
#[kani::proof]
fn test_update_account_balance_kani() {
    let current_balance = kani::any();
    let amount = kani::any();
    let result = update_account_balance(current_balance, amount);
    assert!(balance_update_is_correct(current_balance, amount, result));
}

We can then run cargo kani to check the harness1. But wouldn’t it be nice if we can instead re-use the Bolero harness that we wrote above? This is where Kani’s integration in Bolero comes to play!

Running Kani on a Bolero harness is as simple as invoking cargo bolero test with --engine kani!

To see how this can be used, let’s look at an example of applying fuzzing and Kani through Bolero!

Example

Suppose we’d like to test the following function, nth_rev, which, given a slice and an index, returns the nth element from the end of that slice if the given index is in range, and otherwise None:

fn nth_rev(arr: &[i32], index: usize) -> Option<i32> {
    if index < arr.len() {
        let rev_index = arr.len() - index /* - 1 */;
        return Some(arr[rev_index]);
    }
    None
}

The function contains a classical off-by-one bug, as it misses subtracting one from the “reverse” index. Let’s write a Bolero harness to test it:

const N: usize = 5;

#[test]
#[cfg_attr(kani, kani::proof)]
fn check_rev() {
    bolero::check!()
        .with_type::<([i32; N], usize)>()
        .cloned()
        .for_each(|(arr, index)| {
            let x = nth_rev(&arr, index);
            if index < arr.len() {
                assert!(x.is_some());
            }
        });
}

Notice this line:

#[cfg_attr(kani, kani::proof)]

whose purpose is to treat this function as a proof harness when run with Kani, but treat it as an ordinary test otherwise.

The Bolero harness generates arrays of length N (set to 5 in this example), and an index, calls nth_rev, and checks that it returns Some if the index it received was less than the array length.

Let’s first test this with fuzzing using Bolero’s default engine (libfuzzer)2:

$ cargo bolero test check_rev
# snip ...
test failed; shrinking input...

======================== Test Failure ========================

Input: 
(
    [
        0,
        0,
        0,
        0,
        0,
    ],
    0,
)

Error: 
panicked at 'index out of bounds: the len is 5 but the index is 5', src/main.rs:6:21

The fuzzing engine found an input that causes the expected out-of-bounds error: an array of 5 zeros and an index of zero.

Let’s see if Kani finds the same issue:

$ cargo bolero test check_rev --engine kani
# snip ...
SUMMARY:
 ** 1 of 337 failed (1 unreachable)
Failed Checks: index out of bounds: the length is less than or equal to the given index
 File: "/home/ubuntu/examples/demos/rev-bolero/src/main.rs", line 6, in nth_rev

It did! Now, let’s fix the bug by updating the buggy line to:

        let rev_index = arr.len() - index - 1;

and re-run the fuzzer:

$ cargo bolero test check_rev
# snip ...
#3773   REDUCE cov: 135 ft: 138 corp: 18/282b lim: 52 exec/s: 0 rss: 43Mb L: 8/32 MS: 3 ChangeByte-ChangeBinInt-EraseBytes-
#262144 pulse  cov: 135 ft: 138 corp: 18/282b lim: 2620 exec/s: 131072 rss: 68Mb
#524288 pulse  cov: 135 ft: 138 corp: 18/282b lim: 4096 exec/s: 131072 rss: 93Mb
#1048576        pulse  cov: 135 ft: 138 corp: 18/282b lim: 4096 exec/s: 116508 rss: 142Mb

The fuzzer will run for a while without finding any failures. We can now run Kani to prove the assertion in our harness:

$ cargo bolero test check_rev --engine kani
# snip ...
SUMMARY:
 ** 0 of 338 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.90419155s

and voila! Kani managed to prove that none of the checks can fail for any values of the inputs.

If we have proof capability, do we still need fuzzing?

One question that might arise is: is there any point in using fuzzing alongside Kani? In other words, if we can prove a harness for all inputs with Kani, would we still want to use fuzzing? The answer is yes, because fuzzing and Kani provide complementary benefits.

Kani verifies a Rust program by symbolically analyzing its code. This allows Kani to make mathematical statements about the expected semantics of the Rust code being verified. Kani allows you to prove that, for all possible inputs, the code under verification follows its specification, assuming everything else functions correctly (e.g. the underlying hardware, the OS, etc.).

Fuzzing concretely executes the program under test. This gives you end-to-end confidence that for the set of inputs generated by the fuzzer, the code under verification follows its specification, under real-world conditions. Fuzzing and Kani fit together to give more assurance than either provides on its own.

How is Kani integrated in Bolero?

For those that are curious, let’s briefly discuss how the kani engine is implemented. At a high-level, Bolero redirects value generation to kani::any(), and calls cargo kani under the hood when cargo bolero test is invoked with the kani engine. Also, the for_each function only iterates once in the kani mode, since kani::any() covers all possible values of an input.

Some of the generation capabilities of Bolero require a little more than just calling kani::any(). For instance, Bolero supports generating values in a restricted range [min, max), e.g.

bolero::check!().with_generator(5..37).for_each( // snip... );

To support those in the Kani mode, Bolero leverages assumptions (kani::assume) under the hood:

let value = kani::any();
kani::assume((min..max).contains(&value));
value

To get started, check out the Bolero and Kani tutorials at the following links:

Footnotes

  1. Note that this harness cannot be compiled or executed with rustc as it involves some Kani attributes/functions that are only interpreted by cargo kani ↩

  2. Before running Bolero, make sure to include it as a dev dependency in the Cargo.toml:

    [dev-dependencies]
bolero = "0.8.0"

    ↩