This work is licensed under the Creative Commons Attribution License. Quantifying Side-Channels in RSA and AES

Quantitative information-flow analysis (QIF) offers methods for reasoning about information-theoretic confidentiality properties of programs. The measures used by QIF are associated with operational secu-rity guarantees such as lower bounds for the effort required to determine a secret by exhaustive search. Moreover, they can be concisely expressed in terms of programming language semantics, which enables one to leverage existing program analysis techniques for their computation. This talk reports on a line of work on techniques for the QIF analysis of cache and timing side-channels in implementations of cryptographic algorithms. Attacks exploiting these side-channels are highly effective [2, 3, 7], and most countermeasures against them are only heuristic (i.e. they defeat particular attacks, but are not backed up by a formal security guarantee). The talk will show how QIF techniques can be used for establishing upper bounds for the side-channel leakage of implementations of the RSA and AES cryptosystems, based on formal models of the underlying platforms. For RSA, I will present work [4, 6] on the QIF analysis of input blinding, the state-of-the-art coun-termeasure against timing attacks. The analysis reveals that blinding offers strong guarantees whenever the range of possible timing measurements is small. Based on this insight, we propose the combina-tion of blinding and discretization of execution times as the first countermeasure (beyond constant-tim