Symbolic execution is a widely used program analysis technique to systematically executedifferent program execution paths without requiring concrete inputs. Developed from sym-
bolic execution, Selective Symbolic Execution (SSE) is a technique for creating the illusion
of full system symbolic execution, while symbolically running only the code that is of interest
to the analyst. SSE makes symbolic execution practical for large software like an operating
system by alleviating the problem of path explosion.
In this thesis, we demonstrate the possibility of using SSE to tackle security challenges inoperating systems. Our first work is Mousse, which is a system for selective symbolic execu-
tion of programs with untamed environments. Mousse facilitates testing operating system
services that are highly coupled with their underlying environment by developing three novel
solutions. Our second work is Macaron, which is the first framework that can automatically
and reliably reproduce non-deterministic race condition bugs in the operating system kernel.
We demonstrate the usefulness of Macaron by using it to reproduce bugs found (but not
reproduced) by syzbot, the state-of-the-art continuous kernel fuzzing framework. We build
Macaron using a novel Guided Selective Symbolic Execution (GSSE), static analysis, and a
distance-based thread interleaving points scheduling algorithm.