Wed 7 Nov 2018 15:52 - 16:15 at Horizons 10-11 - Symbolic Execution and Constraint Solving Chair(s): Satish Chandra

The timing characteristics of cache, a high-speed storage between the fast CPU and the slow memory, may reveal sensitive information of a program, thus allowing an adversary to conduct side-channel attacks. Existing methods for detecting timing leaks either ignore cache all together or focus only on passive leaks generated by the program itself, without considering leaks that are made possible by concurrently running some other threads. In this work, we show that timing-leak-freedom is not a compositional property: a program that is not leaky when running alone may become leaky when interleaved with other threads. Thus, we develop a new method, named adversarial symbolic execution, to detect such leaks. It systematically explores both the feasible program paths and their interleavings while modeling the cache, and leverages an SMT solver to decide if there are timing leaks. We have implemented our method in LLVM and evaluated it on a set of real-world ciphers with 14,455 lines of C code in total. Our experiments demonstrate both the efficiency of our method and its effectiveness in detecting side-channel leaks.

Wed 7 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

15:30 - 17:00
Symbolic Execution and Constraint SolvingResearch Papers at Horizons 10-11
Chair(s): Satish Chandra Facebook
15:30
22m
Talk
Concurrency Verification with Maximal Path Causality
Research Papers
Qiuping Yi Texas A&M University, Jeff Huang Texas A&M University
15:52
22m
Talk
Adversarial Symbolic Execution for Detecting Concurrency-Related Cache Timing Leaks
Research Papers
Shengjian (Daniel) Guo Virginia Tech, Meng Wu Virginia Tech, Chao Wang USC
16:15
22m
Talk
Symbolic Execution with Existential Second-Order Constraints
Research Papers
Sergey Mechtaev National University of Singapore, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler, Abhik Roychoudhury National University of Singapore
DOI Pre-print
16:37
22m
Talk
Parameterized Model Counting for String and Numeric Constraints
Research Papers
Abdulbaki Aydin Microsoft, USA, William Eiers University of California at Santa Barbara, USA, Lucas Bang , Tegan Brennan , Miroslav Gavrilov University of California at Santa Barbara, USA, Tevfik Bultan University of California, Santa Barbara, Fang Yu National Chengchi University