Secrust

Secrust is a Rust crate designed to add formal verification to Rust code. By adding lightweight annotations to Rust functions, Secrust enables developers to verify their methods with annotated invariants, preconditions, and postconditions directly in their source code.

Secrust leverages Rust's syntax and ecosystem, integrating with the language's tooling to provide an intuitive developer experience. The crate uses the Z3 SMT solver to reason about program correctness and generates Control Flow Graphs (CFGs) to visualize execution paths, making it easier to identify and eliminate logical errors.

Supported Syntax

Secrust currently supports simple Rust code:

• Arithmetic operations: Verifying computations involving addition, subtraction, multiplication, and division.
• Conditional statements: Handling if/else branches to ensure correctness across all execution paths.
• Loops: Reasoning about loop invariants and termination conditions to verify iterative logic.

Run

Install secrust

Add Z3 on MacOS

1. Install Z3 using Homebrew:

   brew install z3
   brew info z3
   

2. Set environment variables to point to the Z3 paths (modify as needed for your setup):

   export Z3_SYS_Z3_HEADER=/opt/homebrew/Cellar/z3/4.13.3/include/z3.h
   export Z3_SYS_Z3_LIB_DIR=/opt/homebrew/Cellar/z3/4.13.3/lib
   export LIBRARY_PATH=/opt/homebrew/Cellar/z3/4.13.3/lib:$LIBRARY_PATH
   export LD_LIBRARY_PATH=/opt/homebrew/Cellar/z3/4.13.3/lib:$LD_LIBRARY_PATH
   

3. Install secrust pre-release using Cargo:

   cargo install secrust --version 0.1.0-alpha.3
   

Add Z3 on Windows

1. Download Z3:

   • Get the latest precompiled Z3 binary for Windows from the Z3 GitHub releases page.
   • Extract the ZIP file to a directory, e.g., C:\z3.
     • Ensure the extracted directory contains:
       • bin folder: Includes z3.exe and .dll files.
       • include folder: Contains header files like z3.h.

2. Set Environment Variables:

   • Add the following to your system environment variables:

     Z3_SYS_Z3_HEADER=C:\z3\include\z3.h
     Z3_SYS_Z3_LIB_DIR=C:\z3\bin
     LIBRARY_PATH=C:\z3\bin
     LD_LIBRARY_PATH=C:\z3\bin
     

   • Add C:\z3\bin to your PATH.

3. Ensure You Have GCC Installed:

   • If you don't have GCC installed, you can install it using MSYS2:
     1. Download and install MSYS2.
     2. Open the MSYS2 terminal and run:

        pacman -Syu
        pacman -S mingw-w64-x86_64-toolchain
        

     3. Add the following to your system PATH:

        C:\msys64\mingw64\bin
        

4. Ensure You Have LLVM Installed:

   • Install LLVM from LLVM's official website.
   • Add the bin directory of LLVM (e.g., C:\LLVM\bin) to your PATH.
   • Set the LIBCLANG_PATH environment variable:

     LIBCLANG_PATH=C:\LLVM\bin
     

5. Install secrust using Cargo:

   cargo install secrust --version 0.1.0-alpha.3
   

   Or if you download the repo:

   cargo install --path ..\secrust
   

Verify Installation

Run the following command to ensure secrust is installed correctly:

cargo secrust-verify --help

Usage

Run without generating DOT file CFG

Analyze a file without generating Control Flow Graphs:

cargo secrust-verify main.rs

Run generating DOT file CFG

Analyze a file and generate DOT files for the Control Flow Graph:

cargo secrust-verify src/main.rs --dot

DOT files are created in the src/graphs/filename directory for the specified file (e.g., src/main.rs).

You can visualize DOT code online on edotor.net

How it works: Verifying sum_first_n

The following example demonstrates how to verify a simple Rust function using secrust.

Example Code

Save the following code as src/main.rs, and make sure to annotate it with pre!, invariant! and post! assertions:

use secrust::{build_cfg, invariant, old, post, pre};

fn sum_first_n(n: i32) -> i32 {
    pre!(n >= 0);
    let mut sum = 0;
    let mut i = 1;
    invariant!(i <= n + 1 && sum == (i - 1) * i / 2);
    while i <= n {
        sum = sum + i;
        i = i + 1;
    }
    post!(sum == n * (n + 1) / 2);
    return sum;
}

