Skip to content

A Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.

License

ExpoSEJS/ExpoSE

master
Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
November 15, 2020 21:48
November 15, 2020 21:48
April 13, 2020 07:21
lib
June 29, 2019 12:37
August 4, 2020 10:49
May 8, 2019 17:48
September 15, 2018 13:55
November 21, 2018 08:59
July 2, 2019 09:47
August 5, 2020 08:47
August 5, 2020 08:50
July 26, 2019 11:37

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 Bundeswehr University 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 v14.16.1 (other versions may work but are not tested), npm, clang (with clang++), gnuplot (for coverage graphs), make, python2 (as python in path). On Ubuntu, since python2 has been removed by default I found that you may need to install python3-distutils.

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

Installation

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

ExpoSE GUI

In most cases you want to start by running the ExpoSE dashboard. The GUI provides detailed test case information, easy replay, and coverage graphs. Start the ExpoSE dashboard with

$ npm start

ExpoSE CLI

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

Example:

$ expoSE ./tests/numbers/infoflow

Valid Options:

  • replay - Replay a test case with a specific input.
  • ahg - Automatically generate a generic test harness for a specified NPM library.

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
  • EXPOSE_MAX_TIME - The time (in milliseconds) to limit the total execution
  • EXPOSE_TEST_TIMEOUT - The time (in milliseconds) a test case can run for before being timed out
  • EXPOSE_PRINT_COVERAGE - Print out the files checked by an analysis and show the lines which where explored by the analyzer
  • EXPOSE_PRINT_PATHS - Print the output of each test case to stdout
  • EXPOSE_LOG_LEVEL - Level from 0 (None) to 3 (High)
  • EXPOSE_MAX_CONCURRENT - The maximum number of test cases that can run concurrently
  • RECOMPILE - Force ExpoSE to rebuild before executing scripts

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

About

A Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published