| |
 Symbolic Execution Engine For Dynamic Analysis Of System Software |  | Pansilu Madhura Bhashana Pitigalaarachchi PITIGALA ARACHCHILLAGE PhD Candidate School of Computing and Information Systems Singapore Management University | Research Area Dissertation Committee Research Advisor Committee Members External Member - ZHANG Fengwei, Associate Professor, Department of Computer Science and Engineering, Southern University of Science and Technology
|
| | Date 14 November 2025 (Friday) | Time 9:00am - 10:00am | Venue Meeting room 5.1, Level 5 School of Computing and Information Systems 1, Singapore Management University, 80 Stamford Road Singapore 178902 | Please register by 12 November 2025. We look forward to seeing you at this research seminar. 
|
|
|
| | ABOUT THE TALK This dissertation tackles 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 software from these hardware dependencies and provision the necessary system states for its execution, thereby enabling dynamic analysis. Analyzing such software, which is typically privileged, requires specialized tools. Moreover, we need a foothold to host the analyzer 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 frameworks that can be customized to combine multiple analysis techniques.
Addressing these challenges, we propose techniques that advance system software analysis. We present a symbolic execution engine as a framework for dynamic analysis of system software. It operates directly on the memory of live target threads, weaving symbolic execution into native execution. Users can develop custom analyzers that combine conventional dynamic analysis and symbolic execution to perform complex tasks requiring thorough binary-level reasoning. Building on this reference framework, we target two critical system software components. First, we present KRover, a symbolic execution engine for dynamic kernel analysis. KRover operates directly on the states of live kernel threads and enables dynamic symbolic analysis. Next, we present TDXplorer, a framework for dynamic symbolic analysis of Intel’s TDX Module, the core system software and trusted computing base of Intel TDX. TDXplorer is the first dynamic symbolic analysis system for the TDX Module. It provides an emulation environment for executing the TDX Module on a desktop PC, eliminating the need for TDX hardware and enabling both symbolic execution and conventional dynamic analysis. | | | SPEAKER BIOGRAPHY Pansilu Pitigala Arachchillage is a PhD candidate in Computer Science at Singapore Management University, supervised by Prof. Xuhua Ding. His research focuses on software and systems security. His PhD research addresses the challenges in analyzing system programs such as operating system kernels and Trusted Execution Environment firmware by developing tools and system-level techniques that combine dynamic binary analysis and symbolic execution. His work was accepted for publication at ACM CCS 2023 and 2025, and he was awarded the SMU Presidential Doctoral Fellowship in 2024. |
|