We provide the source code of Chopper together with instructions for re-running the experiments presented in the paper.
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.
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.
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 |
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>
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
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>
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>
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>