DOCSEARCHbyAlgolia
Submit Docs

MIRAI Abstract Interpreter

repository·main·Indexed 42 days ago

https://github.com/endorlabs/mirai

A static analysis tool and abstract interpreter for the Rust compiler's Mid-level Intermediate Representation (MIR). MIRAI is used for finding panics, verifying correctness properties, and performing security analysis such as taint and constant-time analysis. It includes the `mirai-annotations` crate for formal verification via assume, precondition, postcondition, and verify macros, and is executed using the `cargo mirai` command.

Tokens
18K
Snippets
49
Records
97
Agent score
53%

What's inside MIRAI

  1. Use MIRAI annotations to assist formal verification

    main

    The mirai-annotations crate provides macros that replace standard Rust assert! and debug_assert! macros. These annotations allow the MIRAI formal verification tool to distinguish between path conditions and verification conditions, manage assumptions versus verifications, and perform expensive checks at compile time rather than runtime.

    There are four primary families of macros based on their logical role:

    1. assume: Conditions the verifier should treat as true.
    2. precondition: Conditions that must be true before a function executes (acts like assume for the caller).
    3. postcondition: Conditions that must be true after a function executes (acts like assume for the caller).
    4. verify: Conditions that the verifier must prove are true.

  2. How MIRAI models the heap

    main

    The heap is modeled as a set of (path, value) pairs.

    • Path: Resembles a MIR Place; it can be a reference, an index into a collection, or an offset from a pointer.
    • Value: Typically a representation of a primitive value, but can be a structured value that is unknown in the current environment.

    This sparse representation makes it feasible to use in function summaries, though it requires complex path canonicalization and weak updates to handle aliasing.

  3. Understand MIRAI's analysis target: MIR

    main

    MIRAI performs abstract interpretation over MIR (Mid-level Intermediate Representation). MIR is the last intermediate data structure produced by the Rust compiler before code generation.

    Analyzing MIR instead of source code or LLVM bitcode provides several benefits:

    • It removes complexity orthogonal to static analysis (like macro expansion).
    • It retains necessary information for name resolution and type analysis that is lost after code generation.
    • It allows the analyzer to use the compiler's own diagnostic services.

    However, users should be aware that MIR is unstable and its semantics can be complex, occasionally requiring the analyzer to maintain a parallel type system to handle abstractions that lose information during the compiler's lowering process.

  4. How MIRAI targets different programmer profiles

    main
    MIRAI is built to be accessible to all Rust programmers by default, rather than being restricted to the formal-methods community. However, it provides specialized options that can be used by security researchers, cryptologists, or other specialists who require higher levels of verification.

  5. How MIRAI's abstract interpreter works

    main

    MIRAI is an interpreter that operates on the Rust compiler's Mid-level Intermediate Representation (MIR). It functions as a symbolic execution engine, treating values as symbolic expressions.

    Key Components:

    • Abstract Values: Most values remain symbolic. MIRAI uses algebraic simplification to manage expression size and avoids expensive SMT solver calls (like Z3) whenever possible. Classical abstract domains (Interval and Tag domains) are computed on demand and cached.
    • Environment: The state of memory is modeled as a functional map from paths to values.
      • Paths: Represent ways to access memory locations (similar to MIR Place).
      • Values: Represent data (similar to MIR Operand).
      • Note: The environment does not store structured values; fields of a struct are stored as separate entries (e.g., p.a and p.b) to keep joins efficient.
    • Summaries: To avoid exponential complexity and handle recursion, MIRAI analyzes functions by computing and caching summaries instead of re-analyzing every call site. A summary includes:
      • Preconditions required to avoid panics.
      • An abstract return value.
      • A list of side-effects.
      • A post-condition.

  6. How MIRAI handles virtual function calls (Devirtualization)

    main

    MIRAI resolves calls to virtual functions by tracking the concrete types of argument values during the analysis of the caller. Once the concrete type is known, MIRAI obtains a specialized summary for that specific implementation of the virtual function.

    This process (devirtualization) makes the analysis of the caller more precise. It relies on the Rust compiler's query system to perform method resolution, which ensures accuracy but makes the analyzer sensitive to changes in the compiler's internal invariants.

  7. How the Expression Domain works

    main

    The Expression Domain is the most precise way to specify possible values by using the expression itself as the abstract value. Operations in this domain result in new expressions encoding operands and operators.

    Key Features

    • Path Sensitivity: MIRAI uses the Expression Domain to simplify conditional joins. For example, if a value results from if c { e1 } else { e2 } and the path context knows the value of c, the abstract value can be simplified directly to e1 or e2.
    • Heuristics and Theorem Proving: MIRAI uses tree pattern matching heuristics to answer questions about expressions. If heuristics fail, it can use a theorem prover like Z3 to attempt to find an answer, though this can make analyzer behavior non-deterministic.
    • Fallback Mechanism: If the Expression Domain cannot provide a precise answer, the analyzer projects the value onto a less precise domain (e.g., an Interval domain). To minimize false positives from these approximations, MIRAI can query a progression of increasingly precise domains and only issue warnings if they all agree.

  8. Understand the Symbolic Expression Domain and SMT solver usage

    main

    MIRAI uses a symbolic expression domain as its default abstract domain. This means the most precise way to represent what a value can be is the expression itself.

    SMT Solver (Z3) Integration

    When MIRAI needs to determine if an expression is satisfiable, it translates the expression into an SMT solver format and uses Z3 to query the result.

    Key behaviors to note:

    • Timeout: SMT solver queries are subject to a small timeout (typically 100 ms).
    • Non-determinism: Because Z3 is heuristic, solver queries can introduce non-determinism into the analysis.
    • Optimization: To mitigate the cost of translating expressions to Z3, MIRAI performs its own algebraic simplification and uses an interval domain (or tag domain) before resorting to an SMT query.

  9. Apply Graph Reductions to the Call Graph

    main

    Reductions are applied sequentially in the order they are listed in the reductions array. They help reduce graph size and complexity by excluding irrelevant nodes and edges.

    Supported reductions:

    1. {"Slice": "function_name"}: Returns a sub-graph containing only nodes reachable from the specified function.
    2. "Fold": Removes all nodes not belonging to the crates listed in included_crates. It preserves paths between included nodes by creating direct edges between them.
    3. "Deduplicate": Ensures at most one edge exists between any two nodes. This removes type information, making the graph better for visual inspection.
    4. "Clean": Removes orphan nodes (nodes with no incoming or outgoing edges).

  10. How MIRAI handles annotations and correctness assertions

    main
    MIRAI is designed to target the full Rust language. While it can analyze unannotated code by performing whole-program analysis and precondition inference, it allows for explicit correctness assertions and invariants via annotations. This hybrid approach means you can use MIRAI on existing codebases without requiring immediate widespread annotation, but you can also provide explicit annotations to improve precision and provide the prover with necessary assumptions.

  11. How MIRAI resolves indirect calls

    main

    Indirect calls (via function pointers or traits) require call-site information to resolve. MIRAI handles this through specialization and summary caching:

    • Trait Calls: If a receiver argument is a generic type that implements a trait, MIRAI queries the Rust compiler to find the specific method implementation for that type.
    • Function Pointers/Closures: If a higher-order function receives a function pointer or closure, MIRAI attempts to resolve the concrete function used at the call site. The summary cache is keyed by both the function ID and the call-site information to support this.
    • Limitations: Call resolution may fail if:
      • The callable is obtained from an iterator over an arbitrarily sized collection.
      • The analysis root itself is generic or contains a callable.
      • The callable is wrapped in an Option<T> where T is unknown.

    In cases where resolution is impossible, MIRAI attempts to infer preconditions that prevent the unresolvable code paths from being reached.

  12. Understand the purpose of MIRAI Standard Contracts

    main

    The mirai-standard-contracts crate provides function definitions that serve as summaries for parts of the Rust standard library.

    Note for Developers: This crate is not intended to be used as a library by other crates. Instead, it is a specialized source for the MIRAI tool. MIRAI runs over this crate to generate a database of summaries. This database is then bundled with the MIRAI binary and serves as the initial seed for the database created when MIRAI analyzes a new project.