Instructions for Virtual Machine Image

Use Virtualbox to import the downloaded .ova file. After booting the virtual machine, you can log into the machine with

Username: ucsd Password: quark

Running the Browser

You can run the verified browser by either (a) clicking the spherical icon on the taskbar to the left, or (b) opening a terminal and running

cd ~/kraken/reflex/coq/bench-quark
./run.sh

More details about the browser are given at ~/kraken/reflex/coq/bench-quark/README.

Running the SSH Server

The SSH server is setup to run when the VM is started. Simply login to localhost to try it out.

More details about the SSH Server are given at ~/kraken/reflex/coq/bench-ssh/README.

Running the Web Server

In order to run the web server, do the following:

cd ~/kraken/reflex/coq/bench-webserver/ml
./kernel

Then you can connect to the web server from your favorite web browser and receive some static web pages.

Running the proof automation on our properties

cd ~/kraken/reflex/coq
make bench BENCHOUT=<results-dir> TIMEOUT=<timeout>

A single file called <results-dir>/results.csv will be created, giving, for each property, the time taken to produce a proof (Ltac), the time taken to check the proof (Qed), and the maximum memory used while creating the proof.

You can also tweak the automation optimizations that are run by modifying Opt.v. This file consists of six boolean valued expressions, each corresponding to an optimization.

Make sure that when you run the automation on these properties, the VM has at least 4GB of memory.

Because of the strange setup in our build system, running the proof automation deletes the binaries for all of our kernels. They must be rebuilt. To rebuild the binary for the kernel residing in ~/kraken/reflex/coq/bench-<name>, simply run

cd ~/kraken/reflex
make build NAME=<name>

Creating your own kernel

Place your kernel in ~/kraken/reflex/coq/bench-<name>. Under that directory, run

ln -s ../Makefile.bench Makefile
cd ~/kraken/reflex
make build NAME=<name>

The resulting binary will reside in ~/kraken/reflex/coq/bench-<name>/ml/kernel. If you want to check the policies for that kernel using our proof automation, run

cd ~/kraken/reflex/coq/bench-<name>
make policies

Source code/Directory structure

The root of the source code is at ~/kraken (kraken is an old name for the project). The implementation of the interpreter is located at ~/kraken/reflex/coq. A description of some of the files under that directory is given at ~/kraken/docs/source-docs.txt.

The kernels for the web browser, ssh server, and web server are located at ~/kraken/reflex/coq/bench-quark/Kernel.reflex, ~/kraken/reflex/coq/bench-ssh/Kernel.reflex, ~/kraken/reflex/coq/bench-webserver/Kernel.reflex, respectively.

Reflex frontend

As described in the paper, the Reflex frontend is written in python. The implementation is at ~/kraken/reflex/coq/parser_ply.py. A discussion of why we choose to implement the frontend in python is provided in ~/kraken/reflex/coq/frontend-discussion.txt.