Hybrid Fuzzing

Luca Borzacchiello

$ whoami

• Participant of 1st CyberChallenge.it (2017)
• 3rd year Ph.D. Student @ Sapienza
• Research interests:
• Program Analysis
• Symbolic Execution
• Fuzzing

Outline

1. Symbolic Execution
2. Concolic Execution
3. Fuzzing and Hybrid Fuzzing
4. Fuzzolic

Symbolic Execution

Symbolic Execution

Program analysis technique pioneered by J. C. King in 1976

Symbolic Execution

Key ideas:

• Each input in the program is associated with a symbol
• Each symbol represents a set of values
• Instructions in the program generates expressions

Program analysis technique pioneered by J. C. King in 1976

Symbolic Execution - Example Straight-line

int32_t foo(int32_t a) {

a = a + 10;

a = a * 2;

return a;

}

Symbolic Execution - Example Straight-line

int32_t foo(int32_t a) {

a = a + 10;

a = a * 2;

return a;

}

Symbolic Execution - Example Straight-line

int32_t foo(int32_t a) {

a = a + 10;

a = a * 2;

return a;

}

Symbolic Execution - Example Straight-line

int32_t foo(int32_t a) {

a = a + 10;

a = a * 2;

return a;

}

Symbolic Execution - Example Straight-line

int32_t foo(int32_t a) {

a = a + 10;

a = a * 2;

return a;

}

Easy! No branches!

Symbolic Execution - Example Branch

What happens at branches?

Symbolic Execution - Example Branch

What happens at branches?

int32_t abs(int32_t a) {

if (a > 0)

return a;

return -a;

}

Symbolic Execution - Example Branch

What happens at branches?

int32_t abs(int32_t a) {

if (a > 0)

return a;

return -a;

}

Symbolic Execution - Example Branch

What happens at branches?

int32_t abs(int32_t a) {

if (a > 0)

return a;

return -a;

}

The execution state is split in two states that models either outcome of the branch

Symbolic Execution - Example Branch

What happens at branches?

int32_t abs(int32_t a) {

if (a > 0)

return a;

return -a;

}

The execution state is split in two states that models either outcome of the branch

​

Each state has a path constraint that defines its condition of validity

Symbolic Execution - Symbolic Formulas

Now What?

Symbolic Execution - Symbolic Formulas

We can use an SMT Solver to reason on the generated formulas: e.g., we can check whether the dividend of a division can be zero

Now What?

[...]

return a / b;

SMT Solver

Is satisfiable?

32-bit bit-vectors

Symbolic Execution - Symbolic Formulas

We can use an SMT Solver to reason on the generated formulas: e.g., we can check whether the dividend of a division can be zero

Now What?

[...]

return a / b;

SMT Solver

Is satisfiable?

yes!

32-bit bit-vectors

Symbolic Execution - Example

​

Symbolic Execution can find all the inputs that makes the assertion at line 8 fail

image credit

Symbolic Execution - Final Remarks

In general, pure static symbolic execution hardly scales on real-world programs:

• Path explosion
• Hard-to-solve constraints
• Symbolic memory accesses
• Emulation time
• …

Static symbolic executors:

Concolic Execution

Concolic Execution

Dynamic flavor of symbolic execution (concrete + symbolic)

Key idea:

• Choose a concrete path (i.e., an input for the program)
• Run concretely the program
• Build symbolic expressions alongside concrete values
• Check conditions on the chosen path

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

concrete value (seed)

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

We can use the negated branch condition to generate a new input that covers the other outcome of the branch

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

Concolic Execution - Example

int32_t foo(int32_t a) {

a = a + 1;

if (a > 5)

if (a < 8)

a = a / 2;

return a;

}

Concolic Execution - Final Remarks

Pros wrt static symbolic execution

• No need to call the solver at branches if we are not interested in generating a new input: less queries
• The implementation can be very fast if we compile the instrumentation (e.g., using LLVM, PIN, QEMU)

Cons wrt static symbolic execution

• To explore a branch that is not taken by the seed, you need to re-execute from the beginning

NOTE: path explosion is still an issue!

Hybrid Fuzzing

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application

​

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application

very effective in practice

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application
• Very effective in practice...

very effective in practice

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application
• Very effective in practice...

very effective in practice

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application
• Very effective in practice...

very effective in practice

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application
• Very effective in practice...

very effective in practice

Fuzzing

• State-of-the-art technique for automatic test-case generation and vulnerability detection
• Based on random mutations of a pool of inputs with the goal of finding crashes in the target application
• Very effective in practice...

very effective in practice

Fuzzing

Still, it has some drawbacks:

• Struggles in overcoming checks against magic numbers or checksums (road-blocks)
• Typically needs a reasonable set of input seeds

Fuzzing

Still, it has some drawbacks:

• Struggles in overcoming checks against magic numbers or checksums (road-blocks)
• Typically needs a reasonable set of input seeds

Can we combine fuzzing and symbolic execution to take the best from the two worlds?

