Array Bounds Model Checking in C Code Based on Predicate Abstraction

As C program compilers do not check the array bounds during compiling, array index out of bounds attacks cause serious security problems. Array bound checking is becoming more and more important, however, original array bound checking, which needs programmers manual working, wastes too much time. In this paper, we propose a strategy to address this issue for C code. In this strategy, we use predicate abstraction in the generated CFG (control flow graph), then the CFG is translated to the SMV model using a translating algorithm. Finally, we use the model checking tool-nuXmv to check the array bound. If the array is out of bound, the nuXmv will give the counter-examples.