Publication Type

PhD Dissertation

Version

publishedVersion

Publication Date

11-2025

Abstract

System software, like any regular software, is prone to errors. It plays a specific role in a computer system by managing the underlying hardware and providing a platform to execute the application software. Defective or vulnerable system software can be exploited by attackers to compromise the entire system. Therefore, the system software must be studied and thoroughly analyzed to evaluate its security. However, due to the inherent complexity and its close interactions with the hardware, analyzing system software is a challenging task. As a result, there is a lack of tools and techniques capable of effectively analyzing system software.

This dissertation tackles some key problems associated with enabling the dynamic analysis of system software. Because system software interacts directly with hardware, its execution is tightly coupled with the underlying platform and dependent on specific hardware features. Therefore, there is a need to decouple such system software from the specific hardware features it depends on and execute it on commodity hardware to enable efficient dynamic analysis. Analyzing such software dynamically requires special analysis tools. However, running an analyzer on the same system that is being analyzed is also difficult, as we need a foothold to host the analyzer itself on the system, provide mechanisms to introspect the target and manage system states. Furthermore, unlike generic tools, there is a lack of user-programmable analysis tools that can be customized to combine different analysis techniques and achieve various analysis tasks requiring thorough binary level reasoning.

To address these challenges, we propose techniques that advance system software analysis by combining symbolic execution with conventional dynamic analysis. First, we present a generic symbolic execution engine as a template for dynamic system software analysis. It adopts a VM-hosting approach, where the target system software runs inside a regular virtual machine, enabling dynamic symbolic analysis. The engine operates directly on the memory of live target threads, weaving symbolic execution into native execution. We enable user-programmable interfaces that allow analysts to develop custom analyzers that combine conventional dynamic analysis and symbolic execution to perform complex analysis tasks.

Building on this reference template, we extend it to target two critical system software components. First, we propose KRover, a symbolic execution engine for dynamic kernel analysis. KRover operates directly on the states of live kernel threads and enables dynamic symbolic analysis. We benchmark it against the state of the art, S2E, and show that KRover is on average 6.8 times faster while using one tenth to one quarter of S2E’s memory. Our case studies on vulnerability generalization, fix validation, and rootkit analysis show how users can build their own kernel analyzers on KRover. Next, we present TDXplorer, a system framework for symbolic analysis of Intel’s TDX Module, the core system software and trusted computing base of Intel Trust Domain Extensions. TDXplorer is the first dynamic symbolic analysis system for the TDX Module. It provides an emulation environment that allows the TDX Module to execute on a desktop PC without requiring TDX hardware, enabling both symbolic execution and conventional dynamic analysis. We evaluate TDXplorer’s performance and verify the accuracy of our TDX emulation against a real TDX server. Our analysis uncovered a canary bug and several discrepancies between the implementation and the documentation. Our case studies on symbolic modeling of secure EPT creation and dynamic memory management demonstrate TDXplorer’s utility and show how users can build their own TDX Module analyzers for complex analysis tasks.

Keywords

Software and System Security, System Software Analysis, Symbolic Execution, Dynamic Program Analysis

Degree Awarded

PhD in Computer Science

Discipline

Software Engineering

Supervisor(s)

DING, Xuhua

First Page

1

Last Page

165

Publisher

Singapore Management University

City or Country

Singapore

Copyright Owner and License

Author

Download

Share

COinS