Search

Concolic testing is a software testing technique, which improves the scalability of symbolic execution by allowing efficient concretization of symbolic expressions. Concretization converts a symbolic expression to a concrete value, e.g., when the constraints of a symbolic expression become too complex for the utilized solver to handle. Unfortunately, concretization negatively impacts completeness of the performed analysis. For example, if a branch in the tested program depends on a previously symbolic value, which is now concrete, this branch will not be tracked by the symbolic execution engine. As such, the tested code is not explored in its entirety and errors may remain undetected. In order to allow a verification engineer to identify code parts which have not been tested sufficiently, due to concretization, we propose a novel metric, which quantifies performed concretizations. Furthermore, we contribute a visualization of this metric, which eases identifying code parts, which depend, directly or indirectly, on symbolic values affected by concretization. To the best of our knowledge, this is the first work proposing a concretization metric for concolic testing, to stimulate further research on this topic we have released our implementation as open-source software. [ABSTRACT FROM AUTHOR]

Constrained Internet of Things (IoT) devices with limited computing resource are increasingly employed in security critical areas. Therefore, it is important for the firmware of these devices to be tested sufficiently. On non-constrained conventional devices, dynamic testing techniques (e.g. fuzzing, symbolic execution, or concolic testing) are successfully utilized to discover critical bugs in tested software. Unfortunately, the diverse ecosystem and the dependence on low-level details of a wide range of peripherals makes it difficult to use these techniques in the IoT context. In order to address these challenges, we present SymEx-VP an open source emulation-based approach for concolic testing of IoT firmware. SymEx-VP is a virtual prototype for RISC-V hardware platforms and allows concolic testing of RISC-V machine code. To support a wide range of different peripherals, SymEx-VP utilizes SystemC, a hardware modeling language for C++. By employing a SystemC extension mechanism, SymEx-VP can inject concolic inputs into the emulated firmware through the memory-mapped I/O peripheral interface of existing SystemC peripheral models. This allows us to support different operating systems and libraries used in the IoT with minimal integration effort. We provide an extensive description of SymEx-VP, illustrate peripheral modeling and firmware testing using it by example, and perform tests with four operating systems to demonstrate the advantages of our OS-agnostic firmware testing method. [ABSTRACT FROM AUTHOR]