Linux kernel is pervasive in the cloud, on mobile platforms, and on supercomputers. To support these diverse computing environments, the Linux kernel provides extensibility and modularity through Loadable Kernel Modules (LKM), while featuring a monolithic architecture for execution efficiency. This architecture design brings a major challenge to the security of Linux kernel. Having LKMs run in the same memory space as the base kernel on Ring 0, a single flaw from LKMs may compromise the entire system, e.g., gaining root access. However, validation and debugging of LKMs are inherently challenging, because of its special interface buried deeply in the kernel, and non-determinism from interrupts. Also, LKMs are shipped by various vendors and the public may not have access to their source code, making the validation even harder. In this paper, we propose a framework for efficient bug detection and replay of commercial off-the-shelf (COTS) Linux kernel modules based on concolic execution. 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. We evaluate our approach on over 20 LKMs covering major modules from the network and sound subsystems of Linux kernel. The results show that our approach can effectively detect various kernel bugs, and reports 5 new vulnerabilities including an unknown flaw that allows non-privileged users to trigger a kernel panic. By leveraging the replay capability of our framework, we patched all the reported bugs in the Linux kernel upstream, including 3 patches that were selected to the stable release of Linux kernel and back-ported to numerous production kernel versions. We also compare our prototype with kAFL, the state-of-the-art kernel fuzzer, and demonstrate the effectiveness of concolic execution over fuzzing on the kernel level.

In this paper, we present crete , a versatile binary-level concolic testing framework, which features an open and highly extensible architecture allowing easy integration of concrete execution frontends and symbolic execution engine backends. crete ’s extensibility is rooted in its modular design where concrete and symbolic execution is loosely coupled only through standardized execution traces and test cases. The standardized execution traces are llvm -based, self-contained, and composable, providing succinct and sufficient information for symbolic execution engines to reproduce the concrete executions. We have implemented crete with klee as the symbolic execution engine and multiple concrete execution frontends such as qemu and 8051 Emulator. We have evaluated the effectiveness of crete on GNU Coreutils programs and TianoCore utility programs for UEFI BIOS. The evaluation of Coreutils programs shows that crete achieved comparable code coverage as klee directly analyzing the source code of Coreutils and generally outperformed angr . The evaluation of TianoCore utility programs found numerous exploitable bugs that were previously unreported.

SystemC is a system-level modeling language increasingly adopted by the semiconductor industry. Quality assurance for SystemC designs is important, since undetected errors may propagate to final silicon implementations and become very costly to fix. The errors, if not fixed, can cause major damage and even endanger lives. However, quality assurance for SystemC designs is very challenging due to their object-oriented nature, event-driven simulation semantics, and inherent concurrency. In this research, we have developed an approach to generating high coverage tests for SystemC designs using symbolic execution. We have applied this approach to a representative set of SystemC designs. The results show that our approach is able to generate tests that provide high code coverage of the designs with modest time and memory usage. Furthermore, the experiment on a RISC CPU design with more than 2K lines of SystemC code demonstrates that our approach scales to designs of practical sizes.

Robustness testing is a crucial stage in the device driver development cycle. To accelerate driver robustness testing, effective fault scenarios need to be generated and injected without requiring much time and human effort. In this paper, we present a practical approach to automatic runtime generation and injection of fault scenarios for driver robustness testing. We identify target functions that can fail from runtime execution traces, generate effective fault scenarios on these target functions using a bounded trace-based iterative strategy, and inject the generated fault scenarios at runtime to test driver robustness using a permutation-based injection mechanism. We have evaluated our approach on 12 Linux device drivers and found 28 severe bugs. All these bugs have been further validated via manual fault injection. The results demonstrate that our approach is useful and efficient in generating fault scenarios for driver robustness testing with little manual effort.

Behavioral synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a register-transfer level (RTL) implementation. In this paper, we present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis front-end. Our approach makes use of dual-rail symbolic simulation of the input and output of a transformation, together with identification and inductive verification of their loop structures. We have evaluated our framework on transformations applied by an open source behavioral synthesis tool to designs from the CHStone benchmark. Our tool can automatically validate more than 75 percent of the total of 1008 compiler transformations applied, taking an average time of 1.5 seconds per transformation.

