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

Program development tools such as bug finders, build automation tools, compilers, debuggers, integrated development environments, and refactoring tools increasingly rely on static analysis techniques to reason about program behavior. Implementing such static analysis tools is a complex and difficult task with concerns about safety and soundness. Safety guarantees that the fixed point computation – inherent in most static analyses – converges and ultimately terminates with a deterministic result. Soundness guarantees that the computed result over-approximates the concrete behavior of the program under analysis. But how do we know if we can trust the result of the static analysis itself? Who will guard the guards?

In this paper, we propose the use of automatic program verification techniques based on symbolic execution and SMT solvers to verify the correctness of the abstract domains used in static analysis tools. We implement a verification toolchain for Flix, a functional and logic programming language tailored for the implementation of static analyses. We apply this toolchain to several abstract domains. The experimental results show that we are able to prove 99.5% and 96.3 of the required safety and soundness properties, respectively.

Mon 16 Jul
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Secure and SoundISSTA Technical Papers at Zurich II
Chair(s): Cristian CadarImperial College London
11:00
20m
Talk
Lightweight Verification of Array Indexing
ISSTA Technical Papers
Martin KelloggUniversity of Washington, Seattle, Vlastimil DortCharles University, Suzanne MillsteinUniversity of Washington, Michael D. ErnstUniversity of Washington, USA
11:20
20m
Talk
Eliminating Timing Side-channel Leaks Using Program Repair
ISSTA Technical Papers
Meng WuVirginia Tech, Shengjian (Daniel) GuoVirginia Tech, Patrick SchaumontVirginia Tech, Chao WangUniversity of Southern California
11:40
20m
Talk
Symbolic Path Cost Analysis for Side-Channel Detection
ISSTA Technical Papers
Tegan Brennan, Seemanta SahaUniversity of California Santa Barbara, Tevfik BultanUniversity of California, Santa Barbara, Corina S. PăsăreanuNASA Ames Research Center
12:00
20m
Talk
Safe and Sound Program Analysis with Flix
ISSTA Technical Papers
Magnus MadsenAalborg University, Ondřej LhotákUniversity of Waterloo, Canada
12:20
10m
Q&A in groups
ISSTA Technical Papers