Optimization Of Constraint Solver For KLEE, A Dynamic Symbolic Execution Tool

Since 20 th century, computer technology has been applied to many aspects of production and social activities as a representative of the high-tech industry. It plays irreplaceable roles in many important areas. The 21 st century, computer technology makes a rapid development. And it promotes industrial and economic development.At the same time, the security issues of software bring high risks into social economic activities. The software testing technology guarantees the software works reliably and correctly. During the study, researchers have arisen many techniques. Since the artificial static detection to the auto-execution fuzz testing, software testing technology has been evolving with the growth in the size and complexity of software. With the increasing scale and complexity of the modern software, the demand for security in software is also keeping rising. Traditional software testing technology can’t meet the current needs of software security, with their own limitations. Currently, dynamic symbolic execution gets widespread concern in the field of software testing because of its some excellent properties.Dynamic symbolic execution(abbrev. DSE) based on symbolic execution raised in the 1970 s. It has some advantages of auto-generation of test case, high path coverage rate, and full automation. Many DSE tools are developed by companies and colleges, such as KLEE by Stanford University and SAGE by Microsoft. The tools perform well in practical applications while some important problems still exist in DSE: path explosion, pointer arithmetic and constraint solving performance. Among the three main problems, constraint solving performance affects the efficiency of DSE tools directly.This article focuses on the constraint solving technology applied in KLEE. And I Designed a new constraint solving architecture in KLEE to improve the performance of constraint solving. In my research, I put Z3 solver into KLEE as a parallel constraint solver with STP solver which has been implemented already. Then I test 9 cases in Unix Coreutils to verify the validity of the design. The result shows that the parallel constraint solver architecture performs better than the original KLEE constraint solver.