Assignment 4: Exploring KLEE

The purpose of this assignment is to learn about and explore KLEE Links to an external site., which is a popular symbolic execution engine built on top of LLVM. The assignment is pretty open-ended and allows for independent exploration. It consists of two parts, described next.

Part 1: Understanding KLEE

Read the seminal KLEE paper: http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf Links to an external site.

Write a summary of the paper, outlining in your own words how the KLEE algorithms works and other interesting aspects of the tool. Based on your understanding of the tool, suggest several (at least 3) different language features that you think KLEE can handle (e.g., if conditions involving integer variables), meaning that it can explore all paths in programs containing such features. Also, suggest several (at least 3) different language features, constructs, or examples that you think KLEE would not be able to handle, meaning that it would not be able to explore all paths in programs containing such features.

The summary should be at least one page.

Part 2: KLEE Case Study

Develop a small benchmark suite of programs based on the features you identified in Part 1. Each program should test one of the identified features. Run KLEE on each program and study the outcome. Was KLEE able to cover all the paths in the program? What are the paths it missed? Write a case study report (at least one page) describing the results and your conclusions. Compare your results against what you predicted in Part 1.

To get you started with KLEE, I installed it into an aptlab VM, which you should be able to instantiate here: https://www.aptlab.net/p/cs6110-s18/klee_vm Links to an external site.

I created several simple exercises to get your started, and I suggest you first go through them - just follow the profile instructions. You are more than welcome to leverage aptlab and this profile to perform your case study. Warning: the experiment you create in aptlab does expire (in 16 hours I think), and in that case you will use all the data in that experiment. So be careful about that. There is an option to extend it as well. Note that copy-pasting in and out of aptlab VM can be painful.

Alternatively, you can install KLEE on your own machine.

Deliverables

The deliverables for this assignment are a pdf document (single document for parts 1 and 2) and source code of your benchmark suite.