KLEE

Version 1.3.0

Using KLEE with Docker

using Docker Images

What is Docker?

Docker provides tools for deploying applications within containers. Containers are (mostly) isolated from each other and the underlying system. This allows you to make a KLEE container , tinker with it and then throw it away when you’re done without affecting the underlying sytem or other containers.

A Docker container is built from a Docker image. A Docker image encapsulates an application which in this case is KLEE. This application level encapsulation is useful because it provides a “portable” and reproducible environment to run KLEE in.

Installing Docker

To run Docker natively on your machine you need to be using a Linux distribution with Docker installed. Follow these links for installation instructions on Ubuntu, OS X and Windows.

Getting the KLEE Docker image

There are two ways of obtaining the KLEE Docker image.

Pulling from the Docker Hub

Our GitHub repository is linked to the DockerHub so that changes to particular branches trigger an automatic rebuild of the corresponding Docker image.

To pull down the latest build of a particular Docker image run:

$ docker pull klee/klee

If you want to use a tagged revision of KLEE you should instead run:

$ docker pull klee/klee:<TAG>

Where <TAG> is one of the tags listed on the DockerHub. Typically this is either latest (corresponds to the master branch) or a version number (e.g. 1.0.0).

Note this process pulls images containing code compiled by a third-party service. We do not accept resonsibility for the contents of the image.

Building the Docker image locally

If you want to build the Docker image manually instead of pulling the image from DockerHub you can do so by running:

$ git clone https://github.com/klee/klee.git
$ cd klee
$ docker build -t klee/klee .

This will use the contents of the Dockerfile in the root of the repository to build the Docker image.

Creating a KLEE Docker container

Now that you have a KLEE Docker image you can try creating a container from the image.

The simplest thing to try is creating a temporary container and gain shell access. To do this run

$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee

Note if you wanted to use a tagged KLEE image replace klee/klee with klee/klee:<TAG> where <TAG> is the tag you wish to use

Note the --ulimit option sets an unlimited stack size inside the container. This is to avoid stack overflow issues when running KLEE.

If this worked correctly your shell prompt will have changed and you will be the klee user.

klee@3c098b05ca85:~$ whoami
klee
klee@3c098b05ca85:~$

You can now try running KLEE inside the container

klee@3c098b05ca85:~$ klee --version
KLEE 1.0.0 (https://klee.github.io)
  Built Sep 21 2015 (17:03:14)
  Build mode: Release+Asserts
  Build revision: unknown

LLVM (http://llvm.org/):
  LLVM version 3.4
  
  Optimized build.
  Built Mar  5 2014 (17:05:10).
  Default target: x86_64-pc-linux-gnu
  Host CPU: core-avx2

and Clang

$ clang --version
Ubuntu clang version 3.4-1ubuntu3 (tags/RELEASE_34/final) (based on LLVM 3.4)
Target: x86_64-pc-linux-gnu
Thread model: posix

Now exit the container

klee@3c098b05ca85:~$ exit

Because the --rm flag was used with the docker run command the container was destroyed (not visible in docker ps -a) when the application running in the container (/bin/bash) terminated.

Persistent Containers

The earlier example didn’t do anything interesting with KLEE and threw the created container away. Here is a simple example that does something slightly more interesting with KLEE and also shows how a container can be persisted.

To create and enter the container run:

$ docker run -ti --name=my_first_klee_container --ulimit='stack=-1:-1' klee/klee

Notice we didn’t use --rm so the container will not be destroyed when we exit it from it and we also gave the container a name using the --name flag.

Now inside the container you can try running the following:

klee@3c098b05ca85:~$ pwd
/home/klee
klee@3c098b05ca85:~$ echo "int main(int argn, char** argv) { return 0; }" > test.c
klee@3c098b05ca85:~$ clang -emit-llvm -g -c test.c -o test.bc
klee@3c098b05ca85:~$ klee --libc=uclibc --posix-runtime test.bc
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/klee/klee_build/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/klee/klee-out-0"
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 44070352)
KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: done: total instructions = 5047
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
klee@3c098b05ca85:~$ ls
klee-last  klee-out-0  klee_build  klee_src  test.bc  test.c

Now exit the container

klee@3c098b05ca85:~$ exit

We can check that the container still exists by running

$ docker ps -a
CONTAINER ID        IMAGE               COMMAND             CREATED              STATUS                     PORTS               NAMES
1c408467bdf7        klee/klee           "/bin/bash"         About a minute ago   Exited (0) 2 seconds ago                       my_first_klee_container

You can restart the container by running

$ docker start -ai my_first_klee_container
klee@1c408467bdf7:~$ ls
klee-last  klee-out-0  klee_build  klee_src  test.bc  test.c
klee@1c408467bdf7:~$ exit

As you can see the files we created earlier are still present.

When you are finished with the container you can run

$ docker rm my_first_klee_container

to remove it.

Working with KLEE containers built from the KLEE Docker image

There are a few useful things to know about KLEE Docker containers created using the KLEE Docker image.

This should give you everything you need to start playing with KLEE using Docker. If you are unfamilar with Docker and wish to learn more a good place to start is Docker’s documentation.