Information-flow analysis is a powerful technique for reasoning about the sensitive information that is exposed by a program during execution. In this talk, I will present the first automatic method for information-flow analysis that discovers what information is leaked and computes its comprehensive quantitative interpretation. The leaked information is characterized by an equivalence relation on secret inputs, and is represented by a logical assertion over the corresponding program variables. For quantifying the leaked information, we determine the number of equivalence classes and their sizes. This data provides the basis for computing a comprehensive set of information-theoretic quantities. We provide an implementation of our method that builds upon existing tools for program verification and model counting. I will give an outlook on an extension of our method based on randomization and approximation techniques.

Subsequently, I will report on the quantitative information-flow analysis of cryptosystems that are protected by blinding, the state-of-the-art countermeasure against timing attacks. The analysis exhibits the modifications needed to make a blinded implementation provably secure, in the sense that the number of timing measurements required for recovering a significant number of key bits is too large for any realistic attacker. We use this result to propose the first practical countermeasure against timing attacks that is backed up by a formal security guarantee.

The talk describes joint work with Michael Backes, Andrey Rybalchenko (automation), and Markus Duermuth (timing attacks).