Dynamic Symbolic Execution for Enhanced Intermediate Representation of Data Flow Space Applications

Abstract

Verifying the safety and security requirements of embedded software requires a code analysis. Many software systems are developed based on software development libraries; therefore, code specifications are known at compiling time. Hence, many source-code analyses will be excluded, and low-level intermediate representations (LLIRs) of the analyzed binaries are preferred. Improving the expressiveness of the LLIR and enhancing it with more information from the binaries will improve the tightness of the applied analyses. This work is interested in developing a lifterthat lifts binaries into an enhanced LLIR and can resolve indirect jumps. LLVM is used as the LLIR. Our proposed lifter, which we call DEL (Dynamic symbolic Execution Lifter), combines both static and dynamic symbolic execution and strives to fully recover the analyzed program’s control flow. DEL consists of an API to translate ARMv7-M assembly instructions into static single assignment LLVM instructions, an LLIR to Z3 expressions parser, a memory model, a register model, and a specialized condition flags handler. This work used a case study based on a software development library for onboard data-handling applications developed at the German Aerospace Center (DLR), which is called the Tasking Framework. DEL demonstrated high accuracy of around 93% in resolving indirect jumps in our case study.