Abstract
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.
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 language | English |
---|---|
Qualification | Ph.D. |
Awarding Institution |
|
Supervisors/Advisors |
|
Award date | 1 Apr 2021 |
Publication status | Unpublished - 16 Mar 2021 |