Trustworthy Software Enabled by Program Analysis and Synthesis

Abstract: Security, robustness, and fairness are all important non-functional properties of critical systems, such as software applications in autonomous driving, healthcare, and finance. Unlike functional correctness, which has been the subject of extensive research, techniques that can formally guarantee these non-functional properties are still severely lacking. In this talk, I will present two techniques based on data-driven synthesis and program analysis for improving security and fairness. The first one is a new method for detecting side-channel leaks, which are a class of emerging security threats that exploit the statistical dependencies between secret data and the physical characteristics of the computing devices. Instead of hand-crafting the analysis algorithm and then proving its soundness, our technique synthesizes the algorithm automatically while guaranteeing that it is sound by construction. The second technique is for synthesizing a machine learning model with a fairness guarantee, which is important for applications that are increasingly used to make socially sensitive decisions. Finally, I will talk about my research in the future, which will focus on providing formal guarantees of security, robustness, and fairness to other emerging applications.

Bio:  Jingbo Wang is a Ph.D. candidate in the Department of Computer Science at the University of Southern California. Her research is at the intersection of software engineering and formal methods, with an emphasis on developing rigorous program analysis and synthesis techniques to improve the security, robustness, and fairness of software systems.  Results of her work have been published at top venues such as ICSE, ESEC/FSE, ASE, CAV, and FMCAD, and have been presented at venues such as the MIT EECS Rising Stars workshop. She also received the USC WiSE Merit Research Award, and was selected as a Young Researcher for the Heidelberg Laureate Forum.