This talk presents Relational Hoare Type Theory (RHTT), a language and verification system for expressing and verifying rich information flow and access control policies via dependent types. A number of security policies, such as conditional declassification, information erasure, and state-dependent information flow and access control, which have been formalized separately in security literature can all be expressed in RHTT using only standard type-theoretic constructions such as monads, higher-order functions, abstract types, abstract predicates, and modules. RHTT can reason about such policies in the presence of dynamic memory allocation, deallocation, pointer aliasing and arithmetic.