Over the past several years, we've developed semantics foundations for JavaScript, built tools atop these foundations, and applied these tools to Web security problems. We've recently started tackling other Web technologies as well. All our work is open source and available from this website.

Semantic Foundations

S5: an executable semantics for modern JavaScript
λ_JS: an executable semantics for JavaScript (circa 2009)
λ_evt: an executable model of event dispatch in Web browsers

Tools

TeJaS: a family of type systems for JavaScript
Strobe: a typechecker for JavaScript
SS5: a symbolic evaluator for JavaScript

Applications

Private-browsing types: Verifying Firefox extensions' compliance with private-browsing mode
jQuery-types: a typechecker for jQuery client programs
ADsafety: verifying language-based Web sandboxes
Static Analysis for Intrusion Detection: finding attacks on AJAX-based applications
Flapjax: a language and library for reactive web applications

Media

Check out this brief video, presented at the JavaScript Tools Conference, that gives an overview of our work: