RHTT: Relational Hoare Type Theory
Last modified: Tue Mar 10 17:02:50 CET 2015
RHTT is a verification system capable of expressing and verifying rich information flow and access control policies via dependent types. It is implemented as an embedded domain-specific language (DSL) in the dependently-typed language of the Coq proof assistant. RHTT is built on the observation that a number of security policies, which have been formalized separately in the literature, can all be usefully expressed using as combinations of standard type-theoretic constructions such as monads, higher-order functions, abstract types, abstract predicates, and modules. Example security policies include access control, state-dependent information flow, information erasure, and conditional declassification. RHTT can reason about such policies in the presence of dynamic memory allocation, deallocation, pointer aliasing and arithmetic.
Source code for RHTT is available here.