From 6fdbdf85ca63853d5a07d0e721ae1221c4df5c6e Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Mon, 20 Jul 2026 13:15:26 +0000 Subject: [PATCH 1/3] Update top-level document --- README.md | 110 ++++++++++++++++++++++++------------------------------ 1 file changed, 49 insertions(+), 61 deletions(-) diff --git a/README.md b/README.md index 07ff847f..7d57ce78 100644 --- a/README.md +++ b/README.md @@ -1,54 +1,51 @@ # Leaf -Concolic execution for Rust through MIR instrumentation. - - -## Table of Contents -- [Getting Started](#getting-started) -- [Documentation](#documentation) - -## Getting Started -1. Clone the repository. -1. Install `leafc` using - ``` - cargo install --path ./compiler - ``` -1. Compile target programs using `leafc`, e.g., - ``` - leafc samples/hello_world.rs - ``` -1. Enable logging for Leaf's backend using `LEAF_LOG` environment variable. - ``` - export LEAF_LOG="info" - ``` -1. Run the compiled program. - ``` - hello_world - ``` -1. An output similar to the following is expected from the execution. - ```log - 2024-12-10 00:40:55 INFO leafrt Initializing runtime library - 2024-12-10 00:40:55 INFO leafrt::pri::basic::instance Initializing basic backend - 2024-12-10 00:40:55 INFO leafrt::backends::basic::outgen Setting up binary output writing to directory: output - 2024-12-10 00:40:55 INFO leafrt::pri::basic::instance Basic backend initialized - 2024-12-10 00:40:55 INFO leafrt::backends::basic::sym_vars Added a new symbolic variable: = 10u8 - 2024-12-10 00:40:55 INFO leafrt::trace::log Notified about constraint {!(<(, 5u8))} at step Def(0:5)[2] - 2024-12-10 00:40:55 INFO leafrt::outgen Found a solution: - { - "1": 0u8, - } - ``` - -This was a demonstration of the basic workflow to perform dynamic symbolic execution using Leaf. - -Leaf comes with a compiler (`leafc`) that instruments programs. -It is a wrapper around the Rust compiler and should be usable in any existing command -in place of `rustc`. -The instrumented program calls the backend during runtime, providing the information about the events inside the program -including the constraints on the variables for the path currently being taken. -By marking a variables of interest as symbolic, the system records the constraints on them, and later provides output -based on them, e.g., concrete values for them which cause the program take paths different from the current one. -For further information please refer to documentations. +Leaf is a Rust-oriented framework for dynamic analysis built around MIR instrumentation. It wraps the Rust compiler through `leafc`, instruments a program at compile time, and routes runtime events to pluggable backends for tracing, symbolic execution, and related analyses. + +## Project layout + +- `compiler/`: the `leafc` driver and instrumentation pipeline +- `runtime/lib`: the shared abstraction library for implementing runtime backends +- `runtime/backends/`: concrete backend implementations +- `common/`: shared facilities and definitions used across the project + +## Requirements + +- Rustup and cargo to install nightly toolchains, `rustc` libraries and building the project. +- Python for helper scripts (e.g., toolchain builder) in the repository + +## Quick start +1. Clone the repository and build the compiler: + ```console + $ git clone https://github.com/sfu-rsl/leaf.git + $ cd leaf + $ cargo install --path ./compiler + ``` + +1. Build a runtime backend, for example the control-flow tracer: + ```console + $ cargo build -p runtime_cf_tracer + ``` + +1. Make the shared library discoverable to the generated program: + ```console + $ mkdir -p target/debug/runtime_cf_tracer + $ ln -sf target/debug/runtime_cf_tracer.so target/debug/runtime_cf_tracer/libleafrt.so + $ export LD_LIBRARY_PATH="$PWD/target/debug/runtime_cf_tracer:$LD_LIBRARY_PATH" + ``` + +1. Compile a sample program with `leafc`: + ```console + $ leafc samples/hello_world.rs + ``` + +1. Run the instrumented binary with logging enabled: + ```console + $ export LEAF_LOG="info" + $ ./hello_world + ``` + +The generated program will emit runtime events through the active backend, which can be inspected through the logging output or any backend-specific artifacts. ## Documentation @@ -57,17 +54,8 @@ Further information, tutorials, and technical details are collected in Leaf Book ## License -Licensed under either of - - * Apache License, Version 2.0 - ([LICENSE-APACHE](LICENSE-APACHE) or http://www.apache.org/licenses/LICENSE-2.0) - * MIT license - ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT) - -at your option. +Leaf is licensed under the MIT or Apache-2.0 licenses. -## Contribution +- Apache License, Version 2.0: [LICENSE-APACHE](LICENSE-APACHE) +- MIT License: [LICENSE-MIT](LICENSE-MIT) -Unless you explicitly state otherwise, any contribution intentionally submitted -for inclusion in the work by you, as defined in the Apache-2.0 license, shall be -dual licensed as above, without any additional terms or conditions. From 1b166a11c610aac236bafaca8635be38f56fa61e Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Mon, 20 Jul 2026 14:10:23 +0000 Subject: [PATCH 2/3] Update the book --- docs/src/leaf.md | 1 - docs/src/user_guide/getting_started.md | 158 +++++++++++------------ docs/src/user_guide/recipes/cargo.md | 4 + docs/src/user_guide/recipes/div_input.md | 3 + docs/src/user_guide/recipes/fuzzing.md | 3 + 5 files changed, 89 insertions(+), 80 deletions(-) diff --git a/docs/src/leaf.md b/docs/src/leaf.md index 1558599e..29b72533 100644 --- a/docs/src/leaf.md +++ b/docs/src/leaf.md @@ -2,7 +2,6 @@ Concolic execution for Rust through MIR instrumentation. Welcome to project Leaf, a tool to perform dynamic symbolic execution for Rust programs. -Leaf helps you with tracking the constraints put on particular variables of interest during the execution of the program. Leaf aims to be robust, extensible, and easily-integrable within real world Rust testing stacks. diff --git a/docs/src/user_guide/getting_started.md b/docs/src/user_guide/getting_started.md index 588c2548..80fe876d 100644 --- a/docs/src/user_guide/getting_started.md +++ b/docs/src/user_guide/getting_started.md @@ -1,91 +1,91 @@ # Getting Started -Although currently working with the first releases of Leaf, we aim to provide a rather straightforward workflow for the users. -Please follow the instruction below to try Leaf in your environment. +Leaf is a Rust-oriented framework for dynamic analysis built around MIR instrumentation. The workflow is: -## Installing Leaf +1. compile and instrument a target program with `leafc`, and +1. provide a runtime backend that receives callbacks from the instrumented program, +4. run the instrumented program with the backend plugged in. + +## Requirements -### Requirements -- Rust (`rustup`) +- Rust - Python +- A working C toolchain and linker -You can install Leaf using `cargo` and by building the source code. - -1. Clone the repository. - ```console - $ git clone https://github.com/sfu-rsl/leaf.git - $ cd leaf - ``` -1. Install Leaf's compiler named as `leafc` using - ```console - $ cargo install --path ./compiler - ``` -## Performing Concolic Execution -As an instrumentation-based dynamic analyzer, Leaf instruments programs such that -they expose information about their behavior during each execution. -Therefore, concolic execution is achieved by compiling the target program and -running the executable. - -1. Pick a program you want to do concolic execution for. Some are available in `samples` directory of the source tree. - ```rust - fn main() { - let x: u8 = 10; - if x < 5 { - println!("Hello, world!"); - } - } - ``` - -1. Mark a variable interest as symbolic. - ```rust - // samples/hello_world.rs - - use leaf::annotations::*; - fn main() { - let x: u8 = 10.mark_symbolic(); - if x < 5 { - println!("Hello, world!"); - } - } - ``` - -1. Compile your target program using `leafc` as you would do with `rustc`. (The first compilation takes longer, bear with it!) - ```console - $ leafc ./hello_world.rs - ``` - -1. Prepare the environment to observe the execution through the standard error - by setting `LEAF_LOG` variable. e.g., - ```bash - export LEAF_LOG="info" - ``` -1. Execute the compiled program. - ```console - $ ./hello_world - ``` -1. An output similar to the following is expected from the execution. - ```log - 2024-12-10 00:40:55 INFO leafrt Initializing runtime library - 2024-12-10 00:40:55 INFO leafrt::pri::basic::instance Initializing basic backend - 2024-12-10 00:40:55 INFO leafrt::backends::basic::outgen Setting up binary output writing to directory: output - 2024-12-10 00:40:55 INFO leafrt::pri::basic::instance Basic backend initialized - 2024-12-10 00:40:55 INFO leafrt::backends::basic::sym_vars Added a new symbolic variable: = 10u8 - 2024-12-10 00:40:55 INFO leafrt::trace::log Notified about constraint {!(<(, 5u8))} at step Def(0:5)[2] - 2024-12-10 00:40:55 INFO leafrt::outgen Found a solution: - { - "1": 0u8, +## Installing Leaf + +1. Clone the repository and enter the workspace. + ```console + $ git clone https://github.com/sfu-rsl/leaf.git + $ cd leaf + ``` + +1. Install the compiler frontend. + ```console + $ cargo install --path ./compiler + ``` + +## Preparing Dynamic Analysis + +1. Build a runtime backend, for example symbolic execution. + ```console + $ cargo build -p runtime_symex + ``` + +1. Make the runtime shared library discoverable to the instrumented binary. + ```console + $ mkdir -p target/debug/runtime_symex + $ ln -sf "$(find target/debug -maxdepth 1 -name 'libleafrt*.so' | head -n 1)" target/debug/runtime_symex/libleafrt.so + $ export LD_LIBRARY_PATH="$PWD/target/debug/runtime_symex:$LD_LIBRARY_PATH" + ``` + +## Analyzing a Program + +Leaf ships with sample programs under the `samples/` directory. A minimal example is the `hello_world` sample. +```rust +fn main() { + let x: u8 = core::hint::black_box(10); + #[cfg(leafc)] + let x: u8 = { + use leaf::annotations::*; + x.mark_symbolic() + }; + + if x < 5 { + println!("Hello, world!"); } - ``` - The logs include information about the constraints put on the variables marked as symbolic for the path taken in the execution. +} +``` -1. Given the current default configuration, a folder named `leaf_out` also gets generated - which contains alternative values for the symbolic variables that should cause - the execution take other paths than the one taken, which we call diverging inputs. +1. Compile the sample with `leafc`. ```console - $ ls ./leaf_out - 0.bin + $ leafc samples/hello_world.rs ``` ------------ +2. Enable logging for the runtime. + ```console + $ export LEAF_LOG="info" + ``` + +3. Run the generated binary. + ```console + $ ./hello_world + ``` + +You should see runtime events emitted by the active backend. The exact output depends on the chosen backend and logging configuration, but the execution should complete and produce instrumentation traces or analysis data. With the example symbolic execution backend in effect, an output similar to the following is expected. +```log +2024-12-10 00:40:55 INFO leafrt Initializing runtime library +2024-12-10 00:40:55 INFO leafrt::pri::basic::instance Initializing basic backend +2024-12-10 00:40:55 INFO leafrt::backends::basic::outgen Setting up binary output writing to directory: output +2024-12-10 00:40:55 INFO leafrt::pri::basic::instance Basic backend initialized +2024-12-10 00:40:55 INFO leafrt::backends::basic::sym_vars Added a new symbolic variable: = 10u8 +2024-12-10 00:40:55 INFO leafrt::trace::log Notified about constraint {!(<(, 5u8))} at step Def(0:5)[2] +2024-12-10 00:40:55 INFO leafrt::outgen Found a solution: +{ + "1": 0u8, +} +``` + +## Next steps -More details about each step is provided in the rest of the book. \ No newline at end of file +The rest of the book covers the compiler pipeline, runtime backends, and more advanced analysis workflows in greater detail. \ No newline at end of file diff --git a/docs/src/user_guide/recipes/cargo.md b/docs/src/user_guide/recipes/cargo.md index af37d759..944d4a5b 100644 --- a/docs/src/user_guide/recipes/cargo.md +++ b/docs/src/user_guide/recipes/cargo.md @@ -11,3 +11,7 @@ $ export RUSTC=leafc $ cargo build ``` +## Leaf's Modifications + +`leafc` is slightly specialized when used by cargo for compiling crate's dependencies. +(TODO) \ No newline at end of file diff --git a/docs/src/user_guide/recipes/div_input.md b/docs/src/user_guide/recipes/div_input.md index 8af06b4b..0a475f7a 100644 --- a/docs/src/user_guide/recipes/div_input.md +++ b/docs/src/user_guide/recipes/div_input.md @@ -1,5 +1,8 @@ # Diverging Input Generation +> [!IMPORTANT] +> This document is currently obsolete and will be removed with further developments of the book. The orchestrators mentioned in this tutorial are currently moved out of the project. + Each instance of concolic execution of a program, records a trace of the constraints put on symbolic variables at each step of the execution. Conditional branches are the major source of these constraints and whether they are held or not diff --git a/docs/src/user_guide/recipes/fuzzing.md b/docs/src/user_guide/recipes/fuzzing.md index cd491c2c..fd341a6d 100644 --- a/docs/src/user_guide/recipes/fuzzing.md +++ b/docs/src/user_guide/recipes/fuzzing.md @@ -1,5 +1,8 @@ # Fuzzing +> [!IMPORTANT] +> This document is currently obsolete and will be removed with further developments of the book. The orchestrators mentioned in this tutorial are currently moved out of the project. + One of the use cases of concolic execution, which is demonstrated to be effective, is hybrid fuzzing, in which fuzzing is aided with solver-found inputs generated by symbolic execution to take certain paths inside the program that other techniques are inefficient From d5f99b37293876542c44548d374ce2bccd824dcc Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Mon, 20 Jul 2026 13:37:11 +0000 Subject: [PATCH 3/3] Set license of the subpackages --- common/Cargo.toml | 3 ++- compiler/Cargo.toml | 1 + macros/Cargo.toml | 1 + runtime/backends/cf_tracer/Cargo.toml | 1 + runtime/backends/mdsan/Cargo.toml | 1 + runtime/backends/symex/Cargo.toml | 1 + runtime/flavors/cf_tracer/Cargo.toml | 1 + runtime/flavors/mdsan/Cargo.toml | 1 + runtime/flavors/noop/Cargo.toml | 1 + runtime/flavors/symex/Cargo.toml | 1 + runtime/flavors/symex_no_implicit/Cargo.toml | 1 + runtime/lib/Cargo.toml | 1 + 12 files changed, 13 insertions(+), 1 deletion(-) diff --git a/common/Cargo.toml b/common/Cargo.toml index c817b92d..bb5602e6 100644 --- a/common/Cargo.toml +++ b/common/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "common" +license = { workspace = true } version = { workspace = true } edition = "2021" @@ -69,5 +70,5 @@ z3-sys = { workspace = true, optional = true } unexpected_cfgs = { level = "warn", check-cfg = [ 'cfg(core_build)', 'cfg(info_db_fmt, values("json", "rkyv"))', - 'cfg(refs_inlining)' + 'cfg(refs_inlining)', ] } diff --git a/compiler/Cargo.toml b/compiler/Cargo.toml index 3ccad495..165dd43c 100644 --- a/compiler/Cargo.toml +++ b/compiler/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "compiler" +license = { workspace = true } version = { workspace = true } edition = "2024" diff --git a/macros/Cargo.toml b/macros/Cargo.toml index 91aa918a..3cb82c4a 100644 --- a/macros/Cargo.toml +++ b/macros/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "macros" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/backends/cf_tracer/Cargo.toml b/runtime/backends/cf_tracer/Cargo.toml index e90a725a..44a63118 100644 --- a/runtime/backends/cf_tracer/Cargo.toml +++ b/runtime/backends/cf_tracer/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_backend_cf_tracer" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/backends/mdsan/Cargo.toml b/runtime/backends/mdsan/Cargo.toml index ef921069..de842d39 100644 --- a/runtime/backends/mdsan/Cargo.toml +++ b/runtime/backends/mdsan/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_backend_mdsan" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/backends/symex/Cargo.toml b/runtime/backends/symex/Cargo.toml index 7c802366..df8f4fc9 100644 --- a/runtime/backends/symex/Cargo.toml +++ b/runtime/backends/symex/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_backend_symex" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/flavors/cf_tracer/Cargo.toml b/runtime/flavors/cf_tracer/Cargo.toml index 876ad6b9..5939ac70 100644 --- a/runtime/flavors/cf_tracer/Cargo.toml +++ b/runtime/flavors/cf_tracer/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_cf_tracer" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/flavors/mdsan/Cargo.toml b/runtime/flavors/mdsan/Cargo.toml index 0c976c98..b1d6acde 100644 --- a/runtime/flavors/mdsan/Cargo.toml +++ b/runtime/flavors/mdsan/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_mdsan" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/flavors/noop/Cargo.toml b/runtime/flavors/noop/Cargo.toml index 38fd20c5..985e6c2d 100644 --- a/runtime/flavors/noop/Cargo.toml +++ b/runtime/flavors/noop/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_noop" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/flavors/symex/Cargo.toml b/runtime/flavors/symex/Cargo.toml index d9ab7aad..54260def 100644 --- a/runtime/flavors/symex/Cargo.toml +++ b/runtime/flavors/symex/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_symex" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/flavors/symex_no_implicit/Cargo.toml b/runtime/flavors/symex_no_implicit/Cargo.toml index 74d86e81..50575ae6 100644 --- a/runtime/flavors/symex_no_implicit/Cargo.toml +++ b/runtime/flavors/symex_no_implicit/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime_symex_no_implicit" +license = { workspace = true } version = { workspace = true } edition = "2021" diff --git a/runtime/lib/Cargo.toml b/runtime/lib/Cargo.toml index 6e0817be..081fd0b0 100644 --- a/runtime/lib/Cargo.toml +++ b/runtime/lib/Cargo.toml @@ -1,5 +1,6 @@ [package] name = "runtime" +license = { workspace = true } version = { workspace = true } edition = "2021"