Journal of Computer Security

Secure Multi-Execution (SME) is a precise and general information flow control mechanism that was claimed to be a good fit for implementing information flow security in browsers. We validate this claim by developing FlowFox, the first fully functional web browser that implements an information flow control mechanism for web scripts based on the technique of secure multi-execution. We provide evidence for the security of FlowFox by proving non-interference for a formal model of the essence of FlowFox, and by showing how it stops real attacks. We provide evidence of usefulness by showing how FlowFox subsumes many ad-hoc script-containment countermeasures developed over the last years. An experimental evaluation on the Alexa top-500 web sites provides evidence for compatibility, and shows that FlowFox is compatible with the current web, even on sites that make intricate use of JavaScript.

The performance and memory cost of FlowFox is substantial (a performance cost of around 20% on macro benchmarks for a simple two-level policy), but not prohibitive. Our prototype implementation shows that information flow enforcement based on secure multi-execution can be implemented in full-scale browsers. It can support powerful, yet compatible policies refining the same-origin-policy in a way that is compatible with existing websites.

Web pages routinely incorporate JavaScript code from third-party sources. However, all code in a page runs in the same security context, regardless of provenance. When Web pages incorporate third-party JavaScript without any checks, as many do, they open themselves to attack. A third-party can trivially inject malicious JavaScript into such a page, causing all manner of harm. Several such attacks have occurred in the wild on prominent, commercial Web sites.

A Web sandbox mitigates the threat of malicious JavaScript. Several Web sandboxes employ closely related language-based techniques to maintain backward-compatibility with old browsers and to provide fine-grained control. Unfortunately, due to the size and complexity of the Web platform and several subtleties of JavaScript, language-based sandboxing is hard and the Web sandboxes currently deployed on major Web sites do not come with any formal guarantees. Instead, they are routinely affected by bugs that violate their intended sandboxing properties.

This article presents a type-based approach to verifying Web sandboxes, using a JavaScript type-checker to encode and verify sandboxing properties. We demonstrate our approach by applying it to the ADsafe Web sandbox. Specifically, we verify several key properties of ADsafe, falsify one intended property, and find and fix several vulnerabilities, ultimately providing a proof of ADsafe's safety.

Due to their high practical impact, Cross-Site Scripting (XSS) attacks have attracted a lot of attention from the members of security community worldwide. In the same way, a plethora of more or less effective defense techniques have been proposed, addressing both causes and effects of XSS vulnerabilities. As a result, an adversary often can no longer inject or even execute arbitrary scripting code in several real-life scenarios. In this article, we examine an attack surface that remains after XSS and similar scripting attacks are supposedly mitigated by preventing an attacker from executing JavaScript code. We address the question of whether an attacker really needs to execute JavaScript or similar functionality to perform attacks aiming for information theft. The surprising result is that an attacker can abuse Cascading Style Sheets (CSS) in combination with other Web techniques like plain HTML, inactive SVG images, or font files. Having employed several case studies, we discuss so called scriptless attacks and demonstrate that an adversary might not need to execute code to preserve his ability to extract sensitive information from well-protected websites. More precisely, we show that an attacker can use seemingly benign features to build side-channel attacks that measure and exfiltrate almost arbitrary data displayed on a given webpage. We conclude this article with a discussion of potential mitigation techniques against this class of attacks. In addition, we have implemented a browser patch that enables a website to make a vital determination as to being loaded in a detached view or a pop-up window. This approach proves useful for prevention of certain types of attacks we here discuss.

Social sign-on and social sharing are becoming an ever more popular feature of web applications. This success is largely due to the APIs and support offered by prominent social networks, such as Facebook, Twitter and Google, on the basis of new open standards such as the OAuth 2.0 authorization protocol. A formal analysis of these protocols must account for malicious websites and common web application vulnerabilities, such as cross-site request forgery and open redirectors. We model several configurations of the OAuth 2.0 protocol in the applied pi-calculus and verify them using ProVerif. Our models rely on WebSpi, a new library for modeling web applications and web-based attackers that is designed to help discover concrete attacks on websites. To ease the task of writing formal models in our framework, we present a model extraction tool that automatically translates programs written in subsets of PHP and JavaScript to the applied pi-calculus. Our approach is validated by finding dozens of previously unknown vulnerabilities in popular websites such as Yahoo and WordPress, when they connect to social networks such as Twitter and Facebook.