Code Verification and Formal Methods

RecipeCratesCategories
Verify Your Rust Code with kanikanicat-development-tools
Concurrent Code Verificationshuttleloomcat-development-tools
loomloomcat-development-tools
shuttleshuttlecat-development-tools

Rust formal methods⮳.

Formal methods are a collection of mathematically rigorous techniques used to specify, design, and verify software and hardware systems. These methods employ formal logic and mathematical proofs to ensure the correctness and reliability of systems, especially those that are safety-critical or security-critical.

Program verification is the process of formally proving the correctness of a program. This involves analyzing the code and ensuring that it meets specific properties, such as:

  • Memory safety: The program does not have memory leaks, buffer overflows, or other memory-related errors.
  • Thread safety: The program can be executed concurrently without causing data races or other concurrency issues.
  • Functional correctness: The program produces the correct output for all valid inputs.
  • Performance: The program meets specific performance requirements, such as execution time or memory usage.

There are two main approaches to Rust program verification:

  1. Static verification: This involves analyzing the code at compile time to identify potential errors and prove the correctness of certain properties. Rust's type system and ownership model already provide a strong foundation for static verification. Additionally, tools like miri⮳ and kani⮳ can be used to perform more advanced static analysis.

  2. Dynamic verification: This involves running the program with different inputs and checking its behavior against expected results. Techniques like fuzz testing can be used to identify potential issues.

Verify Your Rust Code with kani

kani kani-crates.io kani-github kani-lib.rs cat-development-tools

kani⮳ is a Rust verifier / model checker. A model checker formally verifies that a system like a software program meets a given specification, using mathematical techniques (automated reasoning) to prove that a system satisfies a property for all possible states and behaviors. Model checkers explore the entire state space of the system, as opposed to approaches like fuzzing and property testing.

Model checking is a valuable technique for verifying the correctness of critical systems, such as safety-critical software and communication protocols. Kani is particularly useful for verifying unsafe code blocks. Some example properties you can prove with Kani include memory safety (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), the absence of some types of unexpected behavior (e.g., arithmetic overflows), in addition to user-specified assertions.

At present, Kani does not support verifying concurrent code.

Kani offers an easy installation option on three platforms:

  • x86_64-unknown-linux-gnu (Most Linux distributions).
  • x86_64-apple-darwin (Intel Mac OS).
  • aarch64-apple-darwin (Apple Silicon Mac OS).

Python version 3.7 or newer and the package installer pip must be installed.

Install with:

cargo install --locked kani-verifier

Then download the Kani compiler and other necessary dependencies, and place them under ~/.kani/ by default:

cargo kani setup

Run kani:

cargo kani [OPTIONS]

Kani works like cargo test except that it will analyze "proof harnesses" instead of running test harnesses.

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

Concurrent Code Verification

Loom attempts to check all possible interleavings, while Shuttle chooses interleavings randomly. The former is sound (like Kani), but the latter is more scalable to large problem spaces (like property testing).

shuttle

shuttle shuttle-crates.io shuttle-github shuttle-lib.rs cat-development-tools::testing cat-asynchronous cat-concurrency

shuttle⮳ is a library for testing concurrent Rust code.

loom

loom loom-crates.io loom-github loom-lib.rs cat-concurrency cat-data-structures

loom⮳ allows permutation testing for concurrent code.

Other Tools

  • MIRAI⮳.
  • prusti⮳ is an automated program verifier for Rust, based on the Viper infrastructure. It leverages Rust's strong type guarantees to simplify the specification and verification of Rust programs.
  • Creusot⮳ helps you prove your code is correct in an automated fashion.
  • crucible (symbolic execution).

Related Topics

TopicRust Crates
Static Analysis/Lintingclippy⮳ (for catching common code errors and style issues)
Property-Based Testingproptest⮳, quickcheck
Unit TestingUse cargo test (built-in testing framework)
Integration TestingOften usescargo test. Focuses on testing interactions between modules or components.
Fuzzingcargo fuzz, afl.rs⮳ (bindings to AFL)
Code Review Tools: Not Rust-specific, but used in conjunction with Rust code. Examples: GitHub, GitLab, etc.

References