Intro to Model Checking

Sometimes testing is not enough. We need stronger assurances about correctness than a battery of tests, no matter the amount, can give us. For example, let's say we have mission-critical unsafe code (e.g. bare-metal code running on a pace maker). We can't say "we're 95% sure this code has no unexpected behaviour". People's lives are at risk.

Is there a way to automatically prove that some code is correct? Not just that it passes on most inputs, but that all possible inputs will result in the behavior we specify.

Model Checking

Let's give a very simple example of where testing fails:

fn hard_to_test(input: u32) -> u32 {
    if input == 28894 {
        panic!("Evil edge case")
    } else {
        return 5;
    }
}

If we tried testing this like it was a black-box (ignoring how the inside of the function operates), we would never find the edge case that causes it to crash. Even property-based tests aren't able to find this edge case, because the search space is simply too large (2^32 == 4294967296).

On the other hand, model-checking can find this edge case:

#[cfg(kani)]
#[kani::proof]
fn check_hard_to_test() {
    let input = kani::any();
    hard_to_test(input);
}

$ cargo kani
...
RESULTS:
Check 1: hard_to_test.assertion.1
         - Status: FAILURE
         - Description: "Evil edge case"
         - Location: src/main.rs:7:9 in function hard_to_test


SUMMARY:
 ** 1 of 1 failed
Failed Checks: Evil edge case
 File: "src/main.rs", line 7, in hard_to_test
...

We can even do this for more difficult examples:

fn harder_to_test(input: u32) -> u32 {
    if input % 5 == 0 {
        panic!("Eviler edge case")
    } else {
        return 2;
    }
}

#[cfg(kani)]
#[kani::proof]
fn check_harder_to_test() {
    let input = kani::any();
    harder_to_test(input);
}

fn hardest_to_test(input: u32) -> u32 {
    if input % 5 == 6 {
        panic!("Evilest edge case")
    } else {
        return 2;
    }
}

#[cfg(kani)]
#[kani::proof]
fn check_hardest_to_test() {
    let input = kani::any();
    hardest_to_test(input);
}

For these examples, Kani determines that harder_to_test fails:

RESULTS:
Check 1: harder_to_test.assertion.1
         - Status: SUCCESS
         - Description: "attempt to calculate the remainder with a divisor of zero"
         - Location: src/main.rs:21:8 in function harder_to_test

Check 2: harder_to_test.arithmetic_overflow.1
         - Status: SUCCESS
         - Description: "attempt to calculate the remainder with a divisor of zero"
         - Location: src/main.rs:21:8 in function harder_to_test

Check 3: harder_to_test.assertion.2
         - Status: FAILURE
         - Description: "Eviler edge case"
         - Location: src/main.rs:22:9 in function harder_to_test


SUMMARY:
 ** 1 of 3 failed
Failed Checks: Eviler edge case
 File: "src/main.rs", line 22, in harder_to_test

VERIFICATION:- FAILED

but that hardest_to_test succeeds:

RESULTS:
Check 1: hardest_to_test.assertion.1
         - Status: SUCCESS
         - Description: "attempt to calculate the remainder with a divisor of zero"
         - Location: src/main.rs:36:8 in function hardest_to_test

Check 2: hardest_to_test.arithmetic_overflow.1
         - Status: SUCCESS
         - Description: "attempt to calculate the remainder with a divisor of zero"
         - Location: src/main.rs:36:8 in function hardest_to_test

Check 3: hardest_to_test.assertion.2
         - Status: SUCCESS
         - Description: "Evilest edge case"
         - Location: src/main.rs:37:9 in function hardest_to_test


SUMMARY:
 ** 0 of 3 failed

VERIFICATION:- SUCCESSFUL

If you read these functions, Kani is obviously right, but how does Kani know which of these functions have unexpected behaviour and which don't?

Symbolic Execution

Instead of treating every variable as a concrete value (e.g. let input: u32 = 5;), Kani treats every variable as if it could be any value. Then, these variables get constrained as possible values get eliminated. For example:

if x == 5 {
    ... // Already checked
} else {
    ... // Kani is here
}

Kani knows that x could be any u32, except for 5, since that branch was already eliminated.

Then, for every assertion, Kani determines the opposite of that condition (assert!(y == None) -> y != None).

Finally, the information Kani has about paths, constraints, and assertions is translated into satisfiability relations, and it checks that the negation of every assertion is impossible (unsatisfiable), using a SAT solver.

Here's an example I've annotated with comments:

fn example(x: u32, y: u32) -> u32 {
    if x > 5 {
        // I know x > 5 here
        if y > 5 || y < 5 {
            // I know that y > 5 || y < 5 here (in other words y == 5)
            
            if x - y == 0 {
                // I know x - y == 0 here, but that's impossible!
                // I know y must be 5, so in order for x - y == 0,
                // x would need to be 5, but x > 5.
                // Therefore, this panic is unreachable.

                // Additionally, I know the operation x - y is fine,
                // since y is exactly 5, and x is greater than 5,
                // so no underflow will occur.

                panic!("x - y is zero? Terrible!")
            } else {
                // I know x - y != 0 here

                return 2;
            }
        } else {
            // I know that !(y > 5 || y < 5) here (in other words y != 5)
            
            return 10;
        }
    } else {
        // I know x <= 5 here (opposite of x > 5)

        return 38949;
    }
}