Add pages for pure concolic and hybrid fuzz testing (#3)

* Add instructions for hybrid fuzzing

* Rename use cases to recipes

Also, Improve wording for the fuzzing page

* Add a recipe for cargo

* Add a page for diverging input generation

* Add pure concolic testing to the book

docs/src/SUMMARY.md

@@ -6,8 +6,10 @@
 # User Guide
 
 - [Getting Started](./user_guide/getting_started.md)
-- [Use Cases](./user_guide/use_cases/section.md)
-    - [Hybrid Fuzzing](./user_guide/hybrid_fuzzing.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)
 
 # Technical Reference

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
+```
+

docs/src/user_guide/recipes/div_input.md

@@ -0,0 +1,64 @@
+# 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 `{!(<(<Var1: u8>, 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.
+
+
+## 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`.

docs/src/user_guide/recipes/fuzzing.md

@@ -0,0 +1,104 @@
+# Fuzzing
+
+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 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.
+
+## 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 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 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
+
+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 (`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 have a fuzzer written using `libfuzzer-sys`.
+    We assume it is named `fuzz_target_1` and has the following template.
+        ```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` 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.
+    ```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

docs/src/user_guide/recipes/section.md

@@ -0,0 +1,3 @@
+# Recipes
+
+(TBD)