Check bounds overflow bugs in C programs based on LLVM

Abstract

Bounds overflow is one of the most frequently encountered errors in C programs. For example, performing pointer arithmetic without checking bounds can cause bounds overflow. These errors can sometimes be latent for a long time, being discovered only after the program is already in production. I think bounds overflow bugs are the sources of security vulnerabilities in programs, and thus particularly serious.
Benefits to LLVM and LLVMers

Everyone who wants to do some research on checking out-of-bounds errors can benefit from my project. They can add their own new pass to increase the analysis accuracy, or use some of my passes to do a variety of their own jobs. I want to write some passes which can be used to check programs with more than 100,000 lines of source code, and so far as I know, LLVM haven’t implement the goal. I will propose an aggregation of exiting ideas, but I will make some improvement to increase the precision. After the project completed, LLVM will have the ability to check bounds overflow bugs in C programs.
Deliverables

In my project, I will write several passes to support the implementation of bound-checking, and one pass to implement the ultimate task of bound-checking. To elaborate on my results, I will present enough graphs or tables to show the compassion between my method and others.
Project Details

Many tools, such as ASTREE, Archer, SAFEcode, Calysto, KLEE, and Clang, can detect bounds overflows, but some are commercial, some are slow because of a very thorough check, and other can’t detect dereferences if allocations and dereferences are in different functions. I mean to a fast open-source method, which is easy to be integrated into the compilation process, to look for bounds overflow bugs. My main goal: verification speed should be fast, and making trade-off between speed and accuracy. Edvin Torok have proposed an intra-procedural analysis method to check bounds overflow bugs in his master thesis, involved in slicing and inline, but he haven’t done an inter-procedural analysis. I think summary function / (partial) transition function can help me do more accurate analysis based on his work..     
 
Perhaps with the help of summary function / (partial) transition function, verification speed will be obviously slower than that without it. If so, I want do integrate a more effective slicing method to increase the accuracy of the verification. When Facing some unforeseen difficulties or setbacks, I will discuss with my mentor, or my learning partner, because they maybe lighten me. In the worst cases, I can’t implement an effective way to check bounds overflows with inter-procedural analysis, but I can also implement some LLVM passes, which are useful for other analysis based on LLVM or other compilers, to check bounds overflow bugs with partial inter-procedural analysis with the help of inline and slicing.