Accurate binary-level symbolic execution of embedded firmware

Abstract

Symbolic execution is an automated software testing technique that has enabled the discovery of numerous bugs in conventional, non-embedded software. Unfortunately, its application to embedded firmware is presently limited due to unique challenges associated with this domain. Central to many of these challenges is the tight integration of hardware and software components. Due to this tight integration, firmware interacts on a low abstraction level with both the processor and the peripherals provided by a hardware platform. In order to support these interactions, a symbolic execution engine needs to implement the reference manuals specifying processor and peripheral behavior. These specifications have an enormous complexity; hence, prior work approximates peripheral behavior and abstracts processor instruction execution. Unfortunately, these approximations may induce inaccuracies, which can result in bugs being missed in the tested firmware. This dissertation accomplishes a more accurate analysis by contributing a binary-level symbolic execution approach that is faithful to both the specification of peripheral behavior and processor instruction execution. This is achieved by facilitating machine-readable formal descriptions of instruction semantics and an established modeling standard for the description of peripheral behavior. Conducted experiments have resulted in the discovery of 16 previously unknown bugs in a popular embedded operating system, thereby illustrating the effectiveness of the proposed approach.