Using Propositional Calculas to Accurately Structure Control-Flow from Binary Executables

In recent years, there has been a growing need for analyst to explore inside the binary executables for the reasons of decompilation, security analysis, reverse engineering, etc. It is very helpful to recover the high-level control structure information, such as loops and conditionals, from arbitrary control-flow of low-level code.This paper presents a novel approach to structure control-flow graphs in binary executables, which are normally represented by unconditional or conditional jumps. We firstly formalize control flow information of the instructions into expressions of propositional calculus. Then the control flow information can be propagated along the execution path. At last, high-level control structures are identified and recovered through the result of calculation.