fn main() {
    let n = 5;
    let sum = sum_first_n(n);
    println!("Sum is: {}", sum);
}

Run Verification

Run the secrust verification on this file:

cargo secrust-verify src/main.rs --dot

Outputs

1. Verification Results: The terminal will display the results of the verification, including logical implications and their validity status.
2. DOT Graphs: Control Flow Graphs (CFGs) will be generated in the src/graphs/main directory.

For example:

• main.dot will contain the CFG for the main function.
• basic_path_0.dot will contain the graph for the first basic execution path of the annotated sum_first_n function.

To generate a DOT format CFG for any method without adding logical annotations, add the build_cfg!(); macro at the start of the method.

Analyze the DOT Graph

Use tools like Graphviz to visualize the DOT files:

dot -Tpng src/graphs/main/basic_path_0.dot -o basic_path_0.png

Or paste the DOT code on an online editor like edotor.net.

Expected Behavior

• Verification checks the validity of the derived weakest precondition
• Generated graphs provide a clear view of the control flow and verification conditions.

How it works: Verifying sum_first_n

To showcase how Secrust works, let’s walk through the verification process for a simple Rust function that calculates the sum of the first ( n ) integers.

• pre! and post! annotate the function with input and output conditions.
• invariant! provides the loop invariant, which must hold before and after each iteration of while.

1. Generating a CFG and Basic Paths

When you run Secrust with the --dot flag:

cargo secrust-verify src/main.rs --dot

Secrust parses the AST to build a Control Flow Graph (CFG). Then it extracts basic paths, each corresponding to a distinct route through the function.

Figure: CFG generated by Secrust that was manually highlighted to show all basic paths extracted by Secrust and Path 3 basic path representation. Secrust will also save each basic path in a separate .DOT file

Among the paths generated, let’s focus on Path 3, the route taken when the while condition i <= n is true.

2. Deriving the Weakest Precondition

Secrust analyzes each basic path by traversing it backward from the postcondition, repeatedly applying WP rules.

1. Start from the loop invariant at the “bottom” of the path: i <= n + 1 AND sum == (i - 1) * i / 2

2. Move upward through assignments like:

   sum = sum + i;
   i = i + 1;
   

   which update sum to sum + i and i to i + 1. Secrust substitutes these into the invariant, yielding: (i + 1) <= n + 1 AND (sum + i) == ((i + 1) - 1) * (i + 1) / 2

3. Encounter the while i <= n (true branch). This adds an assumption: (i <= n) => ((i + 1) <= n + 1 AND (sum + i) == ((i + 1) - 1) * (i + 1) / 2)

4. Finally, we link it back to the loop’s starting invariant (the path’s precondition).

5. Hence, the final logical implication for Path 3 is: (i <= n + 1 AND sum == (i - 1) * i / 2) => (i <= n) => ((i + 1) <= n + 1 AND (sum + i) == ((i + 1) - 1) * (i + 1) / 2))

3. Z3 Verification

After deriving this implication, Secrust:

1. Builds a Z3 AST representing the formula in SMT-LIB syntax.
2. Asserts its negation in Z3. If unsatisfiable, the original implication holds, thus verifying the path.

Below is a simplified example of the final formula in SMT-LIB:

(=> (and (<= i (+ n 1)) (= sum (div (* (- i 1) i) 2)))
    (=> (<= i n)
        (and (<= (+ i 1) (+ n 1))
             (= (+ sum i) (div (* (- (+ i 1) 1) (+ i 1)) 2)))))

Because the solver reports unsatisfiable for its negation, Path 3 is verified. Repeating this process for all basic paths ensures the entire function satisfies its preconditions, invariants, and postconditions.

Summary

1. Annotated Rust Source → sum_first_n with pre!, post!, and invariant!.
2. CFG Construction → Identify cut points (annotations + loop edges).
3. Basic Paths → Distill distinct routes through the function.
4. WP Backward Analysis → Combine assignments, assumes, and asserts to derive a final logical condition.
5. Z3 Check → If all path formulas are valid, the function is verified.

License

Licensed under either of:

• Apache License, Version 2.0 (LICENSE-APACHE)
• MIT license (LICENSE-MIT)