We study methods that allow web sites to safely combine JavaScript
from untrusted sources. If implemented properly, lters can prevent dangerous
code from loading into the execution environment, while rewriting allows greater
expressiveness by inserting run-time checks. Wrapping properties of the execu-
tion environment can prevent misuse without requiring changes to imported
JavaScript.
Using a formal semantics for the ECMA 262-3 standard language, we prove
security properties of a subset of JavaScript, comparable in expressiveness to
Facebook FBJS, obtained by combining three isolation mechanisms. The isola-
tion guarantees of the three mechanisms are interdependent, with rewriting and
wrapper functions relying on the absence of JavaScript constructs eliminated
by language lters.