vincenzoarceri/safe

Scalable Analysis Framework for ECMAScript

Scalable Analysis Framework for ECMAScript (SAFE) Version 2.0

Introduction

Copyright (c) 2016, KAIST

SAFE 2.0 is a scalable and pluggable analysis framework for JavaScript web applications developed by the Programming Language Research Group at KAIST:

http://plrg.kaist.ac.kr

Older versions are still available at the SAFE1.0 branch.

For more information, please check out our user manual.

Requirements

We assume you are using an operating system with a Unix-style shell (for example, Mac OS X, Linux, or Cygwin on Windows). Assuming SAFE_HOME points to the SAFE directory, you will need to have access to the following:

• J2SDK 1.8. See http://java.sun.com/javase/downloads/index.jsp
• Scala 2.12. See http://scala-lang.org/download
• sbt version 0.13 or later. See http://www.scala-sbt.org
• Bash version 2.5 or later, installed at /bin/bash. See http://www.gnu.org/software/bash/

In your shell startup script, add $SAFE_HOME/bin to your path. The shell scripts in this directory are Bash scripts. To run them, you must have Bash accessible in /bin/bash.

Installation

Type sbt compile and then sbt test in the SAFE directory to make sure that your installation successfully finishes the tests.

Once you have built the framework, you can call it from any directory, on any JavaScript file, simply by typing one of available commands at a command line. You can see the available commands by typing:

safe

or with more explanation:

safe help

Some of the available commands are as follows:

• parse: parses a JavaScript file.
• astRewrite: rewrites a JavaScript AST via Hoister, Disambiguator, and WithRewriter.
• compile: translates a JavaScript file to a SAFE intermediate representation.
• cfgBuild: builds a control flow graph for a JavaScript file.
• analyze: analyzes static properties of JavaScript expressions in a given file.

Changes from SAFE 1.0

• SAFE 2.0 has been tested using Test262, the official ECMAScript (ECMA-262) conformance suite.
• SAFE 2.0 now uses sbt instead of ant to build SAFE.
• SAFE 2.0 now provides an HTML-based debugger for its analyzer.
• Most Java source files are replaced by Scala code and the only Java source code remained is the generated parser code.
• Several components from SAFE 1.0 may not be integrated into SAFE 2.0. Such components include interpreter, concolic testing, clone detector, clone refactoring, TypeScript support, Web API misuse detector, and several abstract domains like the string automata domain.

SAFE 2.0 Roadmap

• SAFE 2.0 will make monthly updates.
• The next update will include a SAFE document, browser benchmarks, and more Test262 tests.
• We plan to support some missing features from SAFE 1.0 incrementally such as a bug detector, DOM modeling, and jQuery analysis.
• SAFE 2.0 is aimed to be a playground for advanced research in JavaScript web applications. Thus, we intentionally designed it to be light-weight.
• Future versions of SAFE 2.0 will address various analysis techniques, dynamic features of web applications, event handling, modeling framework, compositional analysis, and selective sensitivity among others.

Publications

Details of the SAFE framework are available in our papers:

• Battles with False Positives in Static Analysis of JavaScript Web Applications in the Wild (ICSE SEIP 2016)
• Static Analysis of JavaScript Web Applications in the Wild via Practical DOM Modeling (ASE 2015)
• Practically Tunable Static Analysis Framework for Large-Scale JavaScript Applications (ASE 2015)
• Development Nature Matters: An Empirical Study of Code Clones in JavaScript Applications (EMSE 2015)
• Scalable and Precise Static Analysis of JavaScript Applications via Loop-Sensitivity (ECOOP 2015)
• SAFE_WAPI: Web API Misuse Detector for Web Applications (FSE 2014)
• All about the ''with'' Statement in JavaScript: Removing ''with'' Statements in JavaScript Applications (DLS 2013)
• Formal Specification of a JavaScript Module System (OOPSLA 2012)
• SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript (FOOL 2012)

Users

SAFE has been used by:

• JSAI @ UCSB
• ROSAEC @ Seoul National University
• K Framework @ University of Illinois at Urbana-Champaign
• Ken Cheung @ HKUST
• Web-based Vulnerability Detection @ Oracle Labs
• Tizen @ Linux Foundation

Authors

The current developers of SAFE 2.0 are as follows:

• Jihyeok Park
• Youngseo Choi
• Jaemin Hong
• Joonyoung Park
• Sukyoung Ryu

and the following people have contributed to the source code:

• Yeonhee Ryou (SAFE 2.0 core)
• Minsoo Kim (Built-in function modeling)
• PLRG @ KAIST and colleagues in S-Core and Samsung Electronics (SAFE 1.0)