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

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. How can we be sure that they work?

We tackle the problem of proving the security of these sandboxes. Our technique depends on creating specialized types to characterize the properties of the sandboxes, exploiting the structure of the checks contained in the libraries. The resulting checkers work on actual JavaScript code that is effectively unaltered; I will focus on our application to Yahoo!’s ADsafe. We establish soundness using our semantics for JavaScript, which has been tested for conformity against real implementations.

Joint work with Arjun Guha and Joe Politz.

Speaker Details

Shriram Krishnamurthi is an Associate Professor of Computer Science at Brown University. He currently focuses on securing various attack surfaces on the Web. With collaborators and students, he has created several influential systems: DrRacket (programming environment), Margrave (access control policy analyzer), FrTime and Flapjax (reactive programming languages), and Lambda-JS and Typed JavaScript (semantics and types for JavaScript). He is a co-author of “How to Design Programs” and author of “Programming Languages: Application and Interpretation”. He coordinates the Program by Design and Bootstrap outreach programs. He holds an NSF CAREER Award and Brown’s Henry Merritt Wriston Fellowship for distinguished contribution to undergraduate education, and has authored twelve papers recognized by program committees.

Date:
Speakers:
Shriram Krishnamurthi
Affiliation:
Brown University
    • Portrait of Jeff Running

      Jeff Running