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.