A Solverless Symbolic Execution Engine
Automatic test generation is a crucial problem in computer science. It helps the developers in finding bugs (and vulnerabilities) early in the development, hopefully before release. The two main techniques used in this context are fuzzing and symbolic execution. Over the last two decades, both fuzzing and symbolic execution techniques have been extensively used both in academia and industry.
Fuzzing, in its simplest form, randomly mutates a set of seed inputs to generate new test cases, often using genetic algorithms. While it is very efficient and has been proven to be effective in generating test cases that cover a high percentage of the tested program, the technique struggles in bypassing checks against magic numbers and checksums.
Symbolic execution encodes the behavior of the program to first-order logic formulas and uses a satisfiability modulo theory (SMT) solver to reason about those formulas and generate new inputs (i.e., test cases) automatically. The main disadvantage of this technique lies in the difficulty that it has to scale on complex programs.
One crucial performance bottleneck in symbolic execution is the solver. The formulas built on paths of real-world applications may be arbitrary complex (e.g., due to a checksum), and the solver often struggles in trying to solve them.
The strength of fuzzers lies in their ability to produce test cases by mutating only a few bytes of the input: a small modification of the input is often sufficient to explore new code. This insight could be exploited in the context of symbolic execution: a small modification of the input may be sufficient to solve a query, without using an SMT solver.
The goal of this project is to devise a technique that can reason about SMT formulas, without using a solver. The idea is to trade accuracy (i.e., the technique cannot solve all queries) in exchange for better scalability.