What do JavaScript Programs do?
Gareth Smith
Abstract:
JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts. We provide tractable reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. In this talk, we will introduce our reasoning by studying several JavaScript programs. We will demonstrate that reasoning about easy programs is easy, and reasoning about hard programs is possible. We have a strong soundness result. This means that all libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code. An immediate goal is to use our reasoning to develop a symbolic debugger for JavaScript. A long-term goal is use our reasoning about JavaScript, and previous work on reasoning about DOM, to develop secure web applications.
References:
- Towards a Program Logic for JavaScript, Gardner, Maffeis and Smith, POPL2012.
- Local Reasoning about DOM, Gardner, Smith, Wheelhouse and Zarfaty, PODS2008.
- Local Reasoning about Mashups, Gardner, Smith and Wright, VSTTE 2010.