Symbolic Execution for Dynamic Kernel Analysis

Linux kernel-based operating systems have a significant market share in the domains of enterprise/web servers, supercomputers, and mobile devices. Being a large open-source project, the Linux kernel undergoes many changes, with new functionalities (e.g. Support for Rust in the kernel) being added in each release. While the security analysis of the Linux kernel is of critical importance, it is a challenging task. Although symbolic execution based techniques have been used for kernel analysis in the past decade, existing tools have fundamental limitations in kernel thread analysis, such as the need for instrumentation of the target kernel and the lack of user control, command, and access to the target execution. This dissertation aims to address these limitations by proposing a new kernel symbolic execution engine for kernel thread analysis. We then intend to leverage the new engine to conduct a security analysis of Rust drivers written for the Linux kernel. As part of the analysis, we will perform symbolic execution on Rust drivers, detect bugs, and evaluate whether the integration of Rust drivers with the rest of the kernel, written in C, results in any security vulnerabilities.