Concolic Execution of Multi-threaded Assembly Programs

Kurzfassung

At its core, this thesis is an exploratory study that attempts to determine whether a relatively new technique, concolic execution for multi-threaded programs [12], can be used in a particular context, assembly lifting. It presents a prototype for an ARM v7 assembly lifter using this technique. The thesis contains a detailed description of how concolic execution for multi-threaded programs works and also covers many optimizations (both implemented and unimplemented) to improve the scalability of this technique. The work considers mainly embedded software for safety-critical applications, e.g., space applications. Due to the prototypical nature of the assembly lifter, some important features are not yet covered. At the moment, the tool only creates an internal representation of the program and does not translate this representation into the intended target language, LLVM-IR. It also covers only a small subset of the assembly language and does not cover some important features of the assembly language (interrupts, proper initialization of certain global variables, …). The scalability and applicability of the proposed solution is evaluated on synthetic test cases. At the moment, the scalability of the tool is not sufficient to be able to apply it to large assembly programs.