Automated run-time testing has always been the easiest and most efficient approach accounting for the largest share of discovered kernel vulnerabilities. We have seen several iterations of kernel fuzzers: starting from "dumb" fuzzers to fuzzers guided by code coverage. The latter approach, despite simplistic search algorithms, 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, code coverage can be further increased to discover interesting execution paths that trigger new internal states within the kernel.
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 and is more “sound” than dynamic testing. However, the inherent problem associated with symbolic execution is that it can be very expensive: (1) a large set of possible program paths, (2) large size of a program state and, (3) need to query the solver to decide which paths are feasible.
This talk will start with an introduction to symbolic execution and SMT solvers discussing the available optimisation and search algorithms. We will then move on to concolic testing as a solution to some of the problems associated with symbolic execution. In particular, practical optimisations to battle the path explosion will be discussed. Finally, we will present the design and implementation of our concolic Linux kernel executor and compare it to existing fuzzers in terms of achieved code coverage.
Vitaly is a security researcher specialising in reverse engineering and exploit development. He has a solid academic background in programming languages, algorithms and cryptography. He is currently focused on OS security (kernel space exploitation techniques and countermeasures on POSIX systems) and software hypervisors.
