Technical Summary: LEAF – An Instrumentation-based Dynamic Analysis Framework for Rust

Problem Statement

Despite Rust's rapid adoption as a safe programming language, its ecosystem for program analysis tools remains in an early stage. While Rust has strong support for linting, fuzzing, bounded model checking, and deductive verification, it lacks a general-purpose dynamic analysis framework. Existing frameworks for other languages (e.g., DynaPyt for Python, Wasabi for WebAssembly, DiSL for Java) or lower-level binaries (e.g., Pin, DynamoRIO) cannot be directly applied to Rust. These tools either operate at the binary level or lack abstractions that expose Rust-specific language semantics, such as the ownership model, lifetimes, and strict memory access rules. Consequently, developers building dynamic analyses for Rust (e.g., taint analysis, symbolic execution, sanitizers) must reconstruct these high-level semantics from low-level representations, which is error-prone and limits expressiveness.

Methodology

The paper presents LEAF (Language-Enhanced Analysis Framework), an instrumentation-based dynamic analysis framework designed specifically for Rust. LEAF addresses the gap by capturing Rust's rich semantic information at the Mid-level Intermediate Representation (MIR) level and delivering it to analyses as an event stream augmented with runtime facts.

Core Design: Dynamic MIR (DMIR)

The central interface of LEAF is Dynamic MIR (DMIR), an event-driven programming interface.

• Event Stream: DMIR presents program execution as a stream of events corresponding to MIR constructs (assignments, function calls, branches, drops, borrows, etc.).
• Semantic Preservation: Unlike binary-level tracers, DMIR events preserve Rust-level semantics. For instance, an assignment event explicitly distinguishes between a simple write, a move, a mutable borrow, or an immutable borrow.
• Runtime Augmentation: While MIR is a static compile-time representation, DMIR augments these static constructs with runtime facts (e.g., concrete types for generics, actual memory addresses, specific branch outcomes, and concrete function targets).
• Callbacks: Analysis developers implement callbacks (e.g., AssignmentHandler, CallHandler) to process these events. The framework passes both the MIR structure (e.g., place projections, operand types) and the observed runtime values to these callbacks.

Implementation Techniques

LEAF is implemented as an extension to the Rust compiler (leafc), which inserts instrumentation probes into the MIR. Key technical challenges and solutions include:

1. Information Collection (Probes): LEAF inserts probes at MIR execution points. To manage overhead and complexity, it employs five techniques:
   • Specialized Probes: Using distinct probes for different event variants to avoid passing irrelevant arguments.
   • Merged Probes: Combining related events (e.g., atomic intrinsics) into single probes with an event-type argument.
   • Compositional Construction: Building complex MIR structures (like places involving dereferences and field projections) via helper calls that return temporary handles, rather than passing full structures directly.
   • Static References: Storing large data (like type layouts) in compile-time databases and passing only numeric IDs through probes.
   • Inlining and Encoding: Encoding frequent, simple constructs (like local variables without projections) directly into handles to avoid helper call overhead.
2. Information Delivery (Adapter): A Probe-to-DMIR Adapter (PDA) bridges the gap between low-level probe data and the structured DMIR event stream. It decodes compressed values, resolves temporary handles, and reconstructs the full DMIR event structure before invoking the analysis callback.
3. Handling Generics and Dynamic Dispatch: LEAF uses generic helper probes that are monomorphized alongside the code they instrument, ensuring concrete types are available at runtime. For dynamic dispatch (trait objects), it tracks the raw function address and method index.
4. Configurability: LEAF allows analyses to configure instrumentation rules (via instr_rules) to include or exclude specific entities (e.g., places, types, addresses) and code regions (e.g., local functions vs. dependencies). This is crucial for managing overhead.
5. Dependency Instrumentation: To ensure a complete event stream, LEAF forces the recompilation of dependency crates during the target build, applying instrumentation configurations specific to the current analysis.

Key Contributions

1. DMIR Interface: The design and implementation of an event-driven interface that delivers MIR-level semantics augmented with runtime facts to dynamic analyses.
2. Instrumentation Techniques: Novel techniques for capturing and delivering Rust semantic information (ownership, lifetimes, places) efficiently through compiler instrumentation.
3. Substantial Use Cases: Implementation of three complex dynamic analyses to demonstrate expressiveness:
   • Concolic Executor: A full concolic execution engine (11,749 LOC) using the Z3 SMT backend, capable of tracking symbolic expressions through Rust-specific operations like slices and enums.
   • ManuallyDrop Sanitizer: A tool (1,746 LOC) detecting use-after-drop and double-drop errors in programs using ManuallyDrop, leveraging ownership events and shadow memory.
   • Control-Flow Tracer: A lightweight tracer (646 LOC) demonstrating that full control-flow tracing can be achieved with minimal code using LEAF's built-in capabilities.
4. Empirical Evaluation: A comprehensive evaluation of LEAF's compile-time and runtime overhead across eight popular Rust crates and the Rust compiler benchmark suite.

Results

The evaluation quantifies the costs of exposing rich MIR-level information:

• Compilation Overhead: Instrumentation significantly increases compilation time and binary size, particularly for large crates and comprehensive configurations.
  • Under the "MB" configuration (all MIR events except lifetimes), release builds saw compilation time increases up to 72.4x (average ~11.5x) and binary size increases up to 33.0x (average ~4.2x).
  • Configurations including concrete types (+T) and raw addresses (+A) further increased overhead.
  • Selective instrumentation (e.g., local functions only) significantly reduced these costs.
• Runtime Overhead: The runtime cost of executing probes and delivering events is substantial but consistent with other dynamic analysis tools operating at high semantic levels.
  • Using the "MB" configuration, runtime slowdown ranged from 19x to 396x across benchmarks.
  • Adding concrete type information increased overhead by an average of 3.5x, and raw place addresses by 2.8x.
  • LEAF's overhead is comparable to or lower than tools like Miri (which showed 33x–163x higher overhead than LEAF's MB configuration in the same benchmarks) and other concolic execution systems targeting lower-level representations.
• Faithfulness: Across 29,652 test cases in the evaluated crates, instrumented programs passed their original test suites, with only two failures attributed to unsupported panic-handling customizations rather than behavioral divergence.

Significance

The paper claims that LEAF demonstrates that MIR is a practical foundation for Rust-specific dynamic analysis. By providing a framework that faithfully preserves Rust's ownership model, type system, and memory semantics at runtime, LEAF enables the development of complex, high-level dynamic analyses that would otherwise be infeasible or require reconstructing these semantics from lower-level representations. The framework proves that while the overhead of such rich instrumentation is meaningful, it is manageable through configurability, allowing developers to trade off analysis depth against performance costs. LEAF fills a critical gap in the Rust ecosystem, providing the reusable infrastructure necessary to advance dynamic analysis, fuzzing, and verification for the language.