Information Flow Analysis for a Dynamically Typed Functional Language with
Staged Metaprogramming - Supporting Resources
* Submitted by Martin Lester, Luke Ong and Max Schaefer to CSF 2013 & JCS
===============================================================================

This distribution contains an implementation of a CFA-based information flow
analysis for the language SLamJS, written in OCaml, and proofs of its
correctness, mechanised in Coq. The contents are as follows:

* coq-if/*            A mechanisation of the coherence of the information flow
                      analysis with reduction.
* coq-if/lib.v        Auxiliary definitions for the mehanisation.
* coq-if/lambdajs.v   Labelled semantics of Staged Lambda JS.
* coq-if/simple_cfa.v Correctness proof of the information flow analysis
                      based on simple CFA. The coherence of the analysis
                      with evaluation is called "soundness".
* coq-if/cfa.v        Correctness proof of the information flow analysis
                      based on improved CFA. Again, coherence with
                      evaluation is called "soundness".

* coq-cfa/*           As coq-if/*, but without information flow analysis;
                      this is CFA only.

* demo1/*             An implementation of our information flow analysis for
                      SLamJS. It can also evaluate SLamJS programs.
* demo2/*             An implementation of the Boxing Algorithm for SLamJS
                      extended with eval.
* demo*/build.sh      Script to build the tool executable.
* demo1/slamjs        CFA/IF analysis tool executable.
* demo2/boxer         Boxing Algorithm executable.
* demo*/*.ml,*.mli    OCaml source code for the implementation.
* demo*/examples/*    Examples from our paper. Numbering matches JCS version.
* demo*/LICENCE       MIT/X Consortium licence for the implementation.

The implementations are intended primarily as a proof of concept, rather
than production-quality, fully optimised code. Nonetheless, they ought to
work! Run build.sh to compile either, then run the executable for a summary
of options.

The information flow analysis tool (demo1/slamjs) is somewhat more polished
than the Boxing Algorithm tool. As a start, you might like to try the
following from within the demo1 directory (and check they match examples in
the paper):

./slamjs --eval examples/ex05.slj
./slamjs --simple examples/ex05.slj
./slamjs --simple --if-only examples/ex05.slj
./slamjs --simple --if-only --terse examples/ex05.slj

./slamjs --simple --if-only --terse examples/ex13.slj
./slamjs --improved --if-only --terse examples/ex13.slj
or equivalently:
./slamjs --if-only --terse examples/ex13.slj

If you can view Graphviz graphs (for example, with xdot.py):
./slamjs --simple --dot examples/ex05.slj > examples/ex05.dot
xdot.py examples/ex05.dot

The release also includes experimental support for mutable references. Look
at the examples for more information.

The implementation of the Boxing Algorithm in demo2 has these limitations:

* it produces a lot of debug output;
* the implementation of the lexing check has not been completed;
* the algorithm is only integrated with the simple CFA/IF analysis.

However, it should be good enough to check the examples in the paper (and
many more besides):

./boxer --eval examples/box02-ex21.slj
./boxer --box examples/box02-ex21.slj

The Coq proofs have been tested in Coq 8.3pl4 (March 2012). The
implementation has been tested in OCaml 3.12.1. The supplied binaries were
built using these versions running under Debian 7 ("wheezy") on i386.

