Quantifying Information Leakage Using Model Counting Constraint Solvers.

This paper provides a brief overview of recent results in quantitative information flow analysis, model counting constraints solvers, side-channel analysis and attack synthesis. By combining model counting constraints solvers with symbolic execution it is possible to quantify the amount of information that a program leaks about a secret input. As discussed below, this type of analysis is crucial for detection and analysis of side channel vulnerabilities.