Lightweight verification of array indexing

Martin Kellogg, Vlastimil Dort, Suzanne Millstein, Michael D. Ernst

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis
EditorsEric Bodden, Frank Tip
PublisherAssociation for Computing Machinery, Inc
Pages3-14
Number of pages12
ISBN (Electronic)9781450356992
DOIs
StatePublished - Jul 12 2018
Externally publishedYes
Event27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018 - Amsterdam, Netherlands
Duration: Jul 16 2018Jul 21 2018

Publication series

NameISSTA 2018 - Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

Conference

Conference27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018
Country/TerritoryNetherlands
CityAmsterdam
Period7/16/187/21/18

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Software
  • Computer Science Applications

Keywords

  • Checker Framework
  • Index Checker
  • Pluggable type systems

Fingerprint

Dive into the research topics of 'Lightweight verification of array indexing'. Together they form a unique fingerprint.

Cite this