Data-Driven Synthesis of a Provably Sound Side-Channel Analysis
12/10/2021, 9am
Speaker
Abstract
The objective of my dissertation research is to develop rigorous methods and analysis tools for improving the security of software systems. I focus on a class of emerging security threats called side-channel attacks. Recent examples include Meltdown/Spectre, which are side-channel attacks that affect the vast majority of today's computers, thus highlighting their profound social and economical impact. During a side-channel attack, the adversary relies on exploiting statistical dependencies between the secret data and seemingly-unrelated non-functional properties (e.g., power consumption or execution time) of the computer.
While formal verification and program synthesis are promising techniques for detecting and mitigating power side-channel attacks, e.g., by checking and then automatically removing the statistical dependencies in software code, existing methods and tools for verification and program synthesis fall short in terms of both scalability and efficiency. That is, they are either fast but extremely inaccurate or accurate but extremely slow. To fill the gap, I am developing new methods and tools to overcome the scalability/efficiency bottlenecks. My key observation is that, to overcome the scalability/efficiency bottlenecks, we must leverage the unique characteristics of side-channel information leaks inside the software code to optimize the verification and program synthesis methods. Whilethis can be performed manually, it has the disadvantage of being labor-intensive, error-prone and sub-optimal. Thus, I propose to automate theoptimization process using a synergistic combination of rigorous logical-reasoning and machine-learning techniques. So far, I have completed the development of a data-driven, learning-based method for optimizing a security verification tool using annotated examples. The optimized tool can achieve the same empirical accuracy as state-of-the-art, hand-crafted tools while beingseveral hundred times faster.
Speaker Bio
Jingbo Wang is pursuing a Ph.D. in the Department of Computer Science at the University of Southern California (USC). Her research interests lie at the intersection of program verification and software security. She works on detecting and mitigating security vulnerabilities via program verification and synthesis techniques. She received the WiSE Merit award from USC in 2021. She was also the selected attendee of the MIT EECS Rising Star workshop, the 7thHeidelberg Laureate Forum, and the CRA-W Grad Cohort workshop.