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:40 - 12:00 at Zurich II - Secure and Sound Chair(s): Cristian Cadar

Side-channels in software are an increasingly significant threat to the confidentiality of private user information, and the static detection of such vulnerabilities is a key challenge in secure software development. In this paper, we introduce a new technique for scalable detection of side-channels in software. Given a program and a cost model for a side-channel (such as time or memory usage), we decompose the control flow graph of the program into nested branch and loop components, and compositionally assign a symbolic cost expression to each component. Symbolic cost expressions provide an over-approximation of all possible observable cost values that components can generate. Queries to a satisfiability solver on the difference between possible cost values of a component allow us to detect the presence of imbalanced paths (with respect to observable cost) through the control flow graph. When combined with taint analysis that identifies conditional statements that depend on secret information, our technique answers the following question: Does there exist a pair of paths in the program’s control flow graph, differing only on branch conditions influenced by the secret, that differ in observable side-channel value by more than some given threshold? Additional optimization queries allow us to identify the minimal number of loop iterations necessary for the above to hold or the maximal cost difference between paths in the graph. We perform symbolic execution based feasibility analyses to eliminate control flow paths that are infeasible. We implemented our techniques in a prototype, and we demonstrate its favourable performance against state-of-the-art tools as well as its effectiveness and scalability on a set of sizable, realistic Java server-client and peer-to-peer applications.

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 - 11:20
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 - 11:40
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 - 12:00
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 PasareanuNASA Ames Research Center
12:00 - 12:20
Safe and Sound Program Analysis with Flix
ISSTA Technical Papers
Magnus MadsenAalborg University, Ondřej LhotákUniversity of Waterloo, Canada
12:20 - 12:30
Q&A in groups
ISSTA Technical Papers