ADsafety: Type-Based Verification of JavaScript Sandboxing
Joe Gibbs Politz, Spiridon Aristides Eliopoulos, Arjun Guha, and Shriram Krishnamurthi, Brown University
Web sites routinely incorporate JavaScript programs from several sources into a single page. These sources must be protected from one another, which requires robust sandboxing. The many entry-points of sandboxes and the subtleties of JavaScript demand robust verification of the actual sandbox source. We use a novel type system for JavaScript to encode and verify sandboxing properties. The resulting verifier is lightweight and efficient, and operates on actual source. We demonstrate the effectiveness of our technique by applying it to ADsafe, which revealed several bugs and other weaknesses.
Open Access Media
USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.
author = {Joe Gibbs Politz and Spiridon Aristides Eliopoulos and Arjun Guha and Shriram Krishnamurthi},
title = {{ADsafety}: {Type-Based} Verification of {JavaScript} Sandboxing},
booktitle = {20th USENIX Security Symposium (USENIX Security 11)},
year = {2011},
address = {San Francisco, CA},
url = {https://www.usenix.org/conference/usenix-security-11/adsafety-type-based-verification-javascript-sandboxing},
publisher = {USENIX Association},
month = aug
}