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.