Research And Implementation Of The Key Method On Code Static Analysis Based On The Symbolic Execution

With the development of software technology, the software system is applied to all aspects of our lives. It bring us great convenience, but also bear us tremendous risks which caused by software vulnerabilities. Methods to guarantee software quality are a very urgent need. Those methods can be taked into two categories; one is static checking which usually used early stage to detect the potential vulnerabilities through analysis the source code, the other one is dynamic testing which through runing the binary code and checking the result. The sooner of bugs to be found, the smaller of modification costs. So the static checking is an important method to guarantee software quality. Among the static checking methods, symbolic execution for its high degree of accuracy received great attention.Symbolic execution is a context-sensitive path analysis method. In the case of computing resources sufficient enough, it can deeply analysis the program, and found some minor bugs. However, symbolic execution theory itself is also facing several major challenges which are the path explosion, constraint solving and memory model.Firstly, the paper outline the the development of symbolic execution techniques during the last three decades, discussed the basic principles of symbolic execution and related improvements.Those improvements include raised dynamic symbolic execution for test data generation; proposed some heuristic search strategy to suppress the explosion of path; proposed to eliminate irrelevant and incremental solver to improve constraint solving. Then the paper discusses a very powerful intermediate language LLVM IR, introduce its grammar structure, data types, and instruction set, and formalize the data types and instruction set. Then the paper discussed the memory model of symbolic execution, introduced and compared the current mainstream model(name-value model,array model and region-based model).And then the paper proposed TMM(Tree-memory model)model,the core idea of this model is that using a tree structure to represent the nested data. The memory model can effectively solve the challenge of type conversion, pointer alias and uncertain size of data. Finally, based on the TMM, LLVM IR and Z3, we implements a simple symbolic execution engine SSE, and through experiment verified the SSE’s effectiveness and advancement.