Guided Symbolic Execution in Real-World Binary Program

Symbolic execution, one of the methods of program automatic analysis, has significantly improved technically over the past few years. However, it is still not practical to analyze the program using only the symbolic execution itself. The main reason is the lack of memory due to the path explosion problem which occurs during the Real-world Program analysis, for which we cannot get all solutions on all the paths of the program. Therefore, it is practical for the analyst to organize the symbolic execution search path with points having vulnerability rather than getting solutions on all the paths and then to carry out the analysis. In this paper, we propose static analysis method and dynamic analysis method based on Real-World Binary analysis. First, Static Backward Analysis enables the analyst to select potential vulnerable points within the binary and generate a backward Control Flow Graph (CFG) generated from the corresponding point to the user input (I/O) point. At the dynamic analysis stage, we propose Taint Analysis for generating Symbolic File and in Guided Symbolic Execution based on the selected priority path we propose, and Bug Check Model. In order to prove the efficiency of our research, we conducted a study of identifying vulnerable point in severalWindows and Linux Real-world binaries, and the experiment results showed that it was possible to identify vulnerability in various situations of binaries.