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

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