Main Developer
Niklas Broberg
Contributors
David Sands
Bart van Delft
Yannick Zakowski
Javed Nazir
Filippo Del Tedesco
The following case studies have been performed using Paragon so far:
The sealed bids auction is an example where bidders can place a bid that remains secret until the auction is over and can only flow to the other bidders if their bid is the winning bid.
Download the sealed bid auction here and run under Linux make, possibly followed by make java. Note that at this moment runtime lock querying is not correctly translated into Java files which makes it not possible to compile them.
A more detailed description can be found in this draft paper on Paragon.
A Paragon implementation of the first large program written in Jif, which was described here by Askarov and Sabelfeld. There are two versions of the Paragon implementation.
Version 1 is an almost direct translation of the original work with only a few differences (in particular having a trusted declassifier and providing static guarantees instead of Jif's seal pattern).
Version 2 uses more of the expressive power of Paragon and where the original version had the same policy for all sensitive data, more flexible policies are here depending on how the data is used. A description can be found in this draft paper on Paragon.
To compile, make sure that Paragon is installed and the runtime jar is located in the top directory of the extracted zip file (see Download Paragon). Under Windows the example can be built by executing make.bat, under Linux by running make, possibly followed by make java. The resulting Mental Poker class files can then be run calling binder.py.