Relational Hoare Type Theory (RHTT) for Information Flow and Access Control
===========================================================================

This directory contains the Coq files associated with the paper
"Verification of Information Flow and Access Control via Dependent Types"
by Aleks Nanevski, Anindya Banerjee and Deepak Garg.

The files develop libraries and examples for full program verification
in a higher-order and dependently typed variant of Relational Hoare
Logic.

Examples include implementations and verifications of a number of
security policies related to non-interference, declassification,
erasure, as well as state-based policies.

The developments require the Ssreflect extension of Coq V8.3 (have
been tested with patch level 2).

Obtaining and installing SSreflect
==================================

The current version of Ssreflect is available for Coq V8.4.

To install Ssreflect-1.4, download the sources at 

   http://www.msr-inria.inria.fr/Projects/math-components

unpack, and follow the instructions in the INSTALL and README files.

Compiling RHTT libraries and examples
=================================================

After unzipping the archive with RHTT code, go into the unzipped
directory, and set the following shell variables. These will be needed
in order to compile our code.

(1) set the HTT_DIR variable to the htt directory 
(2) set SSRCOQ_LIB to the directory in which you installed the Ssreflect .v and .vo files
(3) set COQBIN to the directory containing the ssrcoq binary (could be
empty if ssrcoq is in the path)

Then from the sources directory type the following. 
This will compile the basic libraries for heaps.

cd htt
make

Then to make the main RHTT code, type

cd ..
make

Description of the files 
========================

The directory contains the following files. 

 1. Make (the generator for the Makefile)

 2. htt/ordtype.v
    Library for types with a decidable ordering relation on them.

 3. htt/finmap.v
    Library for purely functional finite maps, i.e., partial functions
    from keys to values which are defined for only finitely many keys.

 4. htt/rels.v 
    Library for relations over arbitrary type.

 5. htt/heaps.v 
    Main definitions and lemmas related to the datatype of heaps.

 6. htt/hprop.v 
    Definitions and lemmas about separation logic predicates, i.e.,
    predicates over heaps.

 7. htt/domains.v
    Library for posets, CPO's and admissibility.

 8. secmod.v 
    Definition of the model for STsec types of RHTT.  This file is
    described in more detail in Section 3 of the paper. Lemmas about
    continuity of all the constructors. Plus, opaque sealing of the
    constructor definitions, so that reasoning is done only via specs,
    and not via the model.

10. seclog.v
    Inference rules of our logic; used for discharging the proof
    obligations generated by the programs. This file is described in
    more details in Section 4 of the paper.

10. seclogO.v
    Automation of inference rule selection using lemma overloading
    in the style of Gonthier, Zilliani, Nanevski and Dreyer. 
     
11. examples.v
    Some basic examples and experimentation. Contains the proofs for
    the Terauchi and Aiken example, which is presented (in a shortened
    form) in Example 1 of the paper.

12. alice.v
    The main set of examples about information flow and access
    control.  Contains the examples 2, 3, 4 and 5 from Section 2 of
    the paper.  It also contains a number of alternative
    implementations of the Alice signatures. 

13. alice2.v
    Alternative implementations of alice.v. 

14. llist.v
    A library of linked lists (not the one from the paper). Also
    contains the verification of the in-place reversal algorithm.

15. llist2.v
    Alternative specification of singly-linked lists.

16. llist3.v
    Yet another alternative specification of lists. This is the one 
    from Section 5 of the paper. Contains reasoining about low linkage
    and examples with heterogeneous lists.

17. principals.v
    An example introducing principals into the system, so that one can
    grant access based on the identity of the principal. Inspired by
    "Roles, stacks, histories: a triple for Hoare" by Borgstroem,
    Gordon and Pucella.

18. average.v
    An example with "multi-party" computation, where an average salary
    of two employees of a company is declassified, without
    declassifying the individual salaries.



