We study the mechanised specification of the JavaScript language (following the ECMAScript 5 standard) and the verification of JavaScript programs.

JSCert

With Bodin, Charguéraud, and Schmitt at Inria, we have developed JSCert, a substantial Coq specification that is line-by-line close to the core language of the ECMAScript 5 standard. It comes with a reference interpreter, JSRef, proven correct with respect to JSCert and tested using the official Test262 test suite. We are currently extending this specification to the numerous libraries, providing continuous test integration for the ever-growing specification, developing a new, human-readable JSRef, with a tighter connection to the standard and good tracking properties, and creating the web service Explain.js to explain behavioural complexities of JavaScript programs.

JSIL

We have developed a principled compiler from JavaScript (ECMAScript 5 strict) to a small intermediate language JSIL, which has a simpler operational semantics and is better suited to program verification. The compiler has been substantially tested using the Test262 test suite and it comes with a hand-proof of translation correctness for a fragment of the language. We will use JSIL to develop JSVerify - a verification tool for JavaScript. Daiva Naudžiūnienė will this year hold internships at Amazon and Facebook to use JSIL to develop front-ends for the CBMC and Infer verification tools.

Research Support

This research is supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems and previously by the EPSRC/GCHQ grant EP/K032089/1: Certified Verification of Client-Side Web Programs and the EPSRC programme grant EP/H008373/2: Resource Reasoning.

We also interact extensively with Arthur Charguéraud, Alan Schmitt and Martin Bodin of INRIA, who are supported by the AJACS project.

People

Recent Publications

  1. A perspective on specifying and verifying concurrent modules

    Journal of Logical and Algebraic Methods in Programming, vol. 98, pp. 1–25

  2. JSExplain: a Double Debugger for JavaScript

    WWW ’18 Companion: The 2018 Web Conference Companion, April 23–27, 2018, Lyon, France

  3. JaVerT: JavaScript verification toolchain

    PACMPL, vol. 2(POPL), pp. 50:1–50:33

  4. An Infrastructure for Tractable Verification of JavaScript Programs

    Ph.D. Thesis, Imperial College London

  5. Towards Logic-based Verification of JavaScript Programs

    Proceedings of 26th Conference on Automated Deduction (CADE 26)

  6. DOM: Specification and Client Reasoning

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 401–422

  7. Mashic Compiler: Mashup Sandboxing based on Inter-frame Communication

    Journal of Computer Security, vol. 1(24), pp. 91–136

  8. A Trusted Mechanised Specification of JavaScript: One Year On

    Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), pp. 3–10

  9. Modular Monitor Extensions for Information Flow Security in JavaScript

    Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, pp. 47–62

  10. Hybrid Typing of Secure Information Flow in a JavaScript-Like Language

    Trustworthy Global Computing - 10th International Symposium, TGC 2015, Madrid, Spain, August 31 - September 1, 2015 Revised Selected Papers, pp. 63–78