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 quantitatively 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 addition, one can prove that a program is vulnerable to side-channel attacks by synthesizing attacks that recover confidential information.
In this presentation, I will propose methods for synthesizing adaptive side-channel attack steps. I will cover two approaches. The first approach is fully static and pre-computes an attack strategy, and allows us to quantify the expected information gain for an adaptive attacker. The second approach synthesizes side-channel attack steps online. This second approach can produce an attack sequence which extracts a secret value from a program. If an attack is found, it serves as a proof of program vulnerability. Both techniques use symbolic execution, model counting, numeric optimization, and ideas from quantitative information flow.