Practical Dynamic Symbolic Execution for JavaScript

Research output: ThesisDoctoral Thesis

628 Downloads (Pure)


In this thesis we develop a practical and scalable approach for dynamic
symbolic execution (DSE) of JavaScript programs and prove its effectiveness by
implementing ExpoSE, our new DSE engine. ExpoSE uses program instrumentation to
implement DSE, enabling analysis of both web applications and Node.js software
while also allowing quick support for the latest JavaScript standards.
We detail novel encodings for regular expressions, objects, and arrays
which allow ExpoSE to analyze programs out of reach of prior work.
In particular, we present the first complete encoding for ES6 regular
expressions, including symbolic support for capture groups and backreferences.
We show the effectiveness of our design through two case studies. In
the first study we show that our approach is able to generate a suite of
supplementary conformance tests for JavaScript standard library methods
that further the official JavaScript testing suite Test262. Test cases
are generated through symbolic exploration of polyfill implementations and
verified with differential testing. In the second case study we use DSE to automatically deduce what conditions trigger resource loading, enabling
our new speculative loading approach Oblique, a proxy which reduces page
load times by sending resources before a client requests them.
Original languageEnglish
Awarding Institution
  • Royal Holloway, University of London
  • Kinder, Johannes, Supervisor
Award date1 Apr 2021
Publication statusUnpublished - 16 Mar 2021

Cite this