Programmers often view the computing devices as black-boxes, but real computers leak information of the software they execute through various side channels, e.g., variations in power dissipation, radiation, execution time, and sound signature of the processor. Side-channel information may be exploited by adversaries. For example, while cryptographic algorithms may be secure against hundreds of years of brute-force attacks, their actual implementations may be broken in hours or even minutes in the presence of side-channel leaks. In this talk, I will explain how formal verification and program synthesis can be used to (1) detect side-channel leaks of software code running on IoT devices, (2) prove the absence of side-channel leaks, and (3) transform software to eliminate such leaks. We use power side-channel leaks in cryptographic software as examples, but the underlying techniques are applicable to other types of side channels and software systems as well.

Chao Wang is an Associate Professor of Computer Science at University of Southern California. He received his PhD degree from University of Colorado at Boulder in 2004, worked as a Research Staff Member at NEC Labs from 2004 to 2011, and an Assistant Professor at Virginia Tech from 2011 to 2016. His research is in software engineering and formal methods, with focus on developing methods and tools for improving the safety and security of software. He has published a book and more than 70 papers. He received an ONR Young Investigator award in 2013 and an NSF CAREER award in 2012. He also received the FMCAD Best Paper award in 2013, ACM SIGSOFT Distinguished Paper award in 2010, ACM TODAES Best Journal Paper of the Year award in 2008, NEC Labs of America Technology Commercialization Award in 2006, and ACM SIGDA Outstanding PhD Dissertation award in 2004.