Chopper

We provide the source code of Chopper together with instructions for re-running the experiments presented in the paper.

Download

The source code of Chopper along with build instruction are available at https://github.com/davidtr1037/chopper

Chopper is implemented on top of the KLEE symbolic execution engine. It inherits the command-line options of KLEE, and is invoked as follows:

$ klee [klee-options] [program] [program-options]

The options which were added to KLEE are:

--skip-functions=<function1>[:line1/line2/…],<function2>[:line3/line4/…],...

--split-search=<BOOL>

--split-ratio=<INT>

--inline=<function1>,<function2>,...

--use-slicer=<BOOL>

In our experimental evaluation, we run Chopper with the following configuration:

--split-search

--split-ratio=20 (default)

Note that the value of the --skip-functions option is benchmark specific.


Experiments

The experiments were run on machines with 16 GB Memory and 8 CPUs (Intel i7-7600 @ 3.4 GHz), with Ubuntu 16.04 (64 bit).

To re-run the experiments, clone the following repository:

git clone https://github.com/andreamattavelli/chopper-experiments

Before running the experiments, configure the paths to your tools in the common.mk file.


Bug Fixes

We found a bug in our comparison between field-sensitive and field-insensitive objects, which lead to unsound side effects inference in some cases. The bug is fixed in the following commit:

This bug fix affects the results of Table 2. With the bug fix and the latest version of Chopper:

the expected results are:

CVE                       Heuristic               Time
2012-1569 Random 00:01:01
2012-1569 DFS 00:00:39
2012-1569 Coverage 00:00:56
2014-3467-1 Random 00:05:40
2014-3467-1 DFS 00:00:04
2014-3467-1 Coverage 00:02:59
2014-3467-2 Random 00:06:01
2014-3467-2 DFS 00:15:06
2014-3467-2 Coverage 00:08:31
2014-3467-3 Random 00:09:59
2014-3467-3 DFS 00:00:07
2014-3467-3 Coverage 00:04:40
2015-2806 Random 00:02:51
2015-2806 DFS Timeout
2015-2806 Coverage 00:01:12
2015-3622 Random 00:00:18
2015-3622 DFS 00:22:20
2015-3622 Coverage 00:00:18

Failure Reproduction

The experiment follows the protocol from Section 5.1 of the paper.

We run each of the tools (KLEE/Chopper) with several search heuristics (random, DFS, coverage-based) with a time limit of 24 hours.

First, go to the relevant CVE directory:

$ cd libtasn1/<CVE_ID>

Run the experiments with KLEE:

$ make all-klee

Run the experiments with Chopper:

$ make KSLICE=--split-search all-cse

Each of the runs creates its output directory under the name tool-run-search with the output of the corresponding run being redirected to run-tool-search.log.

One can also run the experiment with a specific search heuristic.

For example, the following command runs Chopper with a DFS search heuristic:

$ make run-cse-dfs

Use the klee-stats command in order to check the execution time:

$ klee-stats <output_directory>

Test Suite Augmentation

The experiment follows the protocol from Section 5.2 of the paper.

Before running the experiments, update the PATH environment variable:

$ export PATH=<klee_build_dir>/bin:$PATH

GNU BC

Switch to the following directory:

$ cd bc

Build the bitcode file (you will need WLLVM):

$ make bc.bc

Run baseline KLEE:

$ ./run-klee.sh

Then run Chopper:

$ ./run-chopper.sh

Note: In order to run Chopper without slicing, run:

$ ./run-chopper-no-slice.sh

Build the executable:

$ make clean
$ make bc

Replay the test cases of KLEE and generate the coverage report:

$ ./compute_coverage.sh <klee_out_dir>
$ ./gen_report.sh <klee_report_dir>

Replay the test cases of Chopper and generate the augmented coverage report:

$ ./compute_coverage.sh <chopper_out_dir>
$ ./gen_report.sh <chopper_report_dir>

LibYAML

Switch to the following directory:

$ cd libyaml

Build the bitcode file of the test driver:

$ make test-driver.bc

Run baseline KLEE:

$ ./run-klee.sh

Then run Chopper:

$ ./run-chopper.sh

Note: In order to run Chopper without slicing, run:

$ ./run-chopper-no-slice.sh

Build the executable of the test driver:

$ make clean
$ make test-driver-gcov

Replay the test cases of KLEE and generate the coverage report:

$ ./compute_coverage.sh <klee_out_dir>
$ ./gen_report.sh <klee_report_dir>

Replay the test cases of Chopper and generate the augmented coverage report:

$ ./compute_coverage.sh <chopper_out_dir>
$ ./gen_report.sh <chopper_report_dir>

oSIP

Switch to the following directory:

$ cd libosip

Build the bitcode file of the test driver:

$ make test-driver.bc

Run baseline KLEE:

$ ./run-klee.sh

Run Chopper:

$ ./run-chopper.sh

Note: In order to run Chopper without slicing, run:

$ ./run-chopper-no-slice.sh

Build the executable of the test driver:

$ make clean
$ make test-driver-gcov

Replay the test cases of KLEE and generate the coverage report:

$ ./compute_coverage.sh <klee_out_dir>
$ ./gen_report.sh <klee_report_dir>

Replay the test cases of Chopper and generate the augmented coverage report:

$ ./compute_coverage.sh <chopper_out_dir>
$ ./gen_report.sh <chopper_report_dir>