Skip to content

ECMAScript Specification Language, a new framework for creating dynamic analyses for JavaScript.

License

Notifications You must be signed in to change notification settings

formalsec/ECMA-SL

Repository files navigation

Build

ECMA-SL Project

AboutInstallationExecutionIDEIssuesLicense


About

ECMA-SL is a comprehensive platform designed for the specification and execution of the ECMAScript standard, commonly known as JavaScript. The platform introduces an intermediate language, ECMA-SL, which serves as a bridge between JavaScript and its execution environment. This intermediate language is used to develop reference implementations of the ECMAScript standard that adhere to JavaScript's specification.

Key features of the platform include a JavaScript-to-ECMA-SL (JS2ECMA-SL) parser, allowing the conversion of JavaScript code into the ECMA-SL language. Additionally, ECMA-SL incorporates a compiler from ECMA-SL to Core ECMA-SL, a simplified version of the intermediate language, as well as an interpreter for Core ECMA-SL. The combination of these tools results in a mechanism to execute JavaScript programs using the reference interpreters for the language.



Installation

The ECMA-SL platform is accessed through the ecma-sl application, which is written in the OCaml programming language. To build this application, we employ dune, a composable build system for OCaml.

  1. Install opam
  2. Bootstrap the OCaml compiler:
opam init
opam switch create ecma-sl 4.14.0
eval $(opam env)
  1. Install the library dependencies:
opam update
opam install . --deps-only --with-test
  1. Build the application and run the available test suit:
dune build
dune runtest
  1. (Optional) Generate code coverage summary/report:
BISECT_FILE=`pwd`/bisect dune runtest --force --instrument-with bisect_ppx
bisect-ppx-report summary # Shell summary
bisect-ppx-report html    # Detailed Report in _coverage/index.html
  1. Install the application on your path:
dune install

Integrating OCaml with VSCode

  1. Install the OCaml Platform extension:
  2. Install the OCaml language server and code formatter.
opam install ocaml-lsp-server ocamlformat


ECMA-SL Reference Execution

The ecma-sl application provides the following commands, among others:

  • compile: to compile an ECMA-SL (.esl) program into Core ECMA-SL (.cesl).
  • interpret: to interpret a Core ECMA-SL (.cesl) program.
  • encode: to encode a JavaScript (.js) program in Core ECMA-SL (.cesl)
  • ...

Use ecma-sl --help for more information about the entire application, or ecma-sl <command> --help for in-depth information regarding a specific command, including a comprehensive list of available options.


Compile and Interpret an ECMA-SL Program

  • Compile an ECMA-SL (.esl) program into Core ECMA-SL (.cesl), and interpret the Core ECMA-SL program:
$ ecma-sl compile test/ecma-sl/test_stdlib_inequality.esl -o distinct.cesl
$ ecma-sl interpret distinct.cesl
  • Interpret an ECMA-SL (.esl) program directly (the application extrapolates the language of the program based on the file extension, and compiles the ECMA-SL program to ECMA-SL if needed):
$ ecma-sl interpret test/ecma-sl/test_stdlib_inequality.esl

Verbose / Debug Interpretation

  • Interpret an ECMA-SL (.esl) program in verbose mode (all intermediate interpreter steps are logged):
$ ecma-sl interpret test/ecma-sl/test_stdlib_inequality.esl --debug full
[ecma-sl] Sucessfuly compiled program 'test/ecma-sl/test_stdlib_inequality.esl'.
[ecma-sl] Sucessfuly evaluated program with return '0'.
  • Execute an ECMA-SL (.esl) program with the debug prompt (breakpoints can be added to (.esl) code by preceding the instruction with #):
$ ecma-sl interpret test/ecma-sl/test_stdlib_inequality.esl --db

Encode and execute a JavaScript Program

  • Encode a JavaScript (.js) program in Core ECMA-SL (.cesl), and execute the encoded program using the default reference interpreter.
$ ecma-sl encode test/javascript/simple/catch.js -o catch.cesl
$ ecma-sl execute catch.cesl
Function 'foo' called
Exception caught: 20
Ret: 30
  • Execute a JavaScript (.js) program directly (the application extrapolates the language of the program based on the file extension, and encodes the JavaScript program in Core ECMA-SL if needed):
$ ecma-sl execute test/javascript/simple/catch.js
Function 'foo' called
Exception caught: 20
Ret: 30
  • Test a JavaScript (.js) program using a test harness:
$ ecma-sl test --harness=test/javascript/harness.js test/javascript/simple/string.js
---------------------------------------------------------------
 ECMA-SL Test Summary:

test/javascript/simple/string.js ............ SUCCESS ...

---------------------------------------------------------------

Test Summary:


Tests Successful: 1 / 1 (100.00%) | Time elapsed: ...
Failures: 0, Anomalies: 0, Skipped: 0


ECMA-SL Symbolic Execution

The ecma-sl binary provides a symbolic execution mode via the symbolic command. Symbolic execution requires at least one SMT solver to be installed.

To start using the symbolic command, ensure that Z3 is installed by running:

opam install z3

Afterward, rebuild the ecma-sl binary by following the instructions in installation.

For more information on other available solvers, see Supported Solvers.

Integrated Development Environment (IDE)

Syntax Highlighting for ECMA-SL

  • VSCode - To start using the VSCode syntax highlighter for ECMA-SL, copy the [extension] it into the $HOME/.vscode/extensions folder and restart VSCode.
  • Vim - To start using the Vim syntax highlighter for ECMA-SL, refer to the ecmasl-vim project


Issues

For the list containing all current issues, please consult our issue-tracker.



License

This project is licensed under the GPL-3.0 License - see the LICENSE file for details.

About

ECMAScript Specification Language, a new framework for creating dynamic analyses for JavaScript.

Topics

Resources

License

Code of conduct

Stars

Watchers

Forks

Packages

No packages published