ADsafety: Type-Based Verification of JavaScript Sandboxing

TL;DR

This paper introduces ADsafety, a novel type-based verification method for JavaScript sandboxing, ensuring security properties are maintained across multiple sources in web pages.

Contribution

It presents a lightweight, source-level verifier using a new type system to verify sandboxing properties in JavaScript, demonstrated on ADsafe.

Findings

Revealed several bugs in ADsafe

Identified weaknesses in existing sandboxing approaches

Proved the effectiveness of the type-based verification method

Abstract

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.