Fuzzing vs Symbolic Execution

Driller

First work (2016) on fuzzing improved with concolic execution

Key Ideas:

• Launch the fuzzer (AFL) for some time
• When the fuzzer get stuck (i.e., is unable to generate a new input), run the concolic executor and trying to generate a new input

Issues:

• The concolic executor is slow (interpreted, and written in python)
• The interaction between the fuzzer and the concolic executor is coarse grained

QSYM

Hybrid fuzzer and concolic executor based on Intel PIN (2018)

Key Ideas:

• JIT the instrumentation at runtime using PIN (no interpretation)
• The concolic executor runs in parallel with the fuzzer
• Optimizations: linearization and optimistic solving

QSYM - Parallel Setup

Input queue A

Fuzzer�[master]

Fuzzer�[slave]

QSYM

Input queue B

load/store

load/store

load

store

two-way synchronization

one-way synchronization

one-way synchronization

Input queue C

SymCC

Hybrid fuzzer and concolic executor based on LLVM (2020)

Key Ideas:

• Very fast instrumentation added at compilation time with an LLVM pass
• Parallel setup (as in QSYM)
• Function models to inject symbolic data
• Requires source code and recompilation of all components (or misses symbolic propagation)

Fuzzolic

Fuzzolic

Fast concolic executor based on QEMU (JIT-ed instrumentation)

• Developed independently and in parallel with SymQEMU (another concolic executor based on QEMU)
• Same parallel setup of QSYM
• Two solver backends:
• Z3 SMT solver
• FuzzySAT: approximate solver

Tracer�(QEMU)

Solver�Frontend

Query Pool

Expression Pool

Shared Memories

Solver�Backend

QEMU - JIT Workflow

(a)�Next basic block to execute is in cache?

(b)�JIT compilation of the basic block, then�add it to cache

(c)�Execute basic block �from the cache

YES

NO

THEN

THEN

Note: during JIT compilation, QEMU translate native code to the intermediate language TCG

Fuzzolic - Instrumentation

Fuzzolic instruments the program in TCG

Fuzzolic - Instrumentation

Two instrumentation methods:

• Inline instrumentation (simplified)

​

​

​

mov rbx, rax

x64

Fuzzolic - Instrumentation

Two instrumentation methods:

• Inline instrumentation (simplified)

​

​

​

mov rbx, rax

x64

mov_i64 tcg_reg_rbx, tcg_reg_rax

tcg

Fuzzolic - Instrumentation

Two instrumentation methods:

• Inline instrumentation (simplified)

​

​

​

mov rbx, rax

x64

mov_i64 tcg_reg_rbx, tcg_reg_rax

tcg

mov_i64 tcg_sym_reg_rbx, tcg_sym_reg_rax

mov_i64 tcg_reg_rbx, tcg_reg_rax

instrumented (inline)

Fuzzolic - Instrumentation

Two instrumentation methods:

• Inline instrumentation (simplified)

​

​

​

• Helper instrumentation (simplified)

mov rbx, rax

x64

mov_i64 tcg_reg_rbx, tcg_reg_rax

tcg

mov_i64 tcg_sym_reg_rbx, tcg_sym_reg_rax

mov_i64 tcg_reg_rbx, tcg_reg_rax

instrumented (inline)

call fuzzolic_mov_reg, tcg_sym_reg_rax, tcg_sym_reg_rbx

mov_i64 tcg_reg_rbx, tcg_reg_rax

instrumented (helper)

Fuzzolic - TCG Helpers

Unfortunately, while TCG is architecture-independent, it uses many helpers for particular instructions

• x86 is full of those helpers (e.g., vector instructions)

​

• Fuzzolic has hard-written models for some of those helpers, but many are missing (e.g., floating point instructions)

Fuzzy-SAT - An Approximate Solver

Key Ideas:

• Given a branch query of a concolic executor ( ), the seed that has driven the concolic exploration satisfies by design
• Fuzzing transformations has been proven effective in overcoming branch conditions
• While SMT solvers offer a rich set of solving primitives, most concolic executors (e.g., QSYM) are built on top of a few but essential primitives

​

Fuzzy-SAT - An Approximate Solver

​

Given a branch query and the seed, mutate the bytes of the seed trying to solve while keeping satisfiable.

​

​

Fuzzy-SAT Architecture

Fuzzy-SAT - An Approximate Solver

​

Given a branch query and the seed, mutate the bytes of the seed trying to solve while keeping satisfiable.

​

• Analysis: learn from the symbolic expressions added to

​

​

Fuzzy-SAT Architecture

Fuzzy-SAT - An Approximate Solver

​

Given a branch query and the seed, mutate the bytes of the seed trying to solve while keeping satisfiable.

​

• Analysis: learn from the symbolic expressions added to
• Reasoning: use the acquired knowledge to apply simple but fast transformations to the seed

​

​

​

Fuzzy-SAT Architecture

Fuzzy-SAT - Performance

Fuzzolic - Performance

DEMO

Thanks!

Questions?