Experiments in concolic testing with Klee

Parsing JSON strings (aeson-cbits)

A function originally from json-strings, a Haskell library for JSON. Some concerns have been raised about the current lack of safety guarantees (for instance, see this issue in aeson).

Testing noninterference, quickly (noninterf)

A port of an experiment in random testing for noninterference properties of a small family of abstract machines. (In ICFP 2013, also on arxiv).

---

Build information

Initial setup

Scripts will assume that the root of this directory contains a klee/ folder with:

• klee/bin/: klee executables
• klee/lib/: klee libraries
• klee/include/: klee headers

A typical sequence of commands to get to a working setup:

mkdir klee/
ln -s /path/to/klee/include klee/include
ln -s /path/to/klee/build/bin klee/bin
ln -s /path/to/klee/build/lib klee/lib

We work with clang-5.0. The programs are probably simple enough to run on older versions though.

Running the examples

In each directory,

• make klee to launch Klee:

  • TIMEOUT=N to set a time limit of N seconds (default: 60);
  • NOLIMIT to disable timeouts.
  • OUTPUT_ALL_STATES to output all test cases generated by Klee (by default, we ask Klee to avoid recording test cases that do not discover new parts of the program).

• make replay builds an executable ($NAME.replay) to replay test cases.

  To run $NAME.replay, add libKleeRuntest to the LD_LIBRARY_PATH, and set KTEST_FILE to a test$N.ktest file.

  LD_LIBRARY_PATH=../klee/lib KTEST_FILE=klee-last/test000001.ktest ./noninterf.replay
  

  A shorter way to do that is with make replay TEST_FILE=klee-last/test000001.ktest.

• make coverage KLEE_OUT=klee-out-$N collects coverage information in $SRC.c.gcov (where klee-out-$N corresponds to a directory created by make klee)

These examples have various buggy versions. See Makefile in each directory for corresponding options.

For example, in aeson-cbits, this enables the BUG_DEST_TOO_SMALL.

make DEST_TOO_SMALL=true klee

Misc commands

• make just builds the program for Klee (implied by make klee).
• make cpp just preprocesses the files (for sanity checks).

Reminders

To use STP, Klee docs remind you to apply this. (In some environments, STP may segfault without it.)

ulimit -s unlimited