Static Analysis for AJAX Intrusion Detection

Back in 2008, the group decided to really understand JavaScript. Arjun had built a static analysis for JavaScript from scratch. Being the honest chap that he is, he was forced to put the following caveat into the paper:

"We would like to formally prove that our analysis is sound. A sound analysis would guarantee that our tool will never raise a false alarm, an imporant usability concern. However, a proof of soundness would require a formal semantics for JavaScript and the DOM in browsers, and this does not exist."

This paper was our first foray into the world of analysis for real JavaScript programs. It inspired work on λJS and tractable tools for JavaScript. (paper)