First Advisor

Fei Xie

Date of Publication

Summer 7-16-2019

Document Type


Degree Name

Doctor of Philosophy (Ph.D.) in Computer Science


Computer Science


Computer software -- Testing, Computer science



Physical Description

1 online resource (xii, 118 pages)


Computing systems are experiencing an explosive growth, both in complexities and diversities, ushered in by the proliferation of cloud computing, mobile computing, and Internet of Things. This growth has also exposed the consequences of unsafe, insecure, and unreliable computing systems. These all point to the great needs of sophisticated system validation techniques. Recent advances in research on symbolic execution has shown great promises for automated software analysis, e.g., generating test cases, finding bugs, and detecting security vulnerabilities. However, symbolic execution is mostly adopted to analyze user applications, while modern computing systems in practice consist of many components shipped by various vendors, besides user applications, e.g., operating systems, firmware and hardware devices. In this dissertation, we propose versatile binary-level concolic testing, which defines a standard execution-trace format, and features an open and highly extensible architecture. It allows easy integration of multiple concrete execution frontends and symbolic execution backends, which significantly improves the applicability and flexibility of symbolic execution, especially to modern computing systems with various components.

First, we present the design and implementation of CRETE, the infrastructure of versatile binary-level concolic testing. CRETE provides an open and highly extensible architecture allowing easy integration of multiple concrete and symbolic execution environments, which communicate with each other only by exchanging standardized traces and test cases. We also present several optimizations for scaling CRETE to practical user applications. Our experiments show CRETE outperformed state-of-the-art open-source systems for automated program analysis at source-level and binary-level. It also found numerous bugs that were previously unreported from mature open-source projects.

Second, we present COD, a framework based on versatile binary-level concolic testing for automated bug detection and replay of commercial off-the-shelf (COTS) Linux kernel modules (LKMs). Our framework automatically generates compact sets of test cases for COTS LKMs, proactively checks for common kernel bugs, and allows to reproduce reported bugs repeatedly with actionable test cases. Our experiments show that COD can effectively detect various kernel bugs, and reports 5 new kernel vulnerabilities including an unknown flaw that allows non-privileged users to trigger a kernel panic. With the replay capability of our framework, we patched all the reported bugs in the Linux kernel upstream, including 3 patches were selected to the stable release of Linux kernel and back-ported to numerous production kernel versions.

Last, we present how we leverage versatile binary-level concolic testing for system-level validation of Systems-on-Chips (SoC). We capture run-time traces of Hardware/Software (HW/SW) components across the entire SoC stack which are emulated by multiple virtual platforms. Based on segmented traces captured from various SoC components, we assemble system-level traces and provide interfaces for users to inject system-level assertions to validate. The experimental results demonstrate that our approach can generate effective system-level test cases crosscutting the entire HW/SW stack of SoC and triggering an IP firmware bug from user inputs of an IP utility program, and can catch various bugs with system-level assertions.

Persistent Identifier