Automated Analysis of Security-Critical JavaScript APIs
Abstract
JavaScript is widely used to provide client-side functionality in Web
applications. To provide services ranging from maps to advertisements,
Web applications may incorporate untrusted JavaScript code from third
parties. The trusted portion of each application may then expose an
API to untrusted code, interposing a reference monitor that mediates
access to security-critical resources. However, a JavaScript reference
monitor can only be effective if it cannot be circum- vented through
programming tricks or programming language idiosyncracies. In order to
verify complete mediation of critical resources for applications of
interest, we define the semantics of a restricted version of JavaScript
devised by the ECMA Standards committee for isolation purposes, and
develop and test an automated tool that can soundly establish that a
given API cannot be circumvented or subverted. Our tool reveals a
previously-undiscovered vulnerability in the widely-examined Yahoo!
ADsafe filter and verifies confinement of the repaired filter and other
examples from the Object-Capability literature.
applications. To provide services ranging from maps to advertisements,
Web applications may incorporate untrusted JavaScript code from third
parties. The trusted portion of each application may then expose an
API to untrusted code, interposing a reference monitor that mediates
access to security-critical resources. However, a JavaScript reference
monitor can only be effective if it cannot be circum- vented through
programming tricks or programming language idiosyncracies. In order to
verify complete mediation of critical resources for applications of
interest, we define the semantics of a restricted version of JavaScript
devised by the ECMA Standards committee for isolation purposes, and
develop and test an automated tool that can soundly establish that a
given API cannot be circumvented or subverted. Our tool reveals a
previously-undiscovered vulnerability in the widely-examined Yahoo!
ADsafe filter and verifies confinement of the repaired filter and other
examples from the Object-Capability literature.
Research Areas
