Research On Static Analysis Methods To Detect Buffer Overflows Vulnerability

Buffer overflows at run-time can lead to non-deterministic program behavior, which may be used by malicious attackers to compromise a computer, such as to access or corrupt sensitive information, and even worse, to control the computer to attack others. Every year, hundreds of thousands of network attacks happen, about fifty percent of which are related to buffer overflow vulnerabilities. And the economic waste caused by this kind of attacks is more than 10 billion dollars. Buffer overflow has become the most dangerous and most common software security vulnerability.Static analysis can be used to detect vulnerability by analying source codes. It helps developers in eliminating buffer overflows before software is deployed and improve software security essentially. Compared with dynamic analysis, static analysis methods have such advantages as not slowing down program execution, not leading to compatibility problems and being processed at early stage of software development. Static detection for buffer overflow (SDBO) is becoming a hot topic in the area of information security.The goal of the thesis is to present very high precise and efficient static analysis methods for buffer overflow detection without depending on user annotations. Among the existing static analysis methods, data flow analysis and constraint analysis don't depend on user annotations, and are very efficient at the same tiime. Data flow analysis propagates ranges of constraint variables along control flow, and gains solutions when fixed point is arrived. But data flow analysis method does not trace control conditions. Especially, the traditional widening/narrowing method does not consider data dependence between constraint variables of loop control conditions. Therefore, the precision of existing data flow analysis is poor. Constraint analysis finds program characteristics by building and solving constraint states of the program. If there are co-dependent relations among constraint variables defined in a loop, the constraint states including these relations are infeasible. In addition, the existing constraint-based static detection systems ignore the propagation and solution of execution conditions of instructions, which makes the detection precision very low.To improve the precision and efficience of static analysis methods for buffer overflow vulnerabilities, detailed researches have been done. The main contributions are as follows:(1) To improve the precision of data flow loop analysis, a loop analysis method based on reverse paths is proposed. Buffer overflows are usually related to loops. With the widening/narrowing operator, traditional loop analysis methods can obtain approximate solutions of loops fast, but these methods ignore data dependence between constraint variables, and leads to poor imprecise. In this dissertation, a framework based on bidirectional data flow analysis and the corresponding bidirection dataflow equations are established. On the basis of the framework and the equations, a loop analysis algorithm is proposed. For control nodes that may improve the result of loop analysis, the algorithm first propagates control conditions along reverse paths, and then makes a forward data flow analysis to improve their data flow state. By this way, the precision of the loop analysis is improved.(2) To avoid the redundant constraint conditions that are generated by exhaustive constraint analysis, a demand-driven constraint generating method is proposed. Traditional constraint analysis methods compute constraint information for every instruction. Because many instructions are not related to memory access, the exhaustive method should generate many redundant constraints for buffer overflow detection. Our demand-driven constraint generation approach only maintains constraint states for memory access instructions, and only considers constraint information that is related to buffer overflow detection. Therefor, the number of constraint states and constraint conditions is decreased and the efficiency of constraint generation is improved.(3) To improve the solution precision of constraint state computing, a constraint state computing algorithm which mutually refines the solution of range constraints and control constraints is proposed. Through an iteration of "resolution - check - refinement", the algorithm reduces ranges of constraint variables with range constraints and control constraints, and improves resolution precision of overflow expression step by step. It is more precise than existing ones benefit from control constraints. At the same time, it stops the iteration as soon as the memory access is decided to be safe, avoiding unnecessary computation. To eliminate constraint conditions that make range constraints infeasible, this algorithm builds range dependency graph of the range constraints and breaks loops in the graph, which is more efficient than the tradition methods of using IIS.(4) To overcome the shortcoming of single static analysis mode that cannot gain both high precision and high efficiency, a hierarchy analysis algorithm based on counter-example is proposed. As a hierarchy analysis approach, it first makes a fast detection with flow sensitive and context sensitive analysis to find possible buffer overflow vulnerabilities, then makes a precision detection with path and context sensitive analysis guided by the former result to reduce false positives and identifying the concrete path of inducing buffer overflow. Since the counter examples are constructed under the guide of the fast analysis, the algorithm is more efficient than traditional path-sensitive algorithms, and don't sacrifice precision at the same time. To eliminate the imprecision of buffer overflow static detection with data flow analysis and constraint analysis, the algorithm forms the analysis state of memory access instructions by combining the result of data flow loop analysis and the constraint state of constraint state of constraint analysis.(5) A prototype system is designed and implemented with technologies described above. The experiment results show that the prototype system can detect buffer overflow vulnerabilities automatically with high precision and high efficiency. In the mass, the capability of the prototype system is better than existing classical systems.To sum up, in this dissertation, several key problems of SDBO have been studied and some contributions have been achieved. Our contributions listed above are helpful for enhancing the performance of SDBO in both theory and practice.