Reactive non-interference for the browser: extended version

Given a partially ordered set (poset) of security levels, and a labelling of inputs and outputs with such levels, non-interference (or secure information flow) is a security property expressing that outputs of level l only depend on inputs that are labelled with a level smaller than l. In other words, there is no information flow from high (confidential) levels, to low (public) levels. For web browsers, as programs that interact intensely with a variety of principals, non-interference is an interesting security property, and several authors have studied how enforcement mechanisms for it can be incorporated in a browser, usually focusing on specific scenarios such as securing the flow of information towards advertisements, or securing mashups. In this paper, we investigate the suitability of noninterference as a replacement for the baseline security policy of a browser, the same-origin-policy. We propose an enforcement mechanism that can enforce non-interference with respect to a broad class of security level posets for the full browser. We prove the security and precision of the enforcement mechanism, and implement it for the Featherweight Firefox browser model. Next, we investigate what security level posets are useful in a web context, and how inputs and outputs to the browser should be labelled. Somewhat surprisingly, our analysis shows that useful policies (which approximate but improve the current same-origin-policy) can be defined without any support for declassification.nrpages: 38status: publishe