Making Even Safe Rust a Little Safer: Model Checking Safe and Unsafe Code

In my last article, I explored tools that can help ensure unsafe code in Rust is free from security vulnerabilities caused by undefined behaviours. These tools included sanitizers for memory and concurrency errors, and Miri, an interpreter focused on detecting undefined behaviours. I also demonstrated how sanitizers can be used to find errors in unsafe code in libraries written in C or C++ and called from Rust through FFI.

The software I work on is used for operating critical infrastructure. In addition to being secure, it needs to be reliable. Software errors in cyber-physical systems can impact operations in inconvenient, expensive, or unsafe ways, to people, property, or equipment. Unlike other programming languages with similar performance characteristics, like C or C++, Rust has run-time checks that prevent unsafe code from being executed. For example, unless overridden using unsafe code, Rust will panic if an array is indexed out of bounds, even in a release build. However, run-time panics can result in unpredictable behaviour. In cyber-physical systems, deterministic error handling is preferable, or even required by regulation.^[1] In this article, I will explore tools for checking Rust code, even safe code, to eliminate errors.

Property Testing

Property testing repeatedly exercises code with arbitrary inputs. Proptest is a property testing framework for Rust that is easy to use. Returning to the index out-of-bounds error from the previous article, here is a property test for it:

fn bad_address(i: i32) -> i32 {
    let xs: [i32; 4] = [0, 1, 2, 3];
    xs[i as usize]
}

#[cfg(test)]
mod property_tests {
    use crate::bad_address;
    use proptest::proptest;

    proptest! {
         #[test]
         fn test_bad_address(i: i32) {
             bad_address(i);
         }
    }
}

Running the test with cargo test results in a test failure with the following output:

running 1 test
test property_tests::test_bad_address ... FAILED

failures:

---- property_tests::test_bad_address stdout ----
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 733042689
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 366521344
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 183260672
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 91630336
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 45815168
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 22907584
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 11453792
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 5726896
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 2863448
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 1431724
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 715862
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 357931
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 178965
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 89482
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 44741
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 22370
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 11185
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 5592
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 2796
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 1398
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 699
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 349
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 174
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 87
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 43
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 21
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 10
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 5
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 4
thread 'property_tests::test_bad_address' panicked at src/main.rs:3:5:
index out of bounds: the len is 4 but the index is 4
thread 'property_tests::test_bad_address' panicked at src/main.rs:16:5:
Test failed: index out of bounds: the len is 4 but the index is 4.
minimal failing input: i = 4
        successes: 0
        local rejects: 0
        global rejects: 0



failures:
    property_tests::test_bad_address

test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s

The output demonstrates how Proptest works. It chooses a random integer for the index and runs the test. The first index it tries is 733042689. The test panics because the index is out of bounds, but Proptest doesn’t stop there, it iterates by narrowing the input to try and find a boundary case where the test starts to fail. By default, Proptest will iterate 256 times before giving up.^[2] It eventually finds the boundary case of the index 4 being out of bounds for an array of size 4.

The Limitations of Property Testing

To understand the limitations or property testing, consider the following test that takes the absolute value of an integer:^[3]

use proptest::prelude::*;

proptest! {
    #[test]
    fn i64_abs_is_never_negative(a: i64) {
        // This actually fails if a == i64::MIN, but randomly picking one
        // specific value out of 2⁶⁴ is overwhelmingly unlikely.
        assert!(a.abs() >= 0);
    }
}

The chances of Proptest catching the error in this code is vanishingly small. The test will only fail on one boundary condition, the absolute value of i64::MIN, which will panic. The vast majority of the time, Proptest will perform 256 iterations of random input and report the test has passed:

running 1 test
test i64_abs_is_never_negative ... ok

test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.01s

The Limitations of Exhaustive Testing

Consider the following code:^[4]

fn panic_or_zero(a: i64, b: i64, c: i64, d: i64) -> i64 {
    if a < b && b < c && d > 100 && (a >= c || d < 28) {
        panic!();
    }
    0
}

Can this function panic or will it always return zero? It is hard to know. However, this is an easy function to exhaustively test for all possible inputs:

