Position: PhD Candidate
Current Institution: University of Southern California
Abstract: Enhancing Software Security via Scalable Verification and Program Synthesis Techniques
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. While this can be performed manually it has the disadvantage of being labor-intensive error-prone and sub-optimal. Thus I propose to automate the optimization 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 being several hundred times faster.
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 7th Heidelberg Laureate Forum and the CRA-W Grad Cohort workshop.