Decompiling High-level Control Structures with Propositions

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 recovery 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. We have implemented our method in RADUX, a statical malicious code detector based on semantic analysis. Our experimental result shows that this method can recognize and recovery loops and conditionals effectively, and have the ability of analyzing the predicated instructions.