Explode-js

Example

Considering the example program in the file exec.js:

let exec = require('child_process').exec;

module.exports = function f(source) {
  if (Array.isArray(source)) {
    return exec(source.join(' '));
  }
  return exec(source);
};

Notice that the function f receives a source parameter and, if it is an array, it joins its elements with a space and executes the command. Otherwise, it executes the command directly. Function f is vulnerable to two vulnerabilities of command injection depending on the input.

Explode.js will ask graph.js if it is able to identify the vulnerabilities in the function f. Graph.js, will output the following taint summary:

[
  {
    "filename" : "./test_vfunexported.js",
    "vuln_type" : "command-injection",
    "source" : "module.exports",
    "sink" : "exec",
    "sink_lineno" : 5,
    "type" : "VFunExported",
    "tainted_params" : [ "source" ],
    "params_types" : {
      "source" : "array"
    }
  },
  {
    "filename" : "./test_vfunexported.js",
    "vuln_type" : "command-injection",
    "source" : "module.exports",
    "sink" : "exec",
    "sink_lineno" : 7,
    "type" : "VFunExported",
    "tainted_params" : [ "source" ],
    "params_types" : {
      "source" : "string"
    }
  }
]

Importantly, notice that the summary contains two vulnerabilities with the same source, but with different sinks and parameters. The first vulnerability is related to the case where the source parameter is an array, and the second vulnerability is related to the case where the source parameter is a string.

To confirm the vulnerabilities, Explode.js will execute ecma-sl like this:

$ ecma-sl explode-js taint_summary.json
Genrating ecma-out/symbolic_test_0_0.js
Genrating ecma-out/symbolic_test_1_0.js
       exec : (`source0 : __$Str)
Found 1 problems!
  replaying : ecma-out/symbolic_test_0_0.js...
    running : ecma-out/symbolic_test_0_0/test-suite/witness-0.js
     status : true (created file "success")
       exec : (`source : __$Str)
Found 1 problems!
  replaying : ecma-out/symbolic_test_1_0.js...
    running : ecma-out/symbolic_test_1_0/test-suite/witness-1.js
     status : true (created file "success")

The output show that explode-js first created two symbolic tests, symbolic_test_0_0.js and symbolic_test_1_0.js, and then executed ecma-sl with each of them. The output shows that both tests found a problem, and subsequently during the replaying phase where the symbolic tests are executed with the concrete models generated in ecma-out/symbolic_test_0_0/test-suite/witness-0.js and ecma-out/symbolic_test_1_0/test-suite/witness-1.js, respectively, each being able to create a file named success. This confirms that the vulnerabilities are present in the function f.

Below we analyse the directory structure created by ecma-sl:

$ tree ecma-out
ecma-out
├── symbolic_test_0_0
│   ├── confirmation.json
│   ├── symbolic-execution.json
│   └── test-suite
│       ├── witness-0.js
│       └── witness-0.smtml
├── symbolic_test_0_0.js
├── symbolic_test_1_0
│   ├── confirmation.json
│   ├── symbolic-execution.json
│   └── test-suite
│       ├── witness-1.js
│       └── witness-1.smtml
└── symbolic_test_1_0.js

5 directories, 10 files

The directory ecma-out contains the symbolic tests and the directories symbolic_test_0_0 and symbolic_test_1_0 contain the result of the respective symbolic test.

The ecma-out/symbolic_test_0_0/symbolic-execution.json contains the symbolic execution summary of the first symbolic test:

$ cat ecma-out/symbolic_test_0_0/symbolic-execution.json
{
  "filename": "ecma-out/symbolic_test_0_0.js",
  "execution_time": 0.181838,
  "solver_time": 0.006068000000000018,
  "solver_queries": 1,
  "num_problems": 1,
  "problems": [ { "type": "Exec failure", "sink": "(`source0 : __$Str)" } ]
}

Observe that the symbolic execution summary shows that the symbolic test symbolic_test_0_0.js found a problem related to the sink "Exec" and that the symbolic expression (source0 : __$Str) was responsible for triggering the failure.

The ecma-out/symbolic_test_0_0/confirmation.json file contains the information related to the confirmation of the witnesses in ecma-out/symbolic_test_0_0/test-suite/ generated by the symbolic execution of the first symbolic test and which should trigger observadable effects:

$ cat ecma-out/symbolic_test_0_0/confirmation.json
{
  "filename": "ecma-out/symbolic_test_0_0.js",
  "effectful_payloads": [
    {
      "payload": "ecma-out/symbolic_test_0_0/test-suite/witness-0.js",
      "effect": "(created file \"success\")"
    }
  ]
}

The ecma-out/symbolic_test_0_0/confirmation.json file shows that the witness ecma-out/symbolic_test_0_0/test-suite/witness-0.js was able to create a file named success. Inspecting the content of the file:

$ cat ecma-out/symbolic_test_0_0/test-suite/witness-0.js
module.exports.symbolic_map =
  { "source0" : "`touch success`"
  }

The content of the file shows that the symbolic map contains the assignment source0: "touch success", which is the concrete model that triggered the vulnerability in the function f.

For reference, the ecma-out/symbolic_test_0_0.js looks like this:

$ cat ecma-out/symbolic_test_0_0.js
let exec = require('child_process').exec;

module.exports = function f(source) {
  if (Array.isArray(source)) {
    return exec(source.join(' '));
  }
  return exec(source);
};

let esl_symbolic = require("esl_symbolic");
esl_symbolic.sealProperties(Object.prototype);
// Vuln: command-injection
let source = [ esl_symbolic.string("source0") ];
module.exports(source);