Taming JavaScript with F*

Presented as part of the 2013 HCSS conference.

ABSTRACT:

Traditionally confined to the web browser, JavaScript can now be found on servers running Node.js, on mobile devices of all sorts, and even natively in the Windows 8 operating system. Developers for these platforms routinely program directly in JavaScript, although, increasingly, they may generate JavaScript from other sources using a variety of compilers. Despite this widespread adoption, the programming languages community has a dubious view of JavaScript, because its unusual semantics can lead to hard-to-detect bugs.

In this talk, I will describe ongoing work at Microsoft Research that aims to make JavaScript safer to use. Enabling our work is F*, an ML-like language and program verification system being developed at MSR.

First, in order to statically check properties of JavaScript programs, we provide a translation from JavaScript to F*. Once in F*, we use its verifier to generate precise verification conditions and automatically discharge their proofs using an SMT solver. As a case study, we prove that a collection of JavaScript browser extensions are free of runtime errors. Aside from the annotation of loop and heap invariants, verification is automatic.

In the other direction, we take (a subset of) F* as a representative source language, and prove a compiler from it to JavaScript fully abstract. Full abstraction ensures that a compiled program can safely interact with an untrusted JavaScript context without fear of breaking any of its internal invariants. We use our compiler to program various secure libraries and also to bootstrap parts of the compiler itself within JavaScript.

Thus, our work addresses the needs of those who program directly in JavaScript and need to reason carefully about its semantics, as well as those who program in a higher-level language and wish to stay clear of JavaScript's wild side.

BIO:

Nikhil Swamy is a Researcher in the RiSE group at Microsoft Research, Redmond with a PhD (2008) in programming languages from the University of Maryland, College Park. Nikil's research covers various topics including type systems, program logics, functional programming, program verification, interactive theorem proving and the foundations of computer security. He is the lead designer and implementer of the F* programming language and the current chair of PL(X), the RiSE working group on programming languages.