Symbolic execution is one of the most important computational intelligence methods in vulnerability detection, delivering high code coverage. The bottleneck of dynamic symbolic execution is its running speed, and few existing works focus on research of the problem. In the paper, we present a taint-based symbolic execution method to improve its efficiency.
The property of our method includes: 1) it works on the binary level directly, translating binary into a well-defined intermediate representation; 2) it employs a taint layer to perform data flow analysis and quickly locate the first instruction related with symbolic inputs. 3) Three optimization strategies are utilized in symbolic execution to further speed enhancing, including white list, state elimination and path search optimization. We have implemented a prototype based our method, and evaluated it with several sample programs. The experimental results shows that our method could perform faster symbolic execution and has the ability of vulnerability detection.