Research On C Program Array Out Of Bounds Checking Technology

With the wide range of software applications, users demanding for software to meet the increasingly complex logic function are also pursuit of high security and reliability software. Array out of bound being a kind of common run-time errors in programs, has become such major hidden dangers that affect the normal operation of the program.An array can be essentially seen as a mapping of indices to array elements. Based on this idea, we reduce the problem of checking array-out-of-bound problem to the problem of finding ranges of values of program variables. Abstract interpretation provides a theoretical basis for program static analysis. It can automatically infer the range of variables in a program at compile time. Based on this technique, we build a static analysis framework supporting analysis of arrays, which includes three modules named front-end, abstract domain library and fixed point solver. And abstract domain is the key point of the array analysis.In order to support the analysis of array bounds, from the different levels of accuracy and scalability, we design and implement two types of abstract domains for array analysis.1. The "arrayMerge" domain based on merge semantics. In order to achieve high scalability, we abstract the entire array into a single interval variable, and develop a abstract domain named "arrayMerge".2. The "arraySmash" domain based on smash semantics. From the perspective of high-precision, we use n single interval variables to model array with size n, and each array element is abstracted by interval variables. On this idea, we develop an abstract domain named "arraySmash".Finally, we analyze some array programs through experiment, and the results demonstrate the effectiveness of our tool.