From f9014007e6fa5c6519c1c2e163c5c6d144c45ea5 Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Fri, 3 Jan 2025 18:31:06 +0000 Subject: [PATCH 1/5] Add instructions for hybrid fuzzing --- docs/src/SUMMARY.md | 2 +- docs/src/user_guide/use_cases/fuzzing.md | 106 ++++++++++++++++++ .../user_guide/use_cases/hybrid_fuzzing.md | 3 - 3 files changed, 107 insertions(+), 4 deletions(-) create mode 100644 docs/src/user_guide/use_cases/fuzzing.md delete mode 100644 docs/src/user_guide/use_cases/hybrid_fuzzing.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 49809fd..11a2e31 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -7,7 +7,7 @@ - [Getting Started](./user_guide/getting_started.md) - [Use Cases](./user_guide/use_cases/section.md) - - [Hybrid Fuzzing](./user_guide/hybrid_fuzzing.md) + - [Fuzzing](./user_guide/use_cases/fuzzing.md) - [Configurations](./user_guide/configs.md) # Technical Reference diff --git a/docs/src/user_guide/use_cases/fuzzing.md b/docs/src/user_guide/use_cases/fuzzing.md new file mode 100644 index 0000000..7e2db14 --- /dev/null +++ b/docs/src/user_guide/use_cases/fuzzing.md @@ -0,0 +1,106 @@ +# Fuzzing + +One of the effective use cases of concolic execution is demonstrated to be +hybrid fuzzing, where fuzzing is aided with solver-found inputs generated by symbolic +execution to take certain paths inside the program that other techniques are inefficient +to find. + +Leaf is designed to be easy to integrate within existing stacks and +comes with a built-in support for [LibAFL][1], +a customizable fuzzing framework with modern architecture written in Rust. + +Crate `libafl_leaf` contains facilities for using Leaf-instrumented +programs with the fuzzers written using this library. + +## Hybrid Fuzzing for libFuzzer + +In an abstract manner, hybrid fuzzing for LibAFL-based fuzzers is achievable using +a stage that generates diverging inputs from the current test case. +This stage should perform the concolic execution using the current test case to derive the diverging inputs +and offer them to the fuzzer for evaluation. +Thus, the following steps are presumable for an execution-based concolic executor like Leaf. +1. Build an executable equivalent to the fuzz target, which is suitable for concolic execution. +1. Define a mutator stage that runs the built executable and obtains new inputs. +1. Add the stage to the fuzzer. + +The mentioned ingredients are provided by Leaf. +`leafc` instruments your target program, +`leafo_onetime` helps with collecting the diverging inputs, +and `libafl_leaf` provides the stage. +As `libFuzzer` (through `cargo-fuzz`) is one the most-used to perform fuzzing +for Rust projects, a rudimentary built-in support is also provided for harnesses +written based on [libfuzzer-sys](https://github.com/rust-fuzz/libfuzzer) +to upgrade them to a hybrid fuzzer. +It is developed as extension of [LibAFL][1]'s implementation of `libFuzzer`, so +the [same instructions](https://github.com/AFLplusplus/LibAFL/tree/main/libafl_libfuzzer) applies +for the integration. + +### Recipe + +With an understanding of the general procedure above, you can follow the instruction +below to upgrade your existing fuzzer to a hybrid one. + +* Prerequisites + 1. The one-time orchestrator is installed in your environment. + If not, install it similarly to `leafc` using the following command in Leaf's root folder. + ```console + leaf$ cargo install --path ./orchestrator + ``` + + 1. You already have a fuzzer written using `libfuzzer-sys` like below. + We assume it is named as `fuzz_target_1` in the instructions. + ```rust + #![no_main] + + use libfuzzer_sys::fuzz_target; + + fuzz_target!(|data: &[u8]| { + // fuzzed code goes here + }); + ``` + +1. Replace `libfuzzer-sys` source to Leaf's implementation in `Cargo.toml` of your fuzz project. + ```toml + # From + libfuzzer-sys = { version = "...", features = ["your", "features", "here"] } + + # To + libfuzzer-sys = { git = "https://github.com/sfu-rsl/leaf.git", package = "libafl_libfuzzer", features = ["your", "features", "here"]} + ``` + +1. Change `fuzz_target` macro invocation to `hybrid_fuzz_target` and make + `no_main` attribute conditional based on compilation with `leafc`. + ```rust + #![cfg_attr(not(leafc), no_main)] + + use libfuzzer_sys::hybrid_fuzz_target; + + hybrid_fuzz_target!(|data: &[u8]| { + // fuzzed code goes here + }); + ``` + (`hybrid_fuzz_target` generates a program with a `main` function that reads + the whole standard input, marks it as symbolic, and passes to the closure.) + +1. Build your fuzz target with `leafc` in a *separate* cargo target directory like below. + ```console + fuzz$ RUSTC=leafc cargo build --bin fuzz_target_1 --target-dir ./target/leaf + ``` + +1. Build your fuzzer normally, e.g., + ```console + fuzz$ cargo fuzz build fuzz_target_1 + ``` + +1. Run your fuzzer with the additional argument `conc_program` which points to the + instrumented executable built using `leafc`. + ```console + fuzz$ cargo fuzz run fuzz_target_1 -- -conc_program=./target/leaf/debug/fuzz_target_1 + ``` + +----------------- + +Please refer to the technical documentation for further details about the components and steps mentioned above. + + +[1]: https://github.com/AFLplusplus/LibAFL \ No newline at end of file diff --git a/docs/src/user_guide/use_cases/hybrid_fuzzing.md b/docs/src/user_guide/use_cases/hybrid_fuzzing.md deleted file mode 100644 index 37107ed..0000000 --- a/docs/src/user_guide/use_cases/hybrid_fuzzing.md +++ /dev/null @@ -1,3 +0,0 @@ -# Hybrid Fuzzing - -(TBD) \ No newline at end of file From ba2a922514cab774173c5ec5b6bdaeedf47dba4c Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Fri, 3 Jan 2025 18:45:20 +0000 Subject: [PATCH 2/5] Rename use cases to recipes Also, Improve wording for the fuzzing page --- docs/src/SUMMARY.md | 4 +-- .../{use_cases => recipes}/fuzzing.md | 34 +++++++++---------- docs/src/user_guide/recipes/section.md | 3 ++ docs/src/user_guide/use_cases/section.md | 3 -- 4 files changed, 21 insertions(+), 23 deletions(-) rename docs/src/user_guide/{use_cases => recipes}/fuzzing.md (75%) create mode 100644 docs/src/user_guide/recipes/section.md delete mode 100644 docs/src/user_guide/use_cases/section.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 11a2e31..88ed165 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -6,8 +6,8 @@ # User Guide - [Getting Started](./user_guide/getting_started.md) -- [Use Cases](./user_guide/use_cases/section.md) - - [Fuzzing](./user_guide/use_cases/fuzzing.md) +- [Recipes](./user_guide/recipes/section.md) + - [Fuzzing](./user_guide/recipes/fuzzing.md) - [Configurations](./user_guide/configs.md) # Technical Reference diff --git a/docs/src/user_guide/use_cases/fuzzing.md b/docs/src/user_guide/recipes/fuzzing.md similarity index 75% rename from docs/src/user_guide/use_cases/fuzzing.md rename to docs/src/user_guide/recipes/fuzzing.md index 7e2db14..cd491c2 100644 --- a/docs/src/user_guide/use_cases/fuzzing.md +++ b/docs/src/user_guide/recipes/fuzzing.md @@ -1,16 +1,14 @@ # Fuzzing -One of the effective use cases of concolic execution is demonstrated to be -hybrid fuzzing, where fuzzing is aided with solver-found inputs generated by symbolic +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 to find. -Leaf is designed to be easy to integrate within existing stacks and -comes with a built-in support for [LibAFL][1], +Leaf is aimed to be suitable for this purpose and comes with a built-in support for [LibAFL][1], a customizable fuzzing framework with modern architecture written in Rust. - -Crate `libafl_leaf` contains facilities for using Leaf-instrumented -programs with the fuzzers written using this library. +Crate `libafl_leaf` contains facilities for using Leaf-instrumented programs with +the fuzzers written using this library. ## Hybrid Fuzzing for libFuzzer @@ -23,17 +21,17 @@ Thus, the following steps are presumable for an execution-based concolic executo 1. Define a mutator stage that runs the built executable and obtains new inputs. 1. Add the stage to the fuzzer. -The mentioned ingredients are provided by Leaf. +The mentioned ingredients are provided by Leaf; `leafc` instruments your target program, `leafo_onetime` helps with collecting the diverging inputs, and `libafl_leaf` provides the stage. -As `libFuzzer` (through `cargo-fuzz`) is one the most-used to perform fuzzing -for Rust projects, a rudimentary built-in support is also provided for harnesses +As `libFuzzer` (through `cargo-fuzz`) is one the most-used tools to perform fuzzing +for Rust projects, a rudimentary support is also provided for harnesses written based on [libfuzzer-sys](https://github.com/rust-fuzz/libfuzzer) to upgrade them to a hybrid fuzzer. -It is developed as extension of [LibAFL][1]'s implementation of `libFuzzer`, so -the [same instructions](https://github.com/AFLplusplus/LibAFL/tree/main/libafl_libfuzzer) applies -for the integration. +It is developed as an extension of [LibAFL][1]'s implementation of `libFuzzer`, so +the [same instructions and options](https://github.com/AFLplusplus/LibAFL/tree/main/libafl_libfuzzer) +apply. ### Recipe @@ -41,14 +39,14 @@ With an understanding of the general procedure above, you can follow the instruc below to upgrade your existing fuzzer to a hybrid one. * Prerequisites - 1. The one-time orchestrator is installed in your environment. + 1. The one-time orchestrator (`leafo_onetime`) is installed in your environment. If not, install it similarly to `leafc` using the following command in Leaf's root folder. ```console leaf$ cargo install --path ./orchestrator ``` - 1. You already have a fuzzer written using `libfuzzer-sys` like below. - We assume it is named as `fuzz_target_1` in the instructions. + 1. You have a fuzzer written using `libfuzzer-sys`. + We assume it is named `fuzz_target_1` and has the following template. ```rust #![no_main] @@ -68,7 +66,7 @@ below to upgrade your existing fuzzer to a hybrid one. libfuzzer-sys = { git = "https://github.com/sfu-rsl/leaf.git", package = "libafl_libfuzzer", features = ["your", "features", "here"]} ``` -1. Change `fuzz_target` macro invocation to `hybrid_fuzz_target` and make +1. Change `fuzz_target` macro invocation to `hybrid_fuzz_target`, and make `no_main` attribute conditional based on compilation with `leafc`. ```rust #![cfg_attr(not(leafc), no_main)] @@ -79,7 +77,7 @@ below to upgrade your existing fuzzer to a hybrid one. // fuzzed code goes here }); ``` - (`hybrid_fuzz_target` generates a program with a `main` function that reads + (`hybrid_fuzz_target` additionally writes a program with a `main` function that reads the whole standard input, marks it as symbolic, and passes to the closure.) 1. Build your fuzz target with `leafc` in a *separate* cargo target directory like below. diff --git a/docs/src/user_guide/recipes/section.md b/docs/src/user_guide/recipes/section.md new file mode 100644 index 0000000..62b1c99 --- /dev/null +++ b/docs/src/user_guide/recipes/section.md @@ -0,0 +1,3 @@ +# Recipes + +(TBD) \ No newline at end of file diff --git a/docs/src/user_guide/use_cases/section.md b/docs/src/user_guide/use_cases/section.md deleted file mode 100644 index 4010394..0000000 --- a/docs/src/user_guide/use_cases/section.md +++ /dev/null @@ -1,3 +0,0 @@ -# Use Cases - -(TBD) \ No newline at end of file From 9ac6e77ba3567475cf01e67e453720f30289c369 Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Fri, 3 Jan 2025 18:47:01 +0000 Subject: [PATCH 3/5] Add a recipe for cargo --- docs/src/SUMMARY.md | 1 + docs/src/user_guide/recipes/cargo.md | 13 +++++++++++++ 2 files changed, 14 insertions(+) create mode 100644 docs/src/user_guide/recipes/cargo.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 88ed165..bb165c0 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -7,6 +7,7 @@ - [Getting Started](./user_guide/getting_started.md) - [Recipes](./user_guide/recipes/section.md) + - [Building Cargo Packages](./user_guide/recipes/cargo.md) - [Fuzzing](./user_guide/recipes/fuzzing.md) - [Configurations](./user_guide/configs.md) diff --git a/docs/src/user_guide/recipes/cargo.md b/docs/src/user_guide/recipes/cargo.md new file mode 100644 index 0000000..af37d75 --- /dev/null +++ b/docs/src/user_guide/recipes/cargo.md @@ -0,0 +1,13 @@ +# Building Cargo Packages + +As mentioned before, you can look at `leafc` as a wrapper around `rustc` and +it should be work in any command using `rustc`. + +Building packages is no exception. As supported by `cargo` you can set +[`build.rust`](https://doc.rust-lang.org/cargo/reference/config.html#buildrustc) configuration key +to override the compiler. +```bash +$ export RUSTC=leafc +$ cargo build +``` + From 2c52e89e6be802b3ad48fc738174556cec5474d2 Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Fri, 3 Jan 2025 19:54:21 +0000 Subject: [PATCH 4/5] Add a page for diverging input generation --- docs/src/SUMMARY.md | 1 + docs/src/user_guide/recipes/div_input.md | 39 ++++++++++++++++++++++++ 2 files changed, 40 insertions(+) create mode 100644 docs/src/user_guide/recipes/div_input.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index bb165c0..cfde25d 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -8,6 +8,7 @@ - [Getting Started](./user_guide/getting_started.md) - [Recipes](./user_guide/recipes/section.md) - [Building Cargo Packages](./user_guide/recipes/cargo.md) + - [Diverging Input Generation](./user_guide/recipes/div_input.md) - [Fuzzing](./user_guide/recipes/fuzzing.md) - [Configurations](./user_guide/configs.md) diff --git a/docs/src/user_guide/recipes/div_input.md b/docs/src/user_guide/recipes/div_input.md new file mode 100644 index 0000000..0c684fe --- /dev/null +++ b/docs/src/user_guide/recipes/div_input.md @@ -0,0 +1,39 @@ +# Diverging Input Generation + +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 +determines the target of the branch. +Therefore, concolic execution can be used to find concrete values for the symbolic variables +such that the execution diverges at conditional branches compared to the previous execution. +We refer to these concrete values as diverging inputs, counterexamples, or generally answers. + +The current default configuration of Leaf tries to find a diverging input whenever +a new constraint is observed. +For instance, in the following program, the input (`x = 10`) does not satisfy +the branch condition (`x < 5`), which the backend reports as `{!(<(, 5u8))}`. +It tries to find an input that would satisfy it (so the execution would diverge at this point), +and reports back value `0u8` as a possible one. + +## Diverging Standard Input Generation + +If all symbolic variables are from `u8`, the default configuration puts the found answers +in binary files in which each byte corresponds to a symbolic variable ordered by +when they were marked as symbolic. + +This is mainly meant for situations where we want to mark a file symbolic, e.g., standard input. + +Although the backend (and execution of the instrumented program) is enough to obtain the diverging standard input, +the one-time orchestrator is provided to facilitate this process with further control. + +You can install it by running the following command in Leaf's root folder. +```console +leaf$ cargo install --path ./orchestrator +``` +Then you provide the path to the instrumented program and the desired path to put the diverging inputs at. +For example, +```console +$ leafo_onetime --program ./hello_world --outdir ./next +next/diverging_0.bin +``` +It runs the target program, and prints the names of the files generated as diverging input. From 9683260548f788044127e27e1ed42c59fe07f946 Mon Sep 17 00:00:00 2001 From: Mohammad Omidvar Date: Sat, 4 Jan 2025 00:46:54 +0000 Subject: [PATCH 5/5] Add pure concolic testing to the book --- docs/src/user_guide/recipes/div_input.md | 25 ++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/docs/src/user_guide/recipes/div_input.md b/docs/src/user_guide/recipes/div_input.md index 0c684fe..8af06b4 100644 --- a/docs/src/user_guide/recipes/div_input.md +++ b/docs/src/user_guide/recipes/div_input.md @@ -37,3 +37,28 @@ $ leafo_onetime --program ./hello_world --outdir ./next next/diverging_0.bin ``` It runs the target program, and prints the names of the files generated as diverging input. + + +## Pure Concolic Testing + +By repeating the above procedure for each generated input, more possible paths +in the target program will be covered. We use the term *pure concolic* testing, +as used by [SymCC](https://github.com/eurecom-s3/symcc) for this method of testing. + +If you are interested in finding possible crashes in your program using pure concolic testing, +the project comes with a utility named `leaff_pure_conc`, which runs the loop for programs and captures those that cause a crash +in them. Currently, it only supports programs with symbolic standard input (uses the one-time orchestrator). + +To run pure concolic testing loop for a target: +1. Install the tool. + ```console + leaf$ cargo install --path ./integration/libafl/fuzzers/pure_concolic + ``` +1. Build your program with `leafc`. +1. Pass the executable path to the tool. e.g., + ```console + $ leaff_pure_conc --conc-program ./hello_world + ``` +1. The loop stops if no more new distinct input is found to be given to the program (can possibly run forever). + +We recommend looking at the options available for tuning the loop by passing `--help`.