MirChecker: A Simple Static Analysis Tool for Rust

This tool tries to analyze the MIR generated by the Rust compiler and emit diagnostic messages. It is based on the theory of Abstract Interpretation.

Information about bugs detected by this tool are listed in Trophy Case.

The associated paper titled MirChecker: Detecting Bugs in Rust Programs via Static Analysis will appear at the 28th ACM Conference on Computer and Communications Security (CCS '21).

Requirements

• Rust nightly, as specified in rust-toolchain.

• rustc-dev and llvm-tools-preview:

  $ rustup component add rustc-dev llvm-tools-preview

• GMP, MPFR, PPL and Z3:

  # For Ubuntu:
  $ sudo apt-get install libgmp-dev libmpfr-dev libppl-dev libz3-dev
  
  # For macOS:
  $ brew install gmp mpfr ppl z3

Build

1. Clone the repository (use --recursive to initialize the nested submodule)

   $ git clone --recursive https://github.com/lizhuohua/rust-mir-checker.git
   
   $ cd rust-mir-checker

2. Build & Install

   # You can build and install the cargo subcommand:
   $ cargo install --path .
   
   # Or, you can only build the checker itself:
   $ cargo build

Example

The following is a simple example which contains an out-of-bounds access. For more examples, please see tests and trophy-case.

fn main() {
    let mut a = [1, 2, 3, 4, 5];
    let mut i = 0;
    while i < 5 {
        a[i] = i;
        i = i + 1;
    }
    a[i] = 100;
}

It compiles but will panic at runtime. Our checker can detect it at compile time, the following command will emit a warning:

$ target/debug/mir-checker examples/loop-buffer-overflow.rs --entry main --domain interval --widening_delay 5 --narrowing_iteration 5
warning: [MirChecker] Provably error: index out of bound
 --> examples/loop-buffer-overflow.rs:8:5
  |
8 |     a[i] = 100;
  |     ^^^^

Usage

Before using this tool, make sure your Rust project compiles without any errors or warnings.

# If you have installed the cargo subcommand:
$ cargo mir-checker -- --entry <entry-function-name> --domain <abstract-domain> --widening_delay <N> --narrowing_iteration <N> --suppress_warnings <S>

# Or, you can directly run the checker for a single file
$ target/debug/mir-checker <path-to-file> --entry <entry-function-name> --domain <abstract-domain> --widening_delay <N> --narrowing_iteration <N> --suppress_warnings <S>

• <entry-function-name> is the entry function. The default value is main.
• <abstract-domain> is the numerical abstract domain. Currently, 7 abstract domains are supported: interval, octagon, polyhedra, linear_equalities, ppl_polyhedra, ppl_linear_congruences, and pkgrid_polyhedra_linear_congruences.
• widening_delay controls the number of iterations before triggering widening. <N> is an unsigned integer.
• narrowing_iteration controls the maximum number of narrowing operations that may improve the result. <N> is an unsigned integer.
• suppress_warnings filters out some specific kinds of warnings. <S> is a string where each character represents a kind of warning: a: arithmetic overflow, b: bit-wise overflow, s: inline assembly, c: comparison operations, d: division by zero / remainder by zero, m: memory-safety issues, p: run into panic code, i: out-of-bounds access.

Debug

Set RUST_LOG environment variable to enable logging:

# Enable all logging
$ export RUST_LOG=rust_mir_checker

# Can also set logging level
$ export RUST_LOG=rust_mir_checker=debug

For more settings, please see the documents of env_logger.

Future Work

There are a lot of limitations of MirChecker that we would like to address in the future:

1. Eliminating runtime panics for unsupported cases
2. Reducing false positives
3. Better support for interprocedural analysis
4. Better support for analyzing the standard library
5. Adding support for user annotations

Troubleshooting

For macOS, you may encounter dyld: Library not loaded error, try setting:

$ export LD_LIBRARY_PATH=$(rustc --print sysroot)/lib:$LD_LIBRARY_PATH

Credits

Many ideas and code bases are from the following projects, many thanks!

• MIRAI
• Crab
• IKOS
• Miri
• DR.CHECKER

License

See LICENSE and licenses