Prof. Chao Wang, University of Southern California
Adversarial Symbolic Execution for Detecting Timing Side-Channel Leaks
Abstract: The timing characteristics of cache, a high-speed storage between the fast CPU and the slow main memory, may reveal sensitive information of a software program, thus making it vulnerable to side-channel attacks. Existing program analysis techniques for detecting timing side-channel leaks in software either ignore the impact of cache, or focus only on passive leaks generated by the program itself, without considering leaks made possible by concurrently running multiple threads. In this work, we first show that the absence of timing side-channel leaks is not a compositional property: a thread that is not leaky when running alone may become leaky when it is interleaved with other threads. Then, we leverage KLEE to detect such leaks, by systematically exploring both feasible program paths within a thread and their interleavings with other threads.
Bio: Chao Wang is an Associate Professor of Computer Science at University of Southern California (USC). His research interests are in software engineering and formal methods, with emphasis on logic, verification and automated reasoning. He develops techniques for principled design of software systems to improve safety and security. He published a book, two edited books, and more than 100 research papers. He chaired the program committees of CAV 2020 and AVTA 2018, two premier conferences in formal methods, and served on the program committees of many conferences such as ICSE, FSE, ASE, and ISSTA. He is also an Associate Editor of IEEE Transactions on Software Engineering. He received many awards, including the U.S. Office of Naval Research (ONR) Young Investigator award (2013) and National Science Foundation (NSF) CAREER award (2012), the ACM SIGSOFT Distinguished Paper award (2018 and 2010), FMCAD Best Paper award (2013), and Best Paper of the Year award from ACM Transactions on Design Automation of Electronic Systems (2008).