Abstrakt
In languages like C, out-of-bounds array accesses lead to security vulnerabilities and crashes. Even in managed languages like Java, which check array bounds at run time, out-of-bounds accesses cause exceptions that terminate the program.
We present a lightweight type system that certifes, at compile time, that array accesses in the program are in-bounds. The type system consists of several cooperating hierarchies of dependent types, specialized to the domain of array bounds-checking.
Programmers write type annotations at procedure boundaries, allowing modular verifcation at a cost that scales linearly with program size. We implemented our type system for Java in a tool called the Index Checker.
We evaluated the Index Checker on over 100,000 lines of open-source code and discovered array access errors even in well-tested, industrial projects such as Google Guava.