#[test]
fn test_panic_or_zero() {
    for a in i64::MIN..i64::MAX {
        for b in i64::MIN..i64::MAX {
            for c in i64::MIN..i64::MAX {
                for d in i64::MIN..i64::MAX {
                    assert_eq!(panic_or_zero(a, b, c, d), 0);
                }
            }
        }
    }
}

The only problem is, this test requires 2²⁵⁶ iterations, so even if each iteration takes only a nanosecond, this test will take 10⁶⁰ years to complete.^[5] In many situations, exhaustive testing is impractical.

Model Checking With Kani

Kani is a model checker for Rust that verifies code through deductive mathematical proofs. Kani proofs are similar to tests but they use partially-constrained inputs, rather than concrete values, along with deterministic, symbolic reasoning of the Rust Mid-Level IR (MIR) to evaluate the code under all possible inputs that satisfy the constraints.^[6] Kani proofs are written in Rust and reside alongside source code, just like unit tests. Kani proofs are exceptionally valuable for finding errors in the examples above.

Here is a Kani proof for the function that takes the absolute value of an integer:

#[kani::proof]
fn kani_i64_abs_is_never_negative() {
    let a: i64 = kani::any();
    assert!(a.abs() >= 0);
}

Run Kani as follows:

cargo kani

Kani quickly identifies the integer overflow:

RESULTS:
Check 1: core::num::::abs.assertion.1
         - Status: FAILURE
         - Description: "attempt to negate with overflow"
         - Location: ../../../runner/.rustup/toolchains/nightly-2024-10-03-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/int_macros.rs:3414:17 in function core::num::::abs

Check 2: kani_i64_abs_is_never_negative.assertion.1
         - Status: SUCCESS
         - Description: "assertion failed: a.abs() >= 0"
         - Location: src/main.rs:20:5 in function kani_i64_abs_is_never_negative


SUMMARY:
 ** 1 of 2 failed
Failed Checks: attempt to negate with overflow
 File: "/Users/runner/.rustup/toolchains/nightly-2024-10-03-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/num/int_macros.rs", line 3414, in core::num::::abs

VERIFICATION:- FAILED
Verification Time: 0.28206664s

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

By default, Kani reports failures, not how the failures happened, but it has an experimental concrete-playback feature that will construct a test case to demonstrates the failure. To run Kani with concrete-playback:

cargo kani -Z concrete-playback --concrete-playback inplace

Kani will insert a test case into the source file that exercises the error case:

/// Test generated for harness `kani_i64_abs_is_never_negative`
///
/// Check for `assertion`: "attempt to negate with overflow"

#[test]
fn kani_concrete_playback_kani_i64_abs_is_never_negative_15620477642559825021() {
    let concrete_vals: Vec<Vec<u8>> = vec![
        // -9223372036854775808
        vec![0, 0, 0, 0, 0, 0, 0, 128],
    ];
    kani::concrete_playback_run(concrete_vals, kani_i64_abs_is_never_negative);
}

Here is a Kani proof for the function that will either panic or return zero:

#[kani::proof]
fn kani_panic_or_zero() {
    let a: i64 = kani::any();
    let b: i64 = kani::any();
    let c: i64 = kani::any();
    let d: i64 = kani::any();
    let result = panic_or_zero(a, b, c, d);
    assert_eq!(result, 0);
}

Kani runs in milliseconds and proves this function can never panic:

RESULTS:
Check 1: kani_panic_or_zero.assertion.1
         - Status: SUCCESS
         - Description: "assertion failed: result == 0"
         - Location: src/main.rs:53:5 in function kani_panic_or_zero

Check 2: panic_or_zero.assertion.1
         - Status: SUCCESS
         - Description: "explicit panic"
         - Location: src/main.rs:24:9 in function panic_or_zero


SUMMARY:
 ** 0 of 2 failed

VERIFICATION:- SUCCESSFUL
Verification Time: 0.035682622s

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

Kani for Unsafe Rust

Unsafe code results in undefined behaviours which makes model checking challenging, but Kani can detect certain classes of errors in unsafe code that are unchecked by the compiler.^[7]

Returning to the out-of-bounds error in unsafe code from the previous article, Kani can be used to model-check this code:

fn bad_address(index: i32) -> i32 {
    let xs = [0, 1, 2, 3];
    unsafe { *xs.as_ptr().offset(index as isize) }
}

#[kani::proof]
fn kani_bad_address() {
    let index: i32 = kani::any();
    bad_address(index);
}

