Approaches to JavaScript Security

This is, as best as I can give right now, an exhaustive enumeration of all the different approaches to JavaScript security.

• Source Translation.
  Does a source-to-source translation of JS into a secure subset. The technique is used to jail an included javascript, passing to it only those references to the outside world that it absolutely needs, and preventing it from following reference chains to an outside environment.
  Pros: flexible, follows the object capabilities model, references passed in can implement security monitoring.
  Cons: requires parsing the included script, disallows some JS forms (eval), not much can be done if the included script was written in a way that required passing in more authority than is needed.
  Used by: Caja, Jacaranda, FBJS, ADSafe
• Security Typing.
  Since non-interference can be proved within a sufficiently powerful (and convenient) typing system, we naturally reach for a language solution.
  Pros: the type system can prove the code obeys non-interference
  Cons: crufty syntax introduced for label types, label types difficult to model (polymorphic labels, subtyping, tracking the program counter label, etc), programmer must simultaneously satisify two type systems (admissible program lies in the intersection of orthogonal type systems), requires static type system
  Used by: JiF
• Bytecode Instrumentation.
  Addition of security bytecodes, and necessary modifications to an existing VM so that it ensures non-interference dynamically.
  Pros: works for dynamic languages, fails only on code that actually tries to leak (rather than rejecting code that might leak)
  Cons: difficult to implement, runtime slowdown
  Used by: JSFlow (my project)
• Bytecode Typing.
  Perform security typing on the bytecode instead of on the source.
  Pros: a verifier can refuse code that might leak when that code is loaded (could support eval, by staging the non-interference proofs), this verifier could itself be proved (if implemented in something like Coq)
  Cons: bytecode has less knowledge than the source text (although, with JavaScript the parser could annotate the bytecode with security-related hints, or techniques for typing SSA could also be used), intrepeter produced by Coq would almost certainly underperform.
  Used by: ???
• Bytecode Translation.
  Similar to the secure source subset, but now we parse JavaScript into a bytecode that’s secure by construction (then execute it on a secure VM).
  Pros: The bytecode/VM can be based on a proved core language (such as Flanagan and Austin’s lambda-info)
  Cons: No such VM exists (could be a research project unto itself), would have to implement a JS source-to-secure bytecode translator, and interfacing the secure VM to a browser would be very onerous.
  Used by: ???

In general, I think that the approach we currently use gives the best trade-off in terms of implementation detail, client-visible changes, and implementation effort. However, because I happen to have acquired paranoia (one of the side-effects of working with the security conscious), I find that I cannot completely trust that our implementation behaves as desired. In particular, I wish to have a formal proof that we handle all cases appropriately. I see two major obstacles: (1) Giving a full and complete specification of JS is tedious and itself error-prone, but has been done by hand, and (2) having a proof on one hand, and an implementation on the other does not guarantee that the implementation meets the proof, while an auto-generated implementation from the proof is a no-go because of both performance and integration.