Research And Implementation Of Code Security Inspection Based On The Symbolic Execution

Code security defect has been a stumbling block to the development of IT industry. The main reason could be attributed to the high cost but low efficiency of the security defect inspection. At present, two methods are mainly used to deal with this issue, which are manual inspection and tool inspection. For the former, the efficiency is not very ideal and that’s why the tool inspection is becoming more and more popular. Generally speaking, code security defect inspection tool could be divided into two categories: the traditional static analysis tool and the dynamic test tool. Symbolic execution relies on program analysis. It works by collecting constrain information, and then using the constraint solver to solve it before generating test cases. Theoretically symbolic execution can cover all paths of the program. The main work of this thesis is as follows:(1) Because of the exponential explosion problems hidden in the symbolic execution, the execution state selection algorithm which is based on CFG(Control Flow Graph) is therefore proposed. This algorithm works as follows. The required CFG will be extracted before generating a new execution state select algorithm on the basis of the execution’s weights. Thus, it can cover more paths when the path explosion occurs.(2) It’s suggested in this thesis to use useless function analysis to optimize the dynamic symbolic execution. Useless function analysis is a static analysis method mentioned in this thesis. It can be divided into two stages: the first stage is the dead code elimination, and the second stage is the elimination of pure function. By making use of the two stages to eliminate unnecessary code, it could seek the maximal optimization.(3) Based on the array model, the improvement on the design of the array model is proposed in this thesis. Tree structure is used to represent the array model to facilitate memory safety detection. At the same time, targeting the fact that the array model cannot process the data whose size are undetermined, this thesis betters the model and achieves improvement in dealing with this issues.(4) On the basis of what have been mentioned above, a simple dynamic symbolic execution tool is realized and implemented. The tool succeeds in checking the memory bounds problem, the double free problem, wild pointer problem, memory leak problem, integer overflow problem and division-by-zero bug.(5) Experimental analysis are implemented on the overall system, useless function analysis and CFG selection algorithm respectively. All in all, the results indicate the effectiveness of the tool.