Research On Concolic Testing Based On Symbol Summary

In recent years, more and more attention has been paid to the problem of software security because of the increasing of malicious software and network attacks. Software testing is an important technique to ensure the security and reliability of the software. With the increasing of softwares’ size, the traditional software testing methods can not meet the current demand. Dynamic symbolic execution has become an important technique in this field since it was put forward. This technique can automatically generate test cases and explore different paths with the information that collect during symbolic execution. In spite of the many advantages, dynamic symbolic execution technique is still in the research stage. It has not been widely used in industry, which is because of many technical problems, such as path explosion, floating point arithmetic, symbol of pointers etc. Among these problems, path explosion is most serious, which makes the tool can only complete a small part of the path exploration in a reasonable time range. The consequence is that we get the low rate of code coverage, which seriously affects the performance of the tool. Path explosion is a difficult problem which we can not solve for now. Therefore, in this thesis, I proposed a new dynamic symbolic execution method, which can improve the speed of symbolic execution.In this thesis, the method based on symbolic summary has been proposed, which is based on the detailed analysis of current dynamic symbolic execution’s methods and process. The method combined the characteristics of the paths’ exploration and symbolic execution. It can maximize the use of symbols’ information, which was collected during each execution. And it can avoid a lot of repeated work to improve the overall efficiency of the implementation. In order to verify the effectiveness of the method, this thesis designs and implements a prototype system of CTSS(Concolic Testing based on Symbol Summary). Experimental results show that the proposed method can improve the efficiency of dynamic symbolic execution.