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

Опубликовано 12 августа 2016, 0:28

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.