Kani identifies the error dereferencing the pointer outside the bounds of the array:

RESULTS:
Check 1: std::ptr::const_ptr::::offset.arithmetic_overflow.1
         - Status: SUCCESS
         - Description: "offset: attempt to compute number in bytes which would overflow"
         - Location: ../../../../runner/.rustup/toolchains/nightly-2024-10-03-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:399:18 in function std::ptr::const_ptr::::offset

Check 2: std::ptr::const_ptr::::offset.arithmetic_overflow.2
         - Status: SUCCESS
         - Description: "attempt to compute offset which would overflow"
         - Location: ../../../../runner/.rustup/toolchains/nightly-2024-10-03-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:399:18 in function std::ptr::const_ptr::::offset

Check 3: bad_address.assertion.1
         - Status: SUCCESS
         - Description: "misaligned pointer dereference: address must be a multiple of its type's alignment"
         - Location: src/main.rs:26:14 in function bad_address

Check 4: bad_address.pointer_dereference.1
         - Status: SUCCESS
         - Description: "dereference failure: pointer NULL"
         - Location: src/main.rs:26:14 in function bad_address

Check 5: bad_address.pointer_dereference.2
         - Status: SUCCESS
         - Description: "dereference failure: pointer invalid"
         - Location: src/main.rs:26:14 in function bad_address

Check 6: bad_address.pointer_dereference.3
         - Status: SUCCESS
         - Description: "dereference failure: deallocated dynamic object"
         - Location: src/main.rs:26:14 in function bad_address

Check 7: bad_address.pointer_dereference.4
         - Status: SUCCESS
         - Description: "dereference failure: dead object"
         - Location: src/main.rs:26:14 in function bad_address

Check 8: bad_address.pointer_dereference.5
         - Status: FAILURE
         - Description: "dereference failure: pointer outside object bounds"
         - Location: src/main.rs:26:14 in function bad_address

Check 9: bad_address.pointer_dereference.6
         - Status: UNDETERMINED
         - Description: "dereference failure: invalid integer address"
         - Location: src/main.rs:26:14 in function bad_address


SUMMARY:
 ** 1 of 9 failed
Failed Checks: dereference failure: pointer outside object bounds
 File: "src/main.rs", line 26, in bad_address

VERIFICATION:- FAILED
Verification Time: 0.26855168s

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

To date, Kani does not support concurrency so it cannot be used to find the data race example from the previous article. The verification of concurrent programs using model checking remains an open area of research. Kani will print a warning when it detects concurrent code and compile it as sequential code.

warning: Kani currently does not support concurrency. The following constructs will be treated as sequential operations:
             - atomic_fence_acquire (1)
             - atomic_xadd_acqrel (1)
             - atomic_xsub_acquire (4)
             - atomic_cxchg_seqcst_acquire (1)
             - atomic_cxchg_acqrel_acquire (1)
             - atomic_cxchgweak_release_relaxed (2)
             - atomic_cxchgweak_relaxed_relaxed (2)
             - atomic_cxchgweak_acquire_relaxed (2)
             - atomic_load_acquire (5)
             - atomic_cxchgweak_acqrel_relaxed (2)
             - atomic_xchg_relaxed (1)
             - atomic_cxchgweak_seqcst_relaxed (2)
             - atomic_xchg_acqrel (1)
             - atomic_store_release (3)
             - atomic_cxchg_relaxed_seqcst (1)
             - atomic_cxchg_release_seqcst (1)
             - atomic_xadd_release (1)
             - atomic_fence_release (1)
             - atomic_xsub_relaxed (4)
             - atomic_fence_seqcst (1)
             - atomic_xsub_acqrel (4)
             - atomic_xadd_seqcst (1)
             - atomic_cxchgweak_relaxed_acquire (2)
             - atomic_load_relaxed (5)
             - atomic_cxchgweak_release_acquire (2)
             - atomic_cxchgweak_acquire_acquire (2)
             - atomic_cxchg_seqcst_seqcst (1)
             - atomic_cxchgweak_acqrel_acquire (2)
             - atomic_load_seqcst (5)
             - thread local (replaced by static variable) (8)
             - atomic_xchg_seqcst (1)
             - atomic_xchg_release (1)
             - atomic_cxchgweak_seqcst_acquire (2)
             - atomic_cxchg_acqrel_seqcst (1)
             - atomic_cxchg_release_relaxed (1)
             - atomic_cxchg_relaxed_relaxed (1)
             - atomic_store_seqcst (3)
             - atomic_cxchg_acquire_relaxed (1)
             - atomic_xadd_acquire (1)
             - atomic_fence_acqrel (1)
             - atomic_xsub_release (4)
             - atomic_cxchgweak_relaxed_seqcst (2)
             - atomic_xsub_seqcst (4)
             - atomic_cxchg_seqcst_relaxed (1)
             - atomic_cxchg_acqrel_relaxed (1)
             - atomic_cxchgweak_release_seqcst (2)
             - atomic_cxchg_acquire_seqcst (1)
             - atomic_cxchgweak_acquire_seqcst (2)
             - atomic_cxchgweak_acqrel_seqcst (2)
             - atomic_xchg_acquire (1)
             - atomic_cxchgweak_seqcst_seqcst (2)
             - atomic_store_relaxed (3)
             - atomic_cxchg_relaxed_acquire (1)
             - atomic_cxchg_release_acquire (1)
             - atomic_cxchg_acquire_acquire (1)
             - atomic_xadd_relaxed (1)

