Architecture description language based retargetable symbolic execution

This paper presents an approach to retargetable SMT-constrained symbolic execution of machine code. The retargetability is based on an existing open-source processor architecture description language which has been used for processor design and automatic generation of toolchains for dynamic program analysis. The benefit of the presented approach is that with a given architecture description, no manual writing of an instruction set grammar or of a translation of instruction semantics into logics is necessary. The proposed tool architecture relies on language reflection, code generation and dynamic loading to retarget symbolic execution to different machine code syntax. Instruction semantics is translated into SMT bit-vector logic equations by symbolically interpreting the architecture description language. The approach is implemented as plug-in extension to the Eclipse IDE and evaluated by automatically detecting integer overflows in binaries for the ARMv5 and SPARCv8 architectures.