Write a Blog >>
ISSTA 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA
Mon 16 Jul 2018 11:00 - 11:20 at Zurich II - Secure and Sound Chair(s): Cristian Cadar

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

issta-2018-Technical-Papers
11:00 - 12:30: ISSTA Technical Papers - Secure and Sound at Zurich II
Chair(s): Cristian CadarImperial College London
issta-2018-Technical-Papers11:00 - 11:20
Talk
Martin KelloggUniversity of Washington, Seattle, Vlastimil DortCharles University, Suzanne MillsteinUniversity of Washington, Michael D. ErnstUniversity of Washington, USA
issta-2018-Technical-Papers11:20 - 11:40
Talk
Meng WuVirginia Tech, Shengjian (Daniel) GuoVirginia Tech, Patrick SchaumontVirginia Tech, Chao WangUniversity of Southern California
issta-2018-Technical-Papers11:40 - 12:00
Talk
Tegan Brennan, Seemanta SahaUniversity of California Santa Barbara, Tevfik BultanUniversity of California, Santa Barbara, Corina S PasareanuNASA Ames Research Center
issta-2018-Technical-Papers12:00 - 12:20
Talk
Magnus MadsenAalborg University, Ondřej LhotákUniversity of Waterloo, Canada
issta-2018-Technical-Papers12:20 - 12:30