Preventing Side-Channel Leaks in Web Traffic: A Formal Approach
Michael Backes, Goran Doychev, Boris Köpf · 2013
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. This paper develops a framework for the derivation of formal 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. Leaning on the well-studied properties of these measures, we provide an assembly kit for countermeasures and their security guarantees, and we show that security guarantees are preserved on lower levels of the protocol stack. We further propose a novel technique for the efficient derivation of security guarantees for web applications. The key novelty of this technique is that it provides guarantees that cover all execution paths in a web application, i.e. it achieves completeness. We demonstrate the utility of our techniques in two case studies, where we derive formal guarantees for the security of a medium-sized regionallanguage Wikipedia and an auto-complete input field. 1