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. This chapter presents 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, e.g., operating systems, firmware, and hardware devices. First, this chapter presents the design and implementation of CRETE, the infrastructure of versatile binary-level concolic testing. Second, this chapter presents 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). This 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. Last, this chapter presents how versatile binary-level concolic testing is leveraged for system-level validation of Systems-on-Chips (SoC). The authors capture runtime 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, the authors assemble system-level traces and provide interfaces for users to inject system-level assertions to validate.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Versatile Binary-Level Concolic Testing

  • Bo Chen,
  • Fei Xie

摘要

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. This chapter presents 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, e.g., operating systems, firmware, and hardware devices. First, this chapter presents the design and implementation of CRETE, the infrastructure of versatile binary-level concolic testing. Second, this chapter presents 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). This 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. Last, this chapter presents how versatile binary-level concolic testing is leveraged for system-level validation of Systems-on-Chips (SoC). The authors capture runtime 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, the authors assemble system-level traces and provide interfaces for users to inject system-level assertions to validate.