HTTPS SSH
DRAFT of CATAPULT (revised November 2016):
=========================================================

Check out the CATAPULT draft here (in the repository): 

=> draft/catapult.pdf

The previous submission had a minor inconsistency between 
the text of the paper and the pseudocode (Algorithm 1). 
The textual description and all the evaluation were correct, 
but the pseudocode skipped one line of our approach. The 
current version in the repository has now fixed the 
inconsistencies between the text of the draft and the test 
generation pseudocode (Algorithm 1). 


README file for catapult:
==========================

CATAPULT is a tool based on symbolic execution toolkit KLEE. CATAPULT 
systematically explores cache behaviour of an arbitrary programs and 
it generates test inputs that witness each such cache behaviour. 

Download and Installation: 
===========================

Clone the catapult repository: hg clone https://sudiptac@bitbucket.org/sudiptac/catapult

Since CATAPULT is built on top of KLEE, the installation of CATAPULT 
requires to follow the step to install KLEE in the following:

http://klee.github.io/build-llvm29/

From the aforementioned URL, you only need to change step (5) by downloading 
the modified version of KLEE as follows: 

hg clone https://sudiptac@bitbucket.org/sudiptac/catapult 

From steps (6)-(8), please refer to  http://klee.github.io/build-llvm29/ in order to 
compile and run KLEE. 

Running CATAPULT: 
==========================

Run the tool as follows: 

## klee --write-smt2s --cache-cfg=<cache_configuration_file> <bitcode_file_of_test_subject>

We have introduced the option "--cache-cfg" within KLEE to communicate the cache 
configuration. This option takes the cache configuration within a file and the 
file has the following format: 

-> <number of sets>:<line size>:<associativity>:<unused_field>:<replacement policy> 

<line size> is in number of bytes and <unused_field> is an integer with any value. 
This field is currently ignored and it is reserved for future use. 
<replacement_policy> is "l" (for LRU) or "f" (for FIFO). 

For instance, 32:32:2:90:l captures a two-way set-associative, 2 KB cache with 32 
bytes line size and LRU replacement policy. 

Our tool currently does not handle replacement policies other than LRU or FIFO. 


Running a test program: 
==========================

Check installation: 

Go to benchmarks/test directory and run: 

# klee --write-smt2s --cache-cfg=cache_lru.cfg test_symbolic.bc

This should generate all tests for a toy program "test_symbolic.bc". 


Reporoducing the experimental results: 
======================================

We use the following subjects to evaluate CATAPULT:

- benchmarks/aes_basic_crypto
- benchmarks/openssl/crypto/aes
- benchmarks/openssl/crypto/des
- benchmarks/openssl/crypto/rc4
- benchmarks/openssl/crypto/rc5
- benchmarks/gdklib (two different routines "gdkkeyuni" and "gdkkeyname")

In each of the aforementioned directory, there are two scripts: 

- run_LRU
- run_FIFO

As the names suggest, "run_LRU" produces all results for LRU caches ranging 
from "2-way, 8KB" to "4-way, 64 KB". The script "run_FIFO" does the same for 
FIFO replacement policies. 

The results of run_LRU and run_FIFO scripts are stored in the following 
subdirectories within each subject directory, respectively: 

- log_test_generation, and 
- log_test_generation_FIFO

Note: Some of these experiments may run for *very* long. Therefore, feel free 
to modify the scripts. 


Contact: 
=========
If you face any problem in installation or running the tool, please contact 
Sudipta Chattopadhyay (sudiptaonline@gmail.com)