Venue

Ph.D. Thesis, Imperial College London

Publication Year

2022

Authors

Abstract

JavaScript has been widely adopted for the development of Web applications, being used for both client and server-side code. Client-side JavaScript programs commonly interact with Web APIs, for instance, to capture the user interaction with the Web page via events. The use of such APIs increases the complexity of JavaScript programs. In fact, most errors in these programs are caused by the misuse of Web APIs. There are several approaches for detecting errors in client-side JavaScript programs, but they either assume the use of a single API or do not model APIs faithfully, giving rise to inconsistent behaviour and lack of trust. We address the problem by developing a trustworthy infrastructure for the static analysis of Web APIs. We focus on two aspects of JavaScript programs: event-driven and message-passing programming, as these paradigms are common sources of confusion among developers. We choose to target the DOM event model and the JavaScript Promises and JavaScript async/await, which facilitate event-driven programming. Additionally, we target the message-passing model of the WebMessaging and WebWorkers APIs. We design formal semantics for events and message-passing to capture fundamental operations required by those APIs, and API reference implementations which are trustworthy in that they follow the respective standards and have been thoroughly tested against their official test suites. Using our formal semantics and reference implementations, we develop JaVerT.Click, the first static symbolic execution tool for JavaScript supporting both event-based and message-passing APIs. We evaluated both the reference implementations and the symbolic execution engine of JaVerT.Click. By testing the reference implementations against their official test suites, we found coverage gaps and issues in the test suites, most of which have been since fixed. By testing the symbolic execution engine against three open-source libraries, we established the bounded correctness of functional properties and found real bugs.

Source Materials