Write a Blog >>
ISSTA 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA 2018
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

Displayed 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
20m
Talk
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
20m
Talk
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
20m
Talk
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
20m
Talk
Safe and Sound Program Analysis with Flix
ISSTA Technical Papers
Magnus Madsen Aalborg University, Ondřej Lhoták University of Waterloo, Canada
12:20
10m
Q&A in groups
ISSTA Technical Papers