Lightweight Verification of Array Indexing
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 certifies, at compile time, that array accesses in the program will be in-bounds. The type system consists of several cooperating hierarchies of dependent types, specialized to the domain of array bounds-checking. Programmers can write type annotations at procedure boundaries, allowing modular verification at a cost that scales linearly with program size.
We implemented our type system for Java in a tool we call Charles. We evaluated Charles on over 100,000 lines of open-source code and discovered array access errors even in well-tested, industrial projects such as Google Guava.
Mon 16 Jul
|11:00 - 11:20|
|11:20 - 11:40|
|11:40 - 12:00|
|12:00 - 12:20|
|12:20 - 12:30|