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


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:

$ 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>