Quantitative information-flow analysis (QIF) offers methods for establishing bounds on the information exposed by a system during execution. In this talk, I present past and ongoing work on techniques for the QIF of side-channels in implementations of AES and RSA. For RSA, I will present work on the QIF of blinding, the state-of-the-art countermeasure against timing attacks. The analysis reveals that one can obtain strong guarantees whenever the range of possible timing measurements is small. Based on this result, we propose the combination of blinding and discretization of execution times as the first countermeasure against timing attacks that is provably secure. Our experimental results on a 1024-bit RSA implementation demonstrate the cost-efficiency of this countermeasure. For AES, I will present ongoing work on a method for the automatic QIF of cache side-channels. At the heart of this method is a novel technique for efficient counting of concretizations of abstract cache-states that enables connecting techniques for static cache-analysis and QIF. We implement this counting procedure on top of the AbsInt TimingExplorer, the most advanced engine for static cache-analysis and perform a case study where we derive upper bounds on the cache leakage of a 128-bit AES executable.
The talk will begin with a gentle introduction of the basic QIF tools, i.e. no prior knowledge is required.