A Witness Building Algorithm

What is this repository for?

Ocaml implementation of the module distinction algorithm mentioned in the APLAS 2015 paper:A Secure Compiler for ML Modules. The algorithm takes in 2 MiniML source files and 2 .traces files that are produced by these files. The implementation of the algorithm reuses the parser, type checker and static modules compiler of the secure compiler.

Setup

Set up the environment:

make setup

Compile the algorithm:

make now

Compile and run the tests:

make test

Repository Structure

• src/ : algorithm source code
• tests/ : a series of differing MiniML programs that the algorithm can build a witness for
• witness/ : the produced witnesses are placed here

License

Artistic License 2.0