Software Vulnerability Testing Technology Based On Symbolic Execution

In recent years, people pay close attention to computer security problems, theseproblems are caused by the application software vulnerabilities, and the softwarevulnerabilities refer to that software has potential exceptions or vulnerabilities. Atpresent, there are basically three methods of testing software vulnerabilities: manualanalysis, static automatic test and dynamic automatic test. Manual analysis depends on alot of artificial operations, static automatic test needs to get the software source code,and its reasoning ability is limited, so, the two methods are not suitable for today‘ssoftware which becomes more and more complicated and has diversity functions. Thecurrent mainstream method of dynamic automatic test is fuzzing test, but there are somefaults in fuzzing test which makes it difficult to find some vulnerabilities.Symbolic execution is a dynamic test method, this method monitoring softwareexecutive process dynamically, acquires path constraint condition information, and getsthe input for next execution according to the solution. With the construction of usefultest cases, symbolic execution can not only reach high rate of test code coverage, butcan be targeted to trigger some exceptions or vulnerabilities. The more important thingis, it doesn‘t need to obtain program‘s source code and internal structure, which makes itbe suitable for complex large commercial software.The thesis summarizes the current situation of software vulnerability testing andsymbolic execution, introduces the basic concept of symbolic execution and some tools,describes the main process of symbolic execution, studies some problems and effectivesolutions of symbolic execution, and prospects symbolic execution‘s new developmenttendency in the field of software vulnerability test. This thesis realizes a softwarevulnerability testing system based on symbolic execution. It has a lot of newimprovements comparing with the traditional symbolic execution. Finally, this thesisproves these improvements through testing.The main contents include: dynamically capture the program inputs and make themsymbolically; establish memory mapping table to maintain the relationship of input dataand symbolic variable; track and record the symbolic variable while program running; collect the path constraint conditions, including important information; prospect asimple but effective intermediate language; solver researching and choosing; proposeloop identify algorithm to simplify program flow diagram; the research of path searchalgorithm, and propose a new path search algorithm; propose an intelligent test casechoosing method combined with the new path search algorithm.Through the research of symbolic execution problems, this thesis proposes somecorresponding schemes to improve these problems, especially the improvement to pathexplosion which makes the practical application of symbolic execution become morefeasible and has a certain positive effect and significance to the development ofsymbolic execution.