SYS-OSS/FRET-LibAFL
4
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Book: Explain SymCC constraint solving (follow up on #980) (#986)

Browse Source 
* Make the kind of solving more clear (follow up on #980)

* Update docs/src/advanced_features/concolic.md

Co-authored-by: julihoh <julihoh@users.noreply.github.com>

Co-authored-by: julihoh <julihoh@users.noreply.github.com>
This commit is contained in:
Dominik Maier 2023-01-05 11:51:31 +01:00 committed by GitHub
parent 7d412693c8
commit 1bb37e4b98
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
docs/src/advanced_features/concolic.md
View File

@ -1,4 +1,5 @@
# Concolic Tracing and Hybrid Fuzzing
LibAFL has support for concolic tracing based on the [SymCC](https://github.com/eurecom-s3/symcc) instrumenting compiler.
For those uninitiated, the following text attempts to describe concolic tracing from the ground up using an example.
@ -96,10 +97,10 @@ These callbacks allow the runtime to construct a trace that is similar to the pr
### SymCC and its Runtimes
SymCC ships with 2 runtimes:
SymCC ships with 2 runtimes:
* a 'simple' runtime that attempts to solve any branch conditions it comes across using [Z3](https://github.com/Z3Prover/z3/wiki) and
* a [QSym](https://github.com/sslab-gatech/qsym)-based runtime, which does a bit more filtering on the expressions and also solves them using Z3.
* A 'simple' runtime that attempts to negate and analytically solve any branch conditions it comes across using [Z3](https://github.com/Z3Prover/z3/wiki) and
* A [QSym](https://github.com/sslab-gatech/qsym)-based runtime, which does a bit more filtering on the expressions and also solves them using Z3.
The integration with LibAFL, however, requires you to **BYORT** (_bring your own runtime_) using the [`symcc_runtime`](https://docs.rs/symcc_runtime/0.1/symcc_runtime) crate.
This crate allows you to easily build a custom runtime out of the built-in building blocks or create entirely new runtimes with full flexibility.
@ -134,10 +135,12 @@ Check out the [example hybrid fuzzer's runtime](https://github.com/AFLplusplus/L
### Instrumentation
There are two main instrumentation methods to make use of concolic tracing in LibAFL:
* Using an **compile-time** instrumented target with **SymCC**.
* Using a **compile-time** instrumented target with **SymCC**.
This only works when the source is available for the target and the target is reasonably easy to build using the SymCC compiler wrapper.
* Using **SymQEMU** to dynamically instrument the target at **runtime**.
This avoids building a separate instrumented target with concolic tracing instrumentation and so does not require source code.
It should be noted, however, that the 'quality' of the generated expressions can be significantly worse and SymQEMU generally produces significantly more and significantly more convoluted expressions than SymCC.
Therefore, it is recommended to use SymCC over SymQEMU when possible.