Monadic Reï¬nement Types for Verifying JavaScript Programs - Swamy, Nikhil; Weinberger, Joel; Chen, Juan; Livshits, Ben; Schlesinger, Cole (2012)
Researchers have developed several special-purpose type systems and program logics to analyze JavaScript and other dynamically typed programming languages. Still, no prior system can precisely reason about both higher-order programs and mutable state; each system comes with its own delicate soundness proof (when such proofs are provided at all); and tools based on these theories (when they exist) are a signiﬁcant implementation burden. This paper shows that JavaScript programs can be veriﬁed using a general-purpose veriﬁcation tool—in our case, F*, a dependently typed dialect of ML. Our methodology consists of a few steps. First, we extend prior work on lJS (Guha et al. 2010) by translating JavaScript programs to F*. Within F*, we type pure JavaScript terms using a reﬁnement of the type dyn, an algebraic datatype for dynamically typed values, where the reﬁnement recovers more precise type information. Stateful expressions are typed using the Hoare state monad. Relying on a general-purpose weakest pre-condition calculus for this monad, we obtain higherorder veriﬁcation conditions for JavaScript programs that can be discharged (via a novel encoding) by an off-the-shelf automated theorem prover. Our approach enjoys a fully mechanized proof of soundness, by virtue of the soundness of F*. We report on experiments that apply our tool chain to verify a collection of web browser extensions for the absence of JavaScript runtime errors. We conclude that, despite ommonly held misgivings about JavaScript, automated veriﬁcation for a sizable subset of the language is feasible. Our work opens the door to applying a wealth of research in automated program veriﬁcation techniques to JavaScript programs.