Kani

s2n-quic uses the Kani Rust Verifier tool for verifying properties throughout various places in the codebase. The Kani test harnesses are written using bolero, which is also capable of running them as concrete tests.

Getting started

First, you will need make sure you install Rust and Kani on your system.

Install Rust

The easiest way to install Rust is via rustup. Otherwise, check your system’s package manager for recommended installation methods.

Install Kani

Kani is installed with cargo:

$ cargo install kani-verifier
$ cargo-kani setup

Running Kani proofs

After installing Rust and Kani, you can run the s2n-quic proof harnesses. These are currently all located in the s2n-quic-core crate:

$ cd quic/s2n-quic-core
$ cargo kani --tests

Listing Kani proofs

You can find all of the kani harnesses by searching for kani::proof

$ cd quic/s2n-quic-core
$ grep -Rn 'kani::proof' .

< LIST OF LOCATIONS WITH KANI PROOFS >