Bug discovery has long been a key concern in the field of software security.
Bugs are plentiful and many impact security. When bugs are discovered and fixed,
the underlying risk is mitigated. A wide variety of techniques exist from formal
verification over symbolic execution to fuzzing.
Out of those techniques, formal verification gives the highest of guarantees as
it proves correctness of the underlying code but only scales to a few thousand
lines of code. Symbolic execution abstracts code into formulas and uses a solver
to validate correctness of individual paths. Due to the exponential explosion of
evaluated paths, symbolic execution quickly reaches its limits as well.
Fuzzing, especially coverage-guided fuzzing, uses coverage feedback with simple
random mutation to "guide" execution towards rarely executed code areas.
In the last 10 years, fuzzing has dominated through its simplicity and
effectiveness. It's easy to configure and finds a lot of bugs.
In this research, we challenged the dominate of fuzzing by looking at concolic
execution. Concolic execution is a special form of symbolic execution that ties
the symbolic evaluation to individual paths, thereby limiting the exponential
explosion of paths and enabling some reasoning.
In past research, concolic execution and fuzzing have been combined with the
goal of leveraging the advantages of both systems: fuzzing to quickly iterate
and explore code areas (with iterations of thousands of executions per second)
combined with concolic execution to get past hard constraints and blocking code
paths. The idea was simple: whenever the fuzzer is stuck, the concolic engine
creates a proof-of-concept input that allows the fuzzer to break through this
limitation. Unfortunately, the lack of shared state between the fuzzer and the
concolic/symbolic engine resulted in a lot of lost computation to "recover" the
necessary state.
In our SymCTS we revisit the
design of independent concolic executors and introduce a more fine-grained
coverage metric (based on edge-dependence coverage) and a fine-grained mutator
that allows us better select uncovered code areas. The motivation behind our
work is simple: we discovered that fuzzers often get locked in code areas due to
early randomness. For example, a simple check early in the parser may decide
what functionality is executed later in the program. The fuzzer may chose one of
the two and, due to the following exploration, reach a lot of coverage in one
functionality which completely oppresses the other functionality. Even if the
fuzzer randomly selects the other functionality, coverage
from a single run is not sufficient to signal that this area is interesting.
In SymCTS, we apply a "fuzzing" approach to concolic execution, enabling us to
select interesting paths using edge-dependence coverage. Instead of storing
coverage counts per branch, we focus on pairs of branches. For each branch pair
in the program, we store the minimum and maximum number of times that one branch
gets executed if the other branch is executed as well. This edge-dependence
coverage matrix then helps us to prioritize inputs that cover a given area more
often as long as the other region is still covered. This dependence relationship
between code areas allows us to resolve the earlier mentioned challenge that
fuzzers miss. In addition, we also tune the scheduler to bias execution towards
under-fuzzed areas.
In the evaluation, we demonstrate the effectiveness of our approach on a set of
benchmarks including UniFuzz by comparing against symbolic execution and fuzzing
frameworks. While SymCTS is not a catch-all solution, it highlights how a
concolic engine can select code areas that are under-explored and may be missed
if general purpose fuzzing has captured nearby areas.
Lukas Dresel was the main author behind this work with help from many folks at
the SecLab at UCSB. They deserve most of the credit.