Another thing Kani cannot do yet is verify code called through FFI.^[8] If I write a Kani proof for the C library code called through FFI from the previous article:

#[kani::proof]
fn kani_c_ffi() {
    say_hello();
}

Kani will report the following warning:

warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (3)
         
         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

What About Model Checking C or C++?

Kani works by using the Rust compiler to generate Mid-Level Intermediate Representation (MIR) and then translates MIR into a format compatible with the C Bounded Model Checker (CBMC). However, CBMC can also be used to directly verify C or C++ code without involving Rust or Rust’s FFI.

Returning to the example of unsafe C code and adding an entry point to exercise this code:

#include <string.h>
#include <stdio.h>

// The function under test
void c_say_hello(const char *message) {
    char buffer[10];
    strcpy(buffer, message); // Unsafe: no bounds checking!
    printf("Hello from C! %s\n", buffer);
}

int main(void)
{
    char message = "Hi\0";
    c_say_hello(message);
    return 0;
}

CBMC can be run as follows to check pointers and bounds:

cbmc main.c --bounds-check --pointer-check

CBMC will identify the out-of-bound pointer dereference:

** Results:
/Library/Developer/CommandLineTools/SDKs/MacOSX14.sdk/usr/include/stdio.h function __sputc
[__sputc.overflow.1] line 264 arithmetic overflow on signed - in _p->_w - 1: SUCCESS
[__sputc.pointer_dereference.1] line 264 dereference failure: pointer NULL in _p->_w: SUCCESS
[__sputc.pointer_dereference.2] line 264 dereference failure: pointer invalid in _p->_w: SUCCESS
[__sputc.pointer_dereference.3] line 264 dereference failure: deallocated dynamic object in _p->_w: SUCCESS
[__sputc.pointer_dereference.4] line 264 dereference failure: dead object in _p->_w: SUCCESS
[__sputc.pointer_dereference.5] line 264 dereference failure: pointer outside object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.6] line 264 dereference failure: invalid integer address in _p->_w: SUCCESS
[__sputc.pointer_dereference.7] line 264 dereference failure: pointer NULL in _p->_w: SUCCESS
[__sputc.pointer_dereference.8] line 264 dereference failure: pointer invalid in _p->_w: SUCCESS
[__sputc.pointer_dereference.9] line 264 dereference failure: deallocated dynamic object in _p->_w: SUCCESS
[__sputc.pointer_dereference.10] line 264 dereference failure: dead object in _p->_w: SUCCESS
[__sputc.pointer_dereference.11] line 264 dereference failure: pointer outside object bounds in _p->_w: SUCCESS
[__sputc.pointer_dereference.12] line 264 dereference failure: invalid integer address in _p->_w: SUCCESS
[__sputc.pointer_dereference.13] line 264 dereference failure: pointer NULL in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.14] line 264 dereference failure: pointer invalid in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.15] line 264 dereference failure: deallocated dynamic object in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.16] line 264 dereference failure: dead object in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.17] line 264 dereference failure: pointer outside object bounds in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.18] line 264 dereference failure: invalid integer address in _p->_lbfsize: SUCCESS
[__sputc.pointer_dereference.19] line 265 dereference failure: pointer NULL in _p->_p: SUCCESS
[__sputc.pointer_dereference.20] line 265 dereference failure: pointer invalid in _p->_p: SUCCESS
[__sputc.pointer_dereference.21] line 265 dereference failure: deallocated dynamic object in _p->_p: SUCCESS
[__sputc.pointer_dereference.22] line 265 dereference failure: dead object in _p->_p: SUCCESS
[__sputc.pointer_dereference.23] line 265 dereference failure: pointer outside object bounds in _p->_p: SUCCESS
[__sputc.pointer_dereference.24] line 265 dereference failure: invalid integer address in _p->_p: SUCCESS
[__sputc.pointer_dereference.25] line 265 dereference failure: pointer NULL in *tmp_post: SUCCESS
[__sputc.pointer_dereference.26] line 265 dereference failure: pointer invalid in *tmp_post: SUCCESS
[__sputc.pointer_dereference.27] line 265 dereference failure: deallocated dynamic object in *tmp_post: SUCCESS
[__sputc.pointer_dereference.28] line 265 dereference failure: dead object in *tmp_post: SUCCESS
[__sputc.pointer_dereference.29] line 265 dereference failure: pointer outside object bounds in *tmp_post: SUCCESS
[__sputc.pointer_dereference.30] line 265 dereference failure: invalid integer address in *tmp_post: SUCCESS

 function __builtin___strcpy_chk
