TY - GEN
T1 - Lightweight verification of array indexing
AU - Kellogg, Martin
AU - Dort, Vlastimil
AU - Millstein, Suzanne
AU - Ernst, Michael D.
N1 - Publisher Copyright:
© 2018 Association for Computing Machinery.
PY - 2018/7/12
Y1 - 2018/7/12
N2 - 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 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 verification 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.
AB - 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 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 verification 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.
KW - Checker Framework
KW - Index Checker
KW - Pluggable type systems
UR - http://www.scopus.com/inward/record.url?scp=85051518076&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85051518076&partnerID=8YFLogxK
U2 - 10.1145/3213846.3213849
DO - 10.1145/3213846.3213849
M3 - Conference contribution
AN - SCOPUS:85051518076
T3 - ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis
SP - 3
EP - 14
BT - ISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis
A2 - Bodden, Eric
A2 - Tip, Frank
PB - Association for Computing Machinery, Inc
T2 - 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018
Y2 - 16 July 2018 through 21 July 2018
ER -