Copenhagen Programming Language Seminar

Confining the Ghost in the Machine: Using Types to Secure JavaScript Sandboxing

Arjun Guha
Brown University

November 24th, 2011, 15:00 - 16:00
DIKU, Universitetsparken 1, Meeting room A+B (2-0-04 and 2-0-06)


The commercial Web depends on combining content, especially advertisements, from sites that do not trust one another. Because this content can contain malicious code, several corporations and researchers have designed JavaScript sandboxing techniques (e.g., ADsafe, Caja, and Facebook JavaScript). These sandboxes depend on static restrictions, transformations, and libraries that perform dynamic checks. But, do they actually work?

We tackle the problem of proving the security of these sandboxes. Our technique is to employ a JavaScript type-checker to encode and verify the properties of sandboxes. The type-checker is lightweight, efficient, and operates on actual source. I will discuss our verification of ADsafe, which revealed several bugs and other weaknesses.

Joint work with Spiridon Eliopoulos, Shriram Krishnamurthi, and Joe Gibbs Politz.

Short bio:
Arjun Guha is a graduate student of Computer Science at Brown University. His work focuses on verifying existing Web programs and designing new programming languages for the Web. He co-developed Flapjax (a reactive programming language), LambdaJS (a semantics for JavaScript), and Google Belay (a cloud authorization and sharing protocol).

Scientific host: Fritz Henglein Administrative host:Jette Møller. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, DTU, ITU, and RUC.
COPLAS is part of the FIRST Research School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org