Formal Semantics
The small-step operational semantics of JavaScript is here. This was developed in Stanford in 2008, and follows closely the ECMAScript 3 standard. It covers almost all of the standard.
The big-step operational semantics of a core of JavaScript has been formalized in COQ here. This is being developed at Imperial College London, INRIA Paris and INRIA Rennes. We are currently working on extending the semantics to more constructs, and cover ECMAScript 5.
JavaScript Security
The page of the Foundations of Secure Web Programming project based at Imperial College is here.