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

This directory contains the Coq files associated with the paper

    "Modular Enforcement of Information Flow
          Policies in Data Structures"

The files develop libraries and examples for verification of full
functional correctness, information flow and information erasure policies
for data structures and their clients.  Verification is performed 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 noninterference, declassification,
erasure, as well as state-based policies.  Data structures implemented 
include arrays, bounded stacks and multisets and filter hash tables. 

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

The directory contains the following files. 

 1. Make (the generator for the Makefile)

RHTT base:

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

 3. 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. rels.v 
    Library for relations over arbitrary type.

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

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

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

 8. secmod.v
    Definition of the model for STsec types of RHTT.  

 9. seclog.v
    RHTT inference rules; used for discharging the proof
    obligations generated by the programs.

Paper-specific Files:

10. rbac.v
    Examples of simple role-based access control 

11. multilevel.v
    Examples of multilevel information flow in RHTT

12. simple_datatypes.v
    Barebones model of data structures 
    (Sec. 4)

13. datatypes.v 
    Enhanced model of data structures 
    (Sec. 4)

14. counter.v 
    Counter datatype. 

15. array.v
    Imperative array module used to construct other uniquely represented 
    data structures such as bounded multisets, bounded stacks and 
    UR filter hash tables
    (Sec. 4)

16. multiset.v 
    Uniquely represented insert-only bounded multisets 
    (Sec. 4)

17. stack.v
    Uniquely represented bounded stacks

18. kvmaps.v
    Key-value map and hashable key-value map interfaces; functional key-value
    maps implemented as association lists 
    (Sec. 5d)

19. min.v
    Supporting definitions and lemmas for UR filter hash tables
    (Sec. 5)

20. hashmap.v
    The main UR filter hash table development 
    (Sec. 5)

21. hospital.v
    Dynamic role-based access control 
    (Appendix A)

22. hashing_client.v
    Verification of higher-order erasure for a hospital client with 
    a UR filter hash table as local state 
    (Sec. 6)



