Home

Awesome

ExpoSE

ExpoSE is a dynamic symbolic execution engine for JavaScript, developed at Royal Holloway, University of London by Blake Loring, Duncan Mitchell, and Johannes Kinder (now at LMU Munich). ExpoSE supports symbolic execution of Node.js programs and JavaScript in the browser. ExpoSE is based on Jalangi2 and the Z3 SMT solver.

Requirements

Requires node version v21.7.2 (other versions may work but are not tested), npm, clang (with clang++), gnuplot (for coverage graphs), make, python (Python 3).

mitmproxy (Depends libxml2-dev, libxslt-dev, libssl-dev) is required for electron analysis.

Installation

Execute ./install inside the ExpoSE directory for a clean installation.

Complete instructions (including installing Node.js and NPM using fnm)

curl -fsSL https://fnm.vercel.app/install | bash
eval $(fnm env)
fnm install 21.7.2
fnm use 21.7.2
./install
./expoSE ./tests/numbers/infoflow

ExpoSE CLI

Alternatively, you can invoke ExpoSE directly via the expoSE command line interface.

Example:

$ expoSE ./tests/numbers/infoflow

Valid Options:

ExpoSE Browser Support

There is limited support for symbolic execution of webpages through a custom Electron based web browser. To execute ExpoSE on a website you use the same arguments as the CLI. Note: This also requires python3 and a modern version of mitmproxy to function correctly.

$ expoSE "https://google.com"

Configuration

ExpoSE is configured via environment variables. All work both with the ExpoSE GUI and ExpoSE CLI. Typically these can be set from a terminal by writing a command such as

$ EXPOSE_LOG_LEVEL=1 expoSE target/hello.js

NOTE: To improve performance logging instructions are removed from the output at compile time and so will not be updated if NO_COMPILE is set.

Publications