University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > Understanding and Verifying Javascript Programs.

Understanding and Verifying Javascript Programs.

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact David Greaves.

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.

This talk is part of the Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity