Software side-channel attacks are able to recover confidential information by observing non-functional computation characteristics such as execution 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 this talk, I will discuss the relevant literature of three areas related to this problem. First, automated software verification techniques such as symbolic execution provide a means of summarizing program behavior. Second, results from the field of quantitative information flow give an information theoretic foundation on which to build a quantitative analysis framework, which makes use of program summaries. Third, the combinatorial methods of model counting enable us to effectively implement quantitative program analysis. Over the course of the talk, I will argue that by combining these three areas we can automatically detect and quantify a program’s vulnerability to side-channel attacks.