High-quality tests for post-silicon validation should be ready before a silicon device becomes available in order to save time spent on preparing, debugging and fixing tests after the device is available. Test coverage is an important metric for evaluating the quality and readiness of post-silicon tests. We propose an online-capture offline-replay approach to coverage evaluation of post-silicon validation tests with virtual prototypes for estimating silicon device test coverage. We first capture necessary data from a concrete execution of the virtual prototype within a virtual platform under a given test, and then compute the test coverage by efficiently replaying this execution offline on the virtual prototype itself. Our approach provides early feedback on quality of post-silicon validation tests before silicon is ready. To ensure fidelity of early coverage evaluation, our approach have been further extended to support coverage evaluation and conformance checking in the post-silicon stage. We have applied our approach to evaluate a suite of common tests on virtual prototypes of five network adapters. Our approach was able to reliably estimate that this suite achieves high functional coverage on all five silicon devices.

Direct Memory Access (DMA) interfaces are a common and important component of Hardware/Software (HW/SW) interfaces between peripheral devices and their device drivers. We present a HW/SW co-validation framework to validate DMA interface implementations of a device and its driver. This framework employs a virtual prototype of the device as a reference model and performs co-validation in two stages: (1) conformance checking which checks the DMA interface conformance between the device and its virtual prototype; (2) property checking which checks device/driver interactions across the DMA interface. In conformance checking, the virtual prototype infers the device state transitions by taking the same driver request sequence to the device. Property checking verifies system properties over the device state transitions exposed through the virtual prototype. This framework assists HW/SW integration validation by detecting DMA interface bugs in both devices and drivers. Furthermore, we have developed three key techniques: capture-on-write policy, partial capture, and environmental input prediction, to address two major challenges in scaling the framework: DMA capture overhead and imprecise environmental input simulation. We have applied this approach to four Ethernet adapters, discovering 12 serious DMA interface bugs from the devices, their virtual prototypes and their drivers. The results demonstrate that our approach has major potential in facilitating HW/SW co-validation.

Virtual prototypes are increasingly used in device/driver co-development and co-validation to enable early driver development and reduce product time-to-market. However, drivers developed over virtual prototypes often do not work readily on silicon devices, since silicon devices often do not conform to virtual prototypes. Therefore, it is important to detect the inconsistences between silicon devices and virtual prototypes.

Post-silicon validation is a crucial stage in the system development cycle. To accelerate post-silicon validation, high-quality tests should be ready before the first silicon prototype becomes available. In this paper, we present a concolic testing approach to generation of post-silicon tests with virtual prototypes. We identify device states under test from concrete executions of a virtual prototype based on the concept of device transaction, symbolically execute the virtual prototype from these device states to generate tests, and issue the generated tests concretely to the silicon device. We have applied this approach to virtual prototypes of three network adapters to generate their tests. The generated test cases have been issued to both virtual prototypes and silicon devices. We observed significant coverage improvement with generated test cases. Furthermore, we detected 20 inconsistencies between virtual prototypes and silicon devices, each of which reveals a virtual prototype or silicon device defect.

Virtual prototypes of hardware devices, a.k.a, virtual devices, are increasingly used to enable early software development before silicon prototypes/devices are available. In previous work, we presented a post-silicon conformance checking approach to detecting interface state inconsistencies between a silicon device and its virtual device. In this paper, we present an optimization, adaptive concretization, to reduce the overhead incurred by symbolic execution, a key technique used in our conformance checking approach. We have evaluated our optimized approach on three Ethernet adapters and their virtual devices. The results demonstrate that it is effective and efficient: 21 inconsistencies are discovered and time usages are reduced by an order of magnitude, comparing to the previous approach.

Behavioral synthesis entails application of a sequence of transformations to compile a high-level description of a hardware design (e.g., in C/C++/SystemC) into a Register-Transfer Level (RTL) implementation. We present a scalable equivalence checking framework to validate the correctness of compiler transformations employed by behavioral synthesis. Our approach is based on dual-rail symbolic simulation of the input and output design representations of a transformation. We have evaluated our framework on transformations applied to several designs by an open source behavioral synthesis tool, and we present initial results demonstrating the approach.