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.
Contributors:
Aleksandar Nanevski
Deepak Garg
Gordon Stewart
Anindya Banerjee
Source code for RHTT is available here.
Supplementary material: