Certified Verification of Client-Side Web Programs

Lead Research Organisation: Imperial College London
Department Name: Computing


The Web is evolving at enormous speed from a collection of mainly
static web pages to the current huge dynamic ecosystem where the
boundary between web pages and software application has become
indistinct (e.g. Google maps). This effect is so pronounced that
industry is beginning to view the Web as an operating system: e.g.,
Google's Chrome OS and Firefox OS. This quick transformation has come
at a price. We are stuck with dynamic languages developed for the
early Web. These languages are unsuited to the development of
sophisticated web applications, resulting in modern applications being
either overly conservative or needlessly unreliable and insecure.

JavaScript is the most widely used language for client-side web
programming: that is, in the web browser. Initially, JavaScript was
well-suited for the small web-programming tasks being asked of
it. With the modern Web however, the demands placed on JavaScript have
been huge. The dynamic nature of JavaScript makes understanding its
code notoriously difficult, leading to buggy, untrusted code. This
project will provide a certifying verification tool for JavaScript to
assert that e.g. a particular web application will maintain the
structure of a web page and not leak security information, or that a
browser extension will only perform permitted file system
operations. Our tool will automatically generate proofs which will be
certified (checked) by the well-known Coq proof assistant. Our
ambitious aim is to ensure that the software we use to communicate
with our banks is at least as reliable as the software as our banks
use to communicate with each other.

Planned Impact

A study by Boston Consulting Group 4 found that 8% of the UK GDP is
generated through the Internet. This share is expected to grow to 12%
by 2016, projecting the UK economy to become the world's most
internet-dependent economy. Meanwhile, the Cybersecurity position
statement of Research Council UK quotes the cost of cybercrime to the
UK in 2010 at £27 billion. This will inevitably rise as the UK becomes
more dependent on the Internet. The Web can only function as an
instrument of wealth creation if the programs that are used to access
it are robust, reliable and secure.

We will produce a variety of certifying verification tools, supported
by Coq and with a strong empirical link to industrial languages.
These verification tools will provide much needed support for the
engineers that build the Web.

Tasks 1-2. We provide systematic comparisons between browser
implementations and ECMA reference implementations. Library authors
will be interested in the comparisons between browser implementations,
because they will want their libraries to work on all
browsers. JavaScript implementers will be interested in the ECMA
reference implementations.

Task 3. We will provide the principled development of a core
certifying verification tool for JavaScript, rooted in the Coq
specifications given in Tasks 1-2. The main industrial impact will be
through Task 6.

Task 4. We will provide a library plugin interface for e.g. DOM, with
simple connections to the well-known academic and industrial
verification tools based on separation logic.

Task 5. Working with Miller from Google California, we will provide a
formal description of Secure ECMAScript (SES), proofs that
e.g. Google's makeContractHost enforces contracts between mutually
untrusting parties, and a proof that the SES implementation in
JavaScript is indeed secure.

Task 6. We will build specific, usable development tools for
JavaScript based on JSVerify and the DOM plugin, with the guidance of
Mozilla engineers. E.g., we will assist a web application developer to
produce bug-free apps and a security analyst to review Firefox addons.

This proposal is highly ambitious, ranging from a Coq specification of
a real-world language through to industrially-accepted certifying
development tools. However, our recent research and discussions with
key industrial engineers suggest that these aims are not beyond reach.


10 25 50
publication icon
Arceri V (2017) Abstract Domains for Type Juggling in Electronic Notes in Theoretical Computer Science

publication icon
Bella G. (2015) 2015 Special Track on Computer Security in Proceedings of the ACM Symposium on Applied Computing

publication icon
Charguéraud A (2018) JSExplain

publication icon
Fragoso Santos J (2016) Trustworthy Global Computing

publication icon
Fragoso Santos J (2017) JaVerT: JavaScript verification toolchain in Proceedings of the ACM on Programming Languages

publication icon
Fragoso Santos J (2019) JaVerT 2.0: compositional symbolic execution for JavaScript in Proceedings of the ACM on Programming Languages

publication icon
Gardner P (2018) JaVerT

Description JavaScript is used by 95% of websites (w3techs.com/technologies/details/cp-javascript/all/all), and is the most active language in repositories such as GitHub (http://githut.info). Gardner and Maffeis have developed a substantial mechanised JavaScript specification, at the time the largest language specification in the Coq theorem prover (900 rules).
The specification has become a standard Coq reference, highlighted in the position paper associated with the $10M NSF Exhibition in Science `DeepSpec'. The work led to the reporting of bugs in the standard in browser implementations and in the official test suite. More significantly, using JavaScript as the demonstrator, Gardner and Maffeis have introduced the first methodology for establishing trust in large mechanised language specifications: the formal rules correlate line-by-line with the ECMAScript standard; and the provably-correct reference implementation is systematically tested.

The dynamic, complex nature of JavaScript makes it a difficult target for logic-based verification. Gardner has developed JaVerT, a scalable semi-automatic JavaScript Verification Toolchain based on the JavaScript program logic of Gardner and Maffeis. This work introduced a methodology for establishing trust in such a verification tool,
providing a precise link between mathematical formalism and implementation and carefully crafted abstract specifications that resonate with the knowledge of the software developer. JaVerT leads the field in logic-based JavaScript verification.

Maffeis has completed the ChromeParty browser extension, which captures realistic web browsing data and analyses privacy-related properties. We have reported bugs in the Chromium API for extensions (Chromium is the open-source core of Google Chrome), discovered while working on the ChromeParty extension. We have designed a hybrid type
system for enforcing secure information flow in a subset of JavaScript, which we have implemented and used for securing the code of simple Web applications. Furthermore, we have developed an information flow monitor for a core of JavaScript that can be extended with arbitrary Web APIs, such as the DOM API or the XMLHttpRequest
API. Finally, we have designed and implemented a compiler for automatically sandboxing untrusted JavaScript third-party code and we showed how to use this compiler for automatically generating secure JavaScript Web applications.
Exploitation Route JSCert and JSRef could be adapted for the EcmaScript 6 standard, or, with certain adjustments and interest from the EcmaScript committee, be directly used in the creation process of the forthcoming JavaScript standards. JaVerT and its derivatives could be used by companies interested in symbolic analysis: for example, Amazon and Facebook.
Sectors Digital/Communication/Information Technologies (including Software)

URL http://jscert.org/
Description JSCert: Mozilla JSCert has been used, both directly and through its derivatives, to correct the JavaScript English standard, the official test suite and the JavaScript implementations of browsers. The accuracy of the standard and the official tests is essential to provide a unified JavaScript experience across the browsers. This is especially important for minority market-share browsers such as Mozilla's Firefox, where the lack of interoperable behaviour can cause competitive disadvantage: for example, web applications test exclusively against incumbent browsers like Google Chrome leading to less reliable user experiences on minority browsers. Mozilla actively engaged with the work of the JSCert team as a way to ensure a higher degree of interoperability and consequently a fairer browser market. JSCert: Google and Dfinity Gardner's JSCert methodology has been directly used in the mechanised specification [1] of the WebAssembly (Wasm) language of Google, Mozilla, Microsoft and Apple [2], identifying errors in both the specification and safety proof that required correction before publication. These errors would have undermined the emphasised formal basis of the Wasm standard, adopted as the first universal browser language since JavaScript and widely used in cloud computing, edge computing, and sandboxing. Dfinity have built their tamperproof cloud computing platform around Wasm, attracted by the high level of precision and rigour provided by the formal specification. [1] Mechanising and Verifying the WebAssembly Specification, Watt, CPP'18 [2] Bringing the Web up to Speed with WebAssembly, Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai and JF Bastien, PLDI'17 JSCert: Arm Ltd JSCert emphasised a line-by-line, modular approach for connecting a formal language specification with an informal English standard, called 'eyeball closeness', which directly influenced ARM in their published formalisation of an ARM architecture specification [5] and on-going extensions. This work is part of ARM's long-term strategy to create trustworthy formal specifications of their architecture, to verify formally their processors against these specifications, and to publicly release the specifications to enable formal verification of software as emphasised in the recent ISCF Digital Security by Design challenge. [5] Who Guards the Guards? Formal Validation of the Arm V8-M Architecture Specification, Alastair Reid, OOPSLA'17 JaVerT (POPL'18) and JaVerT 2.0 (POPL'19) Amazon Web Services (AWS). Using JaVerT 2.0 and later Gillian, Gardner's team has verified the deserialisation procedure of the AWS Message Header, part of the AWS Encryption SDK Message Format, formally verifying properties that were previously written by an Amazon code developer as English comments. The verification process revealed two bugs that could have led to minor security vulnerabilities, and these were subsequently fixed by the deveopers. Facebook. Facebook have established the viability of using continuously-integrated compositional analysis techniques inside the industrial design process, both at Facebook and in many other companies. The modular design of JaVerT 2.0 provides a fundamental understanding of bi-abduction, the pioneering compositional analysis technique used by the Facebook static analysis tool Infer, in terms of fixes arising from resource errors.
First Year Of Impact 2015
Sector Digital/Communication/Information Technologies (including Software)
Description Continuous Reasoning: JaVerT 2.0: Automatic Compositional Analysis for JavaScript
Amount $49,246 (USD)
Organisation Facebook 
Sector Private
Country United States
Start 11/2018 
Description Facebook Faculty Research Grant - Philippa Gardner
Amount $40,000 (USD)
Organisation Facebook 
Sector Private
Country United States
Start 09/2015 
Description GCHQ Small Grants scheme
Amount £95,151 (GBP)
Organisation Government Communications Headquarters (GCHQ) 
Sector Public
Country United Kingdom
Start 11/2016 
End 03/2017
Description GCHQ Small Grants scheme
Amount £5,400 (GBP)
Organisation Government Communications Headquarters (GCHQ) 
Sector Public
Country United Kingdom
Start 11/2016 
End 03/2017
Description GCHQ Small Grants scheme
Amount £13,385 (GBP)
Organisation Government Communications Headquarters (GCHQ) 
Sector Public
Country United Kingdom
Start 02/2015 
End 03/2015
Description VeTSpec: Verified Trustworthy Software Specification
Amount £1,579,794 (GBP)
Funding ID EP/R034567/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 08/2018 
End 08/2023
Description Collaboration with Julian Dolby (IBM) 
Organisation IBM
Country United States 
Sector Private 
PI Contribution Research expertise in analysis and verification of JavaScript programs
Collaborator Contribution Research expertise with Rosette, a general framework for the development of program analysis tools, on top of which we built the Cosette tool for symbolic testing of JavaScript programs.
Impact Cosette - a tool for trustworthy symbolic testing of JavaScripts programs, and the associated publication (Symbolic Execution for JavaScript (PPDP'18)). Cosette was applied to whole-program symbolic testing of real-world JavaScript libraries, finding several bugs fixed by the developers.
Start Year 2017
Title Browser security testing web application 
Description Web application to test that browser correctly implements security standards. 
Type Of Technology Webtool/Application 
Year Produced 2014 
Impact Discovered 2 bugs in Mozilla Firefox browser. Helped Mozilla Firefox security patch developer. Discovered and reported security bugs in Blackberry browser. Companion paper accepted to ISSTA 2015 conference. 
URL https://browseraudit.com
Title JaVerT 
Description JaVerT is a cutting-edge verification tool chain for JavaScript based on separation logic. JaVerT works by first translating JavaScript programs and specifications to a small intermediate goto language, called JSIL, and then performing verification on JSIL programs. JaVerT comprises: a compiler from JavaScript to JSIL; a semi-automatic verification tool, called JSILVerify, based on a JSIL program logic; and a logic translator from JavaScript assertions to JSIL assertions. 
Type Of Technology Software 
Year Produced 2018 
Open Source License? Yes  
Impact The JaVerT team is actively collaborating with Amazon and IBM. We are working with Julian Dolby, at IBM New York, on using the JaVerT infrastructure to build an automatic bug finding tool for JavaScript. The PhD student who started the project did an an internship at Amazon on designing a taint analysis for JavaScript using JSIL as a front-end for CBMC. We supervised four Master students (two MEng, once MSc, and one conversion MSc) in 2016. 
URL https://dl.acm.org/doi/abs/10.1145/3158138
Title JaVerT 2.0: Compositional Symbolic Execution for JavaScript 
Description JaVerT 2.0 introduces a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. It supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. JaVerT 2.0 has been evaluated on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
Impact JaVerT 2.0 has won a Facebook Research award ($50K) and was part of a project to verify parts of the Amazon AWS Message Format management system, which then migrated to Gillian. JaVerT 2.0 was the starting point for JaVerT.click, an extension which has the ability to reason about event-driven programs that use the DOM and JavaScript constructs for asynchronous programming. 
URL https://dl.acm.org/doi/abs/10.1145/3290379
Title JaVerT.click 
Description We introduce a trusted infrastructure for symbolic analysis of modern event-driven Web applications. This infrastructure consists of reference implementations of the DOM Core Level 1 and UI Events, JavaScript Promises, and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics that is sufficiently expressive to describe the event models underlying all these APIs. Our reference implementations are trustworthy in that they follow the API respective standards line-by-line and they are thoroughly tested against the appropriate official test-suites, passing all the applicable tests. Using the Core Events Semantics and the reference implementations, we develop JaVerT.Click, a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScript programs that use some (possibly all) these APIs. 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
Impact JaVerT.Click was used to perform comprehensive symbolic testing of the events module of Cash, a widely-used jQuery alternative, creating a symbolic test suite with 100% line coverage, establishing bounded correctness of several essential properties of the module, and discovering two subtle, previously unknown bugs. As part of a project protected under an NDA, it was also used to analyse parts of the Amazon Prime Video codebase. 
URL https://drops.dagstuhl.de/opus/volltexte/2020/13202/
Description Invited talk at the Ecma TC39 meeting, Google, NY 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact I was invted to give a talk about JavaScript Verification at the TC39 - ECMAScript Task group standards committee meeting held at Google, New York. The talk, entitled "Towards Trustworthy Verification of JavaScript" was delivered at the Visions for the future of ECMAScript / Emerging technologies session of the meeting. The TC39 Task Group oversees the standardization of the general purpose, cross platform, vendor-neutral ECMAScript (JavaScript) programming language. This includes the language syntax, semantics, and libraries and complementary technologies that support the language.
Year(s) Of Engagement Activity 2017