Software side-channel attacks are able to recover confidential information by observing non-functional computation characteristics of program execution such as elapsed time, amount of allocated memory, or network packet size. The ability to automatically determine the amount of information that a malicious user can gain through side-channel observations allows one to assess the security of an application. Since most software that accesses confidential information leaks some amount of information through side channels, it is important to quantify the amount of leakage in order to detect vulnerabilities.
In this talk, I will discuss automated techniques that prove the vulnerability of a given program to side-channel attacks by synthesizing attacks that recover confidential information. In particular, I will present methods for synthesizing adaptive side-channel attack steps dynamically while taking system noise into account. This approach can automatically produce a sequence of inputs which extracts a secret value from a program. If an attack is found, it serves as a proof of program vulnerability. The approach I will present makes use of symbolic execution, model counting, numeric optimization, and quantitative information flow for automated attack synthesis.