We present TDXplorer, the first dynamic symbolic analysis system for Intel's TDX Module, the software trusted computing base of TDX. Without using TDX hardware, an analyzer function on top of TDXplorer can not only apply dynamic analysis to control and instrument the TDX Module's execution, but also carry out symbolic execution for path exploration as well as security and functionality reasoning. The two types of analysis are seamlessly integrated in a way that symbolic execution is conducted directly upon the TDX Module's binary code and runtime states, which are shaped by using dynamic analysis techniques. We implement TDXplorer on Linux and measure its performance and correctness against executions on a TDX platform. Our case studies on symbolic modeling of secure EPT creation and KeyHole region management demonstrate that TDXplorer is a versatile and capable tool supporting various analysis tasks.

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.

We present KRover, a novel kernel symbolic execution engine catered for dynamic kernel analysis such as vulnerability analysis and exploit generation. Different from existing symbolic execution engines, KRover operates directly upon a live kernel thread's virtual memory and weaves symbolic execution into the target's native executions. KRover is compact as it neither lifts the target binary to an intermediary representation nor uses QEMU or dynamic binary translation. Benchmarked against S2E, our performance experiments show that KRover is up to 50 times faster but with one tenth to one quarter of S2E memory cost. As shown in our four case studies, KRover is noise free, has the best-possible binary intimacy and does not require prior kernel instrumentation. Moreover, a user can develop her kernel analyzer that not only uses KRover as a symbolic execution library but also preserves its independent capabilities of reading/writing/controlling the target runtime. Namely, the resulting analyzer on top of KRover integrates symbolic reasoning and conventional dynamic analysis and reaps the benefits of their reinforcement to each other.