Language-based Isolation of Untrusted JavaScript

Ankur Taly

In this talk, I will present a language based mechanism for safely incorporating untrusted third-party JavaScript code on a trusted hosting page.

JavaScript is widely used to provide client-side functionality in web applications. In admitting potentially untrusted JavaScript into such applications, security depends on shielding security-critical portions of the application from untrusted JavaScript code. This is typically done using a combination of an API and a sandbox for untrusted code. The goal of the API is to encapsulate all security-critical resources thereby providing mediated/controlled access to them. The goal of the sandbox is to restrict third-party code so that it can side-effect host page resources only by invoking methods on the API. In order to prove corectness of this approach, it is important to verify that the no interleaving of calls to the API methods can return a direct reference to any security-critical resource. We call this the "API Encapsulation Problem".

The talk is divided into two parts. In this first part of this talk, I will present some progress that we made in designing provably-safe sandboxes for the present-version of JavaScript, which conforms to the 3rd edition of the ECMA262 spec (ES3). I will then argue how certain idiosyncratic semantic features of ES3 JavaScript pose significant hurdles to solving the API Encapsulation Problem. In the second part of the talk, I will present our work on JavaScript conforming to the recently released 5th edition of the ECMA262 spec (ES5). The 5th edition of the spec fixes a large number of the semantic inconsistencies of the 3rd edition, thereby making the language more amenable to static analysis. I will present a safe subset of ES5 JavaScript and define a safe sandbox for untrusted code written in it. Next I will present an automated and provably sound procedure for verifying safe encapsulation of security-critical resources by a given API. Finally, I will present some results obtained by running a tool based on our procedure on certain benchmark examples. In particular, I will present a previously unknown attack that our tool found on the well-known Yahoo! AdSafe advertisement filter, and a fix for the attack that allows the tool to prove correctness of the filter.

Joint Work with John Mitchell, Ulfar Erlingsson, Mark Miller, Jasvir Nagra and Sergio Maffeis.