Automated run-time testing (or fuzzing) has always been the easiest and most efficient approach (given the time/number of vulnerabilities ratio) accounting for the largest share of discovered kernel vulnerabilities. We have seen several iterations of fuzzers: starting from "dumb" fuzzers to fuzzers guided by code coverage using genetic algorithms combined with compiler instrumentation. The latter approach has been successfully applied in practice resulting in dozens of previously undiscovered vulnerabilities. Even though this has been an advanced step from template-based fuzzing, there are still major shortcomings associated with this approach.
Static analysis, on the other hand, can achieve complete code coverage (in theory) by exploring all possible execution paths. In practice, this approach has significant drawbacks. The number of possible execution paths is exponential in the input size. Given the size and complexity of the kernel, most approaches based on static analysis would suffer from path/state explosion and generally introduce a large number of false positives.
Symbolic execution presents a middle ground between static analysis and run-time testing. It can cover a much larger execution space than run-time testing. The inherent problem associated with symbolic execution is that it can be very expensive: (1) a large set of possible program paths, (2) need to query the solver to decide which paths are feasible and which assertions could be false, and (3) a program state has many bits.
This presentation will start with an introduction to symbolic execution discussing the advantages and drawbacks associated with applying symbolic execution in kernel fuzzing. We will briefly cover available SMT/SAT solvers and existing kernel fuzzers based on symbolic execution and then move on to concolic testing, followed by our kernel fuzzer design and implementation.