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 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | Secure and SoundISSTA Technical Papers at Zurich II Chair(s): Cristian Cadar Imperial College London | ||
11:00 20mTalk | Lightweight Verification of Array Indexing ISSTA Technical Papers Martin Kellogg University of Washington, Seattle, Vlastimil Dort Charles University, Suzanne Millstein University of Washington, Michael D. Ernst University of Washington, USA | ||
11:20 20mTalk | Eliminating Timing Side-channel Leaks Using Program Repair ISSTA Technical Papers Meng Wu Virginia Tech, Shengjian (Daniel) Guo Virginia Tech, Patrick Schaumont Virginia Tech, Chao Wang University of Southern California | ||
11:40 20mTalk | Symbolic Path Cost Analysis for Side-Channel Detection ISSTA Technical Papers Tegan Brennan , Seemanta Saha University of California Santa Barbara, Tevfik Bultan University of California, Santa Barbara, Corina S. Păsăreanu NASA Ames Research Center | ||
12:00 20mTalk | Safe and Sound Program Analysis with Flix ISSTA Technical Papers | ||
12:20 10m | Q&A in groups ISSTA Technical Papers | ||