Abstract

The behaviour of JavaScript programs executed in the browser is complex. This talk will describe two related projects: JSCert which provides a mechanised specification of the JavaScript English standard (ECMAScript 5); and JSVerify which provides a verification tool for reasoning about Javascript programs. Both projects establish theory and tools for obtaining a better understanding of JavaScript programs. The talk is aimed at a general audience interested in language specification and program verification. Knowledge of JavaScript is not assummed.

JSCert provides a Coq mechanised specification of the core JavaScript language. A key aim is to develop a methodology for establishing trust. The JSCert specification is line-by-line close to the JavaScript English standard. It comes with a reference interpreter, JSRef, which is proven correct with respect to JSCert and tested using the official Test262 test suite. In this talk, I will describe and evaluate the current state of the JSCert project.

JSVerify provides a verification tool for reasoning about JavaScript programs (in ECMA Script 5 strict mode), based on a principled compiler from JavaScript to an intermediate language called JSIL . JSIL has essentially the same memory model as JavaScript but a simpler specification which reduces the workload required to build and adapt analysis tools. The compiler has been substantially tested using the Test262 test suite and a fragment has been proved correct. In this talk, I will describe JSVerify and current plans to build JavaScript front-ends for the analysis tools CBMC (Amazon), Infer (Facebook) and Viper (ETH).

An ultimate challenge is to verify the verifier, checking that the proofs developed by JSVerify are indeed correct using JSCert.