Operating systems are critical components of the Trusted Computing Base (TCB) of any computer system. They need to be secured to ensure the confidentiality, integrity and availability of the applications running on top of them. To achieve this, dynamic program analysis techniques have been used to find vulnerabilities and mitigate weaknesses in operating systems. By executing the program under test and performing analysis, dynamic program analysis can achieve higher accuracy compared to static analysis. This dissertation showcases three applications of dynamic program analysis and addresses the challenges of using them to secure operating systems.

First, we present Mousse, a solution to address the challenges of using Selective Symbolic Execution (SSE) for analyzing the Hardware Abstraction Layer (HAL) programs. HAL programs, which communicate between user space programs and the kernel, are an integral part of many operating systems. Existing symbolic execution engines are inefficient in testing them due to false positives introduced by symbolic hardware or poor performance caused by expensive memory synchronization. In Mousse, we proposed process-level SSE. Combining with environment-aware concurrency and distributed execution, it can achieve good performance with no false positives.

Secondly, we present Sifter, a syscall filtering framework for tightening the attack surface of the operating system. Since malware often uses abnormal syscall patterns to exploit vulnerabilities in the kernel, we build a framework that can trace and analyze syscalls from legitimate programs, and then generate syscall filters that only allow syscall patterns seen in the traces.

Finally, we present the eBPF runtime fuzzer (BRF) for fuzzing eBPF runtime components in the Linux kernel. eBPF is a modern technology in the Linux kernel that allows programs supplied from the user space to be executed in the kernel. Although fuzzing has been proved to be effective in finding bugs in the Linux kernel, the state-of-the-art fuzzer, Syzkaller, fails to reach the eBPF runtime components due to 1) syscall dependencies in the eBPF subsystem, 2) semantic rules imposed by the eBPF verifier to ensure the safety of eBPF programs, and 3) failure to attach and execute the loaded programs. With extensive experiments, we show that BRF is not only more efficient in reaching runtime components, but also covers more code. Finally, it manages to find 4 vulnerabilities (3 of which have been assigned CVE numbers) in the eBPF runtime components.