[__builtin___strcpy_chk.pointer_dereference.1] line 26 dereference failure: pointer NULL in src[(signed long int)i]: FAILURE
[__builtin___strcpy_chk.pointer_dereference.2] line 26 dereference failure: pointer invalid in src[(signed long int)i]: UNKNOWN
[__builtin___strcpy_chk.pointer_dereference.3] line 26 dereference failure: deallocated dynamic object in src[(signed long int)i]: FAILURE
[__builtin___strcpy_chk.pointer_dereference.4] line 26 dereference failure: dead object in src[(signed long int)i]: FAILURE
[__builtin___strcpy_chk.pointer_dereference.5] line 26 dereference failure: pointer outside object bounds in src[(signed long int)i]: FAILURE
[__builtin___strcpy_chk.pointer_dereference.6] line 26 dereference failure: invalid integer address in src[(signed long int)i]: FAILURE
[__builtin___strcpy_chk.pointer_dereference.7] line 27 dereference failure: pointer NULL in dst[(signed long int)i]: UNKNOWN
[__builtin___strcpy_chk.pointer_dereference.8] line 27 dereference failure: pointer invalid in dst[(signed long int)i]: UNKNOWN
[__builtin___strcpy_chk.pointer_dereference.9] line 27 dereference failure: deallocated dynamic object in dst[(signed long int)i]: UNKNOWN
[__builtin___strcpy_chk.pointer_dereference.10] line 27 dereference failure: dead object in dst[(signed long int)i]: UNKNOWN
[__builtin___strcpy_chk.pointer_dereference.11] line 27 dereference failure: pointer outside object bounds in dst[(signed long int)i]: UNKNOWN
[__builtin___strcpy_chk.pointer_dereference.12] line 27 dereference failure: invalid integer address in dst[(signed long int)i]: UNKNOWN

main.c function c_say_hello
[c_say_hello.precondition_instance.1] line 8 strcpy src/dst overlap: SUCCESS

** 5 of 44 failed (2 iterations)
VERIFICATION FAILED

CBMC can be run with the --trace flag to get more information on exactly where the error was detected. The output from CBMC is not as easy to reason about as Kani, but it is clearly a very powerful tool.^[9]

Conclusion

Model checking is a complex topic. I am new to it and I am certainly not an expert, but Kani makes it very accessible to Rust application developers, like me. For a deeper understanding of model checking in general and how Kani works in particular, I highly recommend the excellent talk Verifying Code Using Automated Reasoning by Rémi Delmas.^[10]

Whenever invariants can be expressed as proofs rather than as tests that may or may not be exhaustive, the mathematical guarantees of model checkers will provide stronger assurances the code is correct, even for boundary cases that are difficult to identify, in both safe and unsafe code.