#![allow(unused)]
fn main() {
use my_crate::{function_under_test, meets_specification, precondition};

#[kani::proof]
fn check_my_property() {
   // Create a nondeterministic input
   let input = kani::any();

   // Constrain it according to the function's precondition
   kani::assume(precondition(input));

   // Call the function under verification
   let output = function_under_test(input);

   // Check that it meets the specification
   assert!(meets_specification(input, output));
}
}

• Kani tries to prove that all valid inputs produce outputs that meet specifications, without panicking.
• Else, Kani generates a trace that points to the failure.

Kani Proof

#![allow(unused)]
fn main() {
#[cfg(kani)]
#[kani::proof]
fn proof_u32_roundtrip {
  let val: u16 = kani::any();
  assert_eq!(u16::decode(&mut
    val.encode()[..]).unwrap(), val)
}
}

verifies exhaustively all values of u16

---v

Under the Hood: Bounded Model Checking

Idea:

• Search for counterexamples in (bounded) executions paths
• However, this search is an NP-hard problem

Method:

• Efficiently reduce problem to a Constraint Satisfaction (SAT) problem
• verification reduced to problem of searching satisfiable assignment to a SAT formula.
• leverages highly optimized SAT solvers making the search tractable.

Notes:

Kani uses miniSAT as the backend engine; a lot of other verification tools use Z3 solver.

---v

Translation to constraints

#![allow(unused)]
fn main() {
fn foo(x: i32) -> i32 {
    let mut y: i32 = 8;
    let mut w: i32 = 0;
    let mut z: i32 = 0;
    if x != 0 {
        z -= 1;
    } else {
        w += 1;
    }
    assert!(z == 7 || w == 9);
    w+z
}
}

#![allow(unused)]
fn main() {
y = 8,
z = x? y-1: 0,
w = x? y+1: 0,
z != 7 /\ w != 9 (negation of the assert condition)
}

---v

How does it handle loops?

• Bounded in BMC to the rescue!
• Loops are unwound up to a certain bounded depth $k$, else the verification does not terminate.
• Determining the sweet-spot $k$ is a trade-off between tractability and verification confidence .

---v

Demo: Unwinding Loops

#![allow(unused)]
fn main() {
fn initialize_prefix(length: usize, buffer: &mut [u8]) {
    // Let's just ignore invalid calls
    if length > buffer.len() {
        return;
    }

    for i in 0..=length {
        buffer[i] = 0;
    }
}

#[cfg(kani)]
#[kani::proof]
#[kani::unwind(1)] // deliberately too low
fn check_initialize_prefix() {
    const LIMIT: usize = 10;
    let mut buffer: [u8; LIMIT] = [1; LIMIT];

    let length = kani::any();
    kani::assume(length <= LIMIT);

    initialize_prefix(length, &mut buffer);
}
}

---v

Dealing with Loops: Summary

Process:

• Start with unwinding $k$ times
• If no bug is found, increase $k$ until either:
  • A bug is found
  • verifier times-out
  • predetermined upper-bound $N$ for $k$ is reached

---v

Implementing Arbitrary for custom type

#![allow(unused)]
fn main() {
use arbitrary::{Arbitrary, Result, Unstructured};

#[derive(Copy, Clone, Debug)]
pub struct Rgb {
    pub r: u8,
    pub g: u8,
    pub b: u8,
}

impl<'a> Arbitrary<'a> for Rgb {
    fn arbitrary(u: &mut Unstructured<'a>) -> Result<Self> {
        let r = u8::arbitrary(u)?;
        let g = u8::arbitrary(u)?;
        let b = u8::arbitrary(u)?;
        Ok(Rgb { r, g, b })
    }
}
}

Exercise

Verify Fixed-width & Compact Encoding for integer types in SCALE.

Open Ended properties!

• RoundTrip: Decode (Encode (x)) == x
• DecodeLength(x) == Decode(x).length()
• EncodeAppend(vec,item) == Encode(vec.append(item))
• ......

Notes:

• Potentially, we might play around with a few of these properties during a workshop this weekend.

More Verification

Less Bugs

Questions