diff --git a/.github/workflows/kmir.yml b/.github/workflows/kmir.yml new file mode 100644 index 0000000000000..ab70092167c78 --- /dev/null +++ b/.github/workflows/kmir.yml @@ -0,0 +1,33 @@ +name: KMIR + +on: + workflow_dispatch: + merge_group: + pull_request: + branches: [ main ] + push: + paths: + - 'library/**' + - '.github/workflows/kmir.yml' + - 'kmir-proofs/**' + +jobs: + run-kmir-proofs: + name: Run supplied KMIR proofs + runs-on: ubuntu-latest + env: + container_name: "kmir-${{ github.run_id }}" + + steps: + - name: Checkout Repository + uses: actions/checkout@v4 + + - name: Run Proofs in Tool Container + run: | + docker run --rm -t \ + --name ${{ env.container_name }} \ + -w /home/kmir/workspace \ + -u $(id -u):$(id -g) \ + -v $PWD:/home/kmir/workspace \ + runtimeverificationinc/kmir:ubuntu-jammy-0.3.152 \ + kmir-proofs/unchecked_arithmetic/run-proofs.sh diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 29894869eecfc..b5963f1ddd4c5 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -10,6 +10,7 @@ - [Kani](./tools/kani.md) - [GOTO Transcoder](./tools/goto-transcoder.md) - [VeriFast](./tools/verifast.md) + - [KMIR](./tools/kmir.md) --- diff --git a/doc/src/tools.md b/doc/src/tools.md index 4de93a49686ee..b746c7afd3ec9 100644 --- a/doc/src/tools.md +++ b/doc/src/tools.md @@ -14,7 +14,7 @@ please see the [Tool Application](general-rules.md#tool-applications) section. | Kani Rust Verifier | [![Kani](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kani.yml) | | GOTO-Transcoder (ESBMC) | [![GOTO-Transcoder](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/goto-transcoder.yml) | | VeriFast for Rust | [![VeriFast](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/verifast.yml) | - + | KMIR Symbolic Rust Execution | [![KMIR](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml/badge.svg)](https://github.com/model-checking/verify-rust-std/actions/workflows/kmir.yml) | diff --git a/doc/src/tools/kmir.md b/doc/src/tools/kmir.md new file mode 100644 index 0000000000000..9840b651fb4b2 --- /dev/null +++ b/doc/src/tools/kmir.md @@ -0,0 +1,218 @@ +## Tool Name +**KMIR** + +## Description + +[KMIR](https://github.com/runtimeverification/mir-semantics) is a formal +verification tool for Rust that defines the operational semantics of Rust’s +Middle Intermediate Representation (MIR) in K (through Stable MIR). By +leveraging the [K framework](https://kframework.org/), KMIR provides a parser, +interpreter, and symbolic execution engine for MIR programs. This tool enables +direct execution of concrete and symbolic input, with step-by-step inspection of +the internal state of the MIR program's execution, serving as a foundational +step toward full formal verification of Rust programs. Through the dependency +[Stable MIR JSON](https://github.com/runtimeverification/stable-mir-json/), KMIR +allows developers to extract serialized Stable MIR from Rust’s compilation +process, execute it, and eventually prove critical properties of their +code. + +This diagram describes the extraction and verification workflow for KMIR: + +![kmir_env_diagram_march_2025](https://github.com/user-attachments/assets/bf426c8d-f241-4ad6-8cb2-86ca06d8d15b) + + +The K Framework ([kframework.org](https://kframework.org/) is the basis of how +KMIR operates to guarantee properties of Rust programs. K is a rewrite-based +semantic framework based on [matching logic](http://www.matching-logic.org/) in +which programming languages, their operational semantics and type systems, and +formal analysis tools can be defined through syntax, configurations, and rules. +The _syntax_ definitions in KMIR model the AST of Stable MIR (e.g., the +statements and terminator of a basic block in a function body) and configuration +data that exists at runtime (e.g., the stack frame structure of a function +call). +The _configuration_ of a KMIR program organizes the state of an executed program in +nested configuration units called cells (e.g., a stack frame is part of a stack +stored in the configuration). +_K Framework transition rules_ of the KMIR semantics are rewriting steps that +match patterns and transform the current continuation and state accordingly. +They describe how program configuration and its contained data changes when +particular program statements or terminators are executed (e.g., a returning +function modifies the call stack and writes a return value into the caller's +local variables). + +Using the K semantics of Stable MIR, the KMIR execution of an entire Rust +program represented as Stable MIR breaks down to a series of configuration +rewrites that compute data held in local variables, and the program may either +terminate normally or reach an exception or construct with undefined behaviour, +which terminates the execution abnormally. KMIR is designed to provide sound +assurances about undefined behavior (UB) in Rust’s MIR. Rather than statically +over‑approximating or flagging UB at every unsafe block, KMIR models the full +MIR semantics, including UB transitions, using a **refusal-to-execute** strategy. +This means that if symbolic execution reaches a MIR instruction and cannot prove +that executing it would not result in UB (e.g., an out-of-bounds pointer dereference +or an unchecked arithmetic overflow), execution halts in a `UB DETECTED` state. +This state cannot be unified with a valid target state in the proof, so the proof +fails. KMIR systematically explores all feasible paths under the user-supplied +preconditions. Only when **every** path terminates without hitting UB *and* +satisfies the target property does KMIR declare the program UB-free (and correct +for the property). This ensures that any “no UB” claim holds under the sole assumption +that KMIR’s implementation is correct. + +Programs modelled in K Framework can be executed _symbolically_, i.e., operating +on abstract input which is not fully specified but characterized by _path conditions_ +(e.g., that an integer variable holds an unknown but non-negative value). + +K (and thus KMIR) verifies program correctness by performing an +_all-path-reachability proof_ using the symbolic execution engine and verifier +derived from the K encoding of the Stable MIR operational semantics. +The K semantics framework is based on reachability logic, which is a theory +describing transition systems in [matching logic](http://www.matching-logic.org/). +An all-path-reachability proof in this system verifies that a particular +_target_ end state is _always_ reached from a given starting state. +The rewrite rules branch on symbolic inputs covering the possible transitions, +creating a model that is provably complete. For all-path reachability, every +leaf state is required to unify with the target state. +A one-path-reachability proof is similar to the above, but the proof requirement +is that _at least one_ leaf state unifies with the target state. + +When performing a proof of a program that involves recursion or a loop construct, +one of several possible techniques can be used: + +1) K (and thus KMIR) are capable of unbounded verification via allowing the + user to write loop invariants. However, these loop invariants would then + need to be written in K's native language. +2) As potential future work, it would be possible to implement an annotation + language to provide the required context for loop invariant directly in + source code (as done in the past using natspec for Solitidy code). +3) In general, K also supports bounded loop unrolling, by way of identifying + loop heads and counting how many times the same loop head has been observed. + This technique is managed by the all-path reachability prover library for + K and works out of the box with suitable arguments, without requiring any + special support from the back-end. + +Our front-end, at the time of writing, does not have either of these +options turned on. As soon as larger programs will require it, we will decide +whether the preference is to implement support for user-supplied K-level +loop invariants, or bounded loop unrolling support, or (probably) offer both. + +KMIR also prioritizes UI with interactive proof exploration available +out-of-the-box through the terminal KCFG (K Control Flow Graph) viewer, allowing +users to inspect intermediate states of the proof to get feedback on the +successful path conditions and failing at unifying with the target state. An +example of a KMIR proof being analyzed using the KCFG viewer can be seen below: + +image + + +## Tool Information + +* [x] Does the tool perform Rust verification? + *Yes – It performs verification at the MIR level, an intermediate + representation of Rust programs in the Rust compiler `rustc`.* +* [x] Does the tool deal with *unsafe* Rust code? + *Yes – By operating on MIR, KMIR can analyze both safe and unsafe Rust code.* +* [x] Does the tool run independently in CI? + *Yes – KMIR can be integrated into CI workflows via our package manager and + Nix-based build system or through a docker image provided.* +* [x] Is the tool open source? + *Yes – KMIR is [open source and available on GitHub](https://github.com/runtimeverification/mir-semantics).* +* [x] Is the tool under development? + *Yes – KMIR is actively under development, with ongoing improvements to MIR + syntax coverage and verification capabilities.* +* [x] Will you or your team be able to provide support for the tool? + *Yes – The Runtime Verification team is committed to supporting KMIR and will + provide ongoing maintenance and community support.* + +## Licenses +KMIR is released under an OSI-approved open source license. It is distributed +under the BSD-3 clause license, which is compatible with the Rust standard +library licenses. Please refer to the [KMIR GitHub +repository](https://github.com/runtimeverification/mir-semantics?tab=BSD-3-Clause-1-ov-file) +for full license details. + +## Comparison to Other Approved Tools +The other tools approved at the time of writing are Kani, Verifast, and +Goto-transcoder (ESBMC). + +- **Verification Backend:** KMIR primarily differs from all of these tools by + utilizing a unique verification backend through the K framework and + reachability logic (as explained in the description above). KMIR has little + dependence on an SAT solver or SMT solver. Kani's CBMC backend and + Goto-transcoder (ESBMC) encode the verification problem into an SAT / SMT + verification condition to be discharged by the appropriate solver. Kani + recently added a Lean backend through Aeneas, however Lean does not support + matching or reachability logic currently. Verifast performs symbollic + execution of the verification target like KMIR, however reasoning is performed + by annotating functions with design-by-contract components in separation + logic. +- **Verification Input:** KMIR takes input from Stable MIR JSON, an effort to + serialize the internal MIR in a portable way that can be reusable by other + projects. +- **K Ecosystem:** Since all tools in the K ecosystem share a common foundation + of K, all projects benefit from development done by other K projects. This + means that performance and user experience are projected to improve due to the + continued development of other semantics. + +## Steps to Use the Tool + +The [KMIR docker +image](https://github.com/runtimeverification/mir-semantics/blob/c221c81d73a56c48692a087a2ced29917de99246/Dockerfile.kmir) +is currently the best option for casual users of KMIR. It contains an +installation of K Framework, the tool `kmir`, and the `stable-mir-json` +extraction tool, which is a custom version of `rustc` which extracts Stable MIR +as JSON or as graphviz' *.dot when compiling a crate. +The image is [available on Docker Hub](https://hub.docker.com/r/runtimeverificationinc/kmir/tags). + +Alternatively, the tools for `kmir` can be built from source as [described in +the `mir-semantics` repository's +`README.md`](https://github.com/runtimeverification/mir-semantics). This +requires an installation of `K Framework`, best done [using the `kup` +tool](https://github.com/runtimeverification/kup/README.md), and includes a +git submodule dependency on `stable-mir-json`. + +The `stable-mir-json` tool is a custom driver for `rustc` which, while compiling +Rust code, writes the code's Stable MIR, represented in a JSON format, to a +file. Just like `rustc` itself, `stable-mir-json` extracts MIR of a single +crate and must be invoked via `cargo` for multi-crate programs. Besides the JSON +extraction, `stable-mir-json` can also write a graphviz `dot` file representing +the Stable MIR structure of all functions and their call graph within the crate. + +The `kmir` tool provides commands to work with the Stable MIR representation of +Rust programs that `stable-mir-json` extracts. + +* Run Stable MIR code extracted from Rust programs (`kmir run my-program.smir.json`); +* Prove that a given Rust program or function will terminate without panics or + undefined behaviour (`kmir prove-rs my-program.rs [--start-symbol my_function]`). + This command invokes `stable-mir-json` internally, and then performs an all-path + reachability proof that the program reaches normal termination under all possible inputs. + Any statements that would panic or cause undefined behaviour will terminate execution + so this proves the successful execution. Pre-and post-conditions can be modelled + using assertions and conditional execution. +* (Advanced use for K experts:) Prove a property about a Rust program, which is given + as a K "claim" and proven using an all-path reachability proof in K + (`kmir prove my-program-spec.k`); +* Print or inspect the control flow graph of a program's proof constructed by the + `kmir prove` or `kmir prove-rs` commands (`kmir show module.proof_identifier` + and `kmir view module.proof_identifier`); + +An example of proofs using KMIR, and how to construct them in Rust code, +are [provided in the `kmir-proofs` +directory](https://github.com/model-checking/verify-rust-std/tree/main/kmir-proofs). + +The `kmir` tool is under active development at the time of writing. +Future development will include using source code annotations instead of explicit +test functions to better integrate with Rust code bases, using a suitable annotation +language to express pre- and post-conditions. + +## Background Reading + +- **[Matching Logic](http://www.matching-logic.org/)** + Matching Logic is a foundational logic underpinning the K framework, providing + a unified approach to specifying, verifying, and reasoning about programming + languages and their properties in a correct-by-construction manner. + +- **[K Framework](https://kframework.org/)** + The K Framework is a rewrite-based executable semantic framework designed for + defining programming languages, type systems, and formal analysis tools. It + automatically generates language analysis tools directly from their formal + semantics. diff --git a/kmir-proofs/README.md b/kmir-proofs/README.md new file mode 100644 index 0000000000000..76f899d7ce20f --- /dev/null +++ b/kmir-proofs/README.md @@ -0,0 +1,107 @@ +# Formal Rust Code Verification Using KMIR + +This directory contains a collection of programs and specifications to +illustrate how KMIR can validate the properties of Rust programs and +standard library functions. + + +## Setup + +KMIR verification can either be run from [docker images provided under +`runtimeverificationinc/kmir`](https://hub.docker.com/r/runtimeverificationinc/kmir), +or using a local installation of +[`mir-semantics`](https://github.com/runtimeverification/mir-semantics/) +with its dependency +[`stable-mir-json`](https://github.com/runtimeverification/stable-mir-json). The +installation is described in the repository's `README.md` files. + +The following description assumes that the `kmir` tool and `stable-mir-json` are +installed and available on the path. + +## Program Property Proofs in KMIR + +The most user-friendly way to create and run a proof in KMIR is the `prove-rs` +functionality, which allows a user to prove that a given program will +run to completion without an error. + +Desired post-conditions of the program, such as properties of the computed result, +can be formulated as simple `assert` statements. Preconditions can be modelled +as `if` statements which skip execution altogether if the precondition is not met. +They can be added to a test function using the following macro: + +```Rust +/// If the precondition is not met, the program is not executed (exits cleanly, ex falso quodlibet) +macro_rules! precondition { + ($pre:expr, $block:expr) => { + if $pre { $block } + }; +} +``` +If the precondition is not met, the statements in `$block` won't be executed. If +the `$block` is executed, we can assume that the boolean expression `$pre` holds +true. + +KMIR will stop executing the program as soon as any undefined behaviour arises +from the executed statements. Therefore, running to completion proves the absense +of undefined behaviour, as well as the post-conditions expressed as assertions +(possibly under the assumption of preconditions modelled using the above macro). + +## Example: Proving Absense of Undefined Behaviour in `unchecked_*` arithmetic + +The proofs in subdirectory `unchecked_arithmetic` concern a section of +the challenge of securing [Safety of Methods for Numeric Primitive +Types](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html#challenge-11-safety-of-methods-for-numeric-primitive-types) +of the Verify Rust Standard Library Effort. + + +As an example of a property proof in KMIR, consider the following function which +tests that `unchecked_add` does not trigger undefined behaviour if its safety +conditions are met by the arguments: + +```Rust +fn unchecked_add_i32(a: i32, b: i32) { + + precondition!( + ((a as i128 + b as i128) <= i32::MAX as i128) && + ( a as i128 + b as i128 >= i32::MIN as i128), + // ========================================= + unsafe { + let result = a.unchecked_add(b); + assert!(result as i128 == a as i128 + b as i128) + } + ); +} +``` + +According to the [documentation of the unchecked_add function for the i32 primitive +type](https://doc.rust-lang.org/std/primitive.i32.html#method.unchecked_add), + +> "This results in undefined behavior when `self + rhs > i32::MAX` or +> `self + rhs < i32::MIN`, i.e. when `checked_add` would return `None`" + + +If the sum of the two arguments `a` and `b` does not exceed the bounds of type `i32` +(checked by computing it in range `i128`), the `unchecked_add` function should +not trigger undefined behaviour and produce the correct result, expressed by the +`precondition` macro and the assertion at the end of the unsafe block. + +To run the proof, we execute `kmir prove-rs` and provide the function name as +the `--start-symbol`. The `--verbose` option allows for watching the proof being +executed, the `--proof-dir` will contain data about the proof's intermediate states +that can be inspected afterwards. + +```shell +kmir prove-rs unchecked_arithmetic.rs --proof-dir proof --start-symbol unchecked_add_i32 --verbose +``` + +After the proof finishes, the prover reports whether it passed or failed, and some +details about the execution control flow graph (such as number of nodes and leaves). +The graph can be shown or interactively inspected using commands `kmir show` and `kmir view`: + +```shell +kmir view --proof-dir proof unchecked_arithmetic.unchecked_add_i32 +kmir show --proof-dir proof unchecked_arithmetic.unchecked_add_i32 [--no-full-printer] +``` + +While `kmir show` only prints the control flow graph, `kmir view` opens an interactive +viewer where the graph nodes can be selected and displayed in different modes. diff --git a/kmir-proofs/unchecked_arithmetic/run-proofs.sh b/kmir-proofs/unchecked_arithmetic/run-proofs.sh new file mode 100755 index 0000000000000..bb9642a1aaffe --- /dev/null +++ b/kmir-proofs/unchecked_arithmetic/run-proofs.sh @@ -0,0 +1,28 @@ +#! /bin/bash + +set -eu + +DIR=$(realpath $(dirname $0)) + +cd $DIR + +start_symbols=$(sed -n -e 's,// @kmir prove-rs: ,,p' unchecked_arithmetic.rs) +# By default: unchecked_add_i32 unchecked_sub_usize unchecked_mul_isize +# See `main` in program. start symbols need to be reachable from `main`. + +echo "Running proofs for start symbols ${start_symbols} in unchecked_arithmetic.rs" + +for sym in ${start_symbols}; do + echo "#########################################" + echo "Running proof for $sym" + echo "#########################################" + + kmir prove-rs --start-symbol $sym --verbose --proof-dir proofs --reload unchecked_arithmetic.rs + + echo "#########################################" + echo "Proof finished, with the following graph:" + echo "#########################################" + kmir show --proof-dir proofs unchecked_arithmetic.${sym} --no-full-printer + + echo "#########################################" +done diff --git a/kmir-proofs/unchecked_arithmetic/unchecked_arithmetic.rs b/kmir-proofs/unchecked_arithmetic/unchecked_arithmetic.rs new file mode 100644 index 0000000000000..333ab6169bcca --- /dev/null +++ b/kmir-proofs/unchecked_arithmetic/unchecked_arithmetic.rs @@ -0,0 +1,125 @@ +// @kmir prove-rs: unchecked_add_i32 unchecked_sub_usize unchecked_mul_isize + +fn main() { + unchecked_add_i32(1,2); + unchecked_sub_usize(1, 2); + unchecked_mul_isize(1, 2); +} + +/// If the precondition is not met, the program is not executed (exits cleanly, ex falso quodlibet) +macro_rules! precondition { + ($pre:expr, $block:expr) => { + if $pre { $block } + }; +} + +///////////////////////////////////////////////////////////////////// + +fn unchecked_add_i32(a: i32, b: i32) { + + precondition!( + ((a as i64 + b as i64) <= i32::MAX as i64) && + ( a as i64 + b as i64 >= i32::MIN as i64), + // ========================================= + unsafe { + let result = a.unchecked_add(b); + assert!(result as i64 == a as i64 + b as i64) + } + ); +} + + +macro_rules! unchecked_add_claim_for { + ($name:ident, $ty:ident) => { + #[allow(unused)] + fn $name(a: $ty, b: $ty) + { + use std::$ty; + precondition!( + ((a as i128 + b as i128) <= $ty::MAX as i128) && + ( a as i128 + b as i128 >= $ty::MIN as i128), + // ========================================= + unsafe { + let result = a.unchecked_add(b); + assert!(result as i128 == a as i128 + b as i128) + } + ); + } + } +} + +unchecked_add_claim_for!(unchecked_add_i8 , i8 ); +unchecked_add_claim_for!(unchecked_add_i16 , i16 ); +// unchecked_add_claim_for!(unchecked_add_i32 , i32 ); // already above +unchecked_add_claim_for!(unchecked_add_i64 , i64 ); +unchecked_add_claim_for!(unchecked_add_isize, isize); +unchecked_add_claim_for!(unchecked_add_u8 , u8 ); +unchecked_add_claim_for!(unchecked_add_u16 , u16 ); +unchecked_add_claim_for!(unchecked_add_u32 , u32 ); +unchecked_add_claim_for!(unchecked_add_u64 , u64 ); +unchecked_add_claim_for!(unchecked_add_usize, usize); + +///////////////////////////////////////////////////////////////////// + +macro_rules! unchecked_sub_claim_for { + ($name:ident, $ty:ident) => { + #[allow(unused)] + fn $name(a: $ty, b: $ty) + { + use std::$ty; + precondition!( + ((a as i128 - b as i128) <= $ty::MAX as i128) && + ( a as i128 - b as i128 >= $ty::MIN as i128), + // ========================================= + unsafe { + let result = a.unchecked_sub(b); + assert!(result as i128 == a as i128 - b as i128) + } + ); + } + } +} + +unchecked_sub_claim_for!(unchecked_sub_i8 , i8 ); +unchecked_sub_claim_for!(unchecked_sub_i16 , i16 ); +unchecked_sub_claim_for!(unchecked_sub_i32 , i32 ); +unchecked_sub_claim_for!(unchecked_sub_i64 , i64 ); +unchecked_sub_claim_for!(unchecked_sub_isize, isize); +unchecked_sub_claim_for!(unchecked_sub_u8 , u8 ); +unchecked_sub_claim_for!(unchecked_sub_u16 , u16 ); +unchecked_sub_claim_for!(unchecked_sub_u32 , u32 ); +unchecked_sub_claim_for!(unchecked_sub_u64 , u64 ); +unchecked_sub_claim_for!(unchecked_sub_usize, usize); + +///////////////////////////////////////////////////////////////////// + +macro_rules! unchecked_mul_claim_for { + ($name:ident, $ty:ident) => { + #[allow(unused)] + fn $name(a: $ty, b: $ty) + { + use std::$ty; + precondition!( + ((a as i128 * b as i128) <= $ty::MAX as i128) && + ( a as i128 * b as i128 >= $ty::MIN as i128), + // ========================================= + unsafe { + let result = a.unchecked_mul(b); + assert!(result as i128 == a as i128 * b as i128) + } + ); + } + } +} + +unchecked_mul_claim_for!(unchecked_mul_i8 , i8 ); +unchecked_mul_claim_for!(unchecked_mul_i16 , i16 ); +unchecked_mul_claim_for!(unchecked_mul_i32 , i32 ); +unchecked_mul_claim_for!(unchecked_mul_i64 , i64 ); +unchecked_mul_claim_for!(unchecked_mul_isize, isize); +unchecked_mul_claim_for!(unchecked_mul_u8 , u8 ); +unchecked_mul_claim_for!(unchecked_mul_u16 , u16 ); +unchecked_mul_claim_for!(unchecked_mul_u32 , u32 ); +// insufficient bit size for precondition +// unchecked_mul_claim_for!(unchecked_mul_u64 , u64 ); +// unchecked_mul_claim_for!(unchecked_mul_usize, usize);