Internet traffic is exposed to potential eavesdroppers. Standard encryption mechanisms do not provide sufficient protection: Features such as packet sizes and numbers remain visible, opening the door to so-called side-channel attacks against web traffic. In this talk, we present a novel framework for deriving formal security guarantees against traffic side-channels. We present a model which captures important characteristics of web traffic, and we define measures of security based on quantitative information flow. To enable the evaluation of real-life web applications, we propose algorithms for the efficient derivation of security guarantees, based on properties of Markov chains. We demonstrate the utility of our techniques in two case studies.

This is joint work with Boris Köpf and Michael Backes.