A Refined State Monad, with applications to capability-based access control

Abstract:

Behavioural type and effect systems regulate properties such as adherence to object and communication protocols, dynamic security policies, avoidance of race conditions, and many others. Typically, each system is based on some specific syntax of constraints, and is checked with an ad hoc solver.

Instead, we advocate types refined with first-order logic formulas as a basis for behavioural type systems, and general purpose automated theorem provers as an effective means of checking programs.

To illustrate this approach, we give type systems for two related notions of permission-based access control: stack inspection and history-based access control. These type systems are both instances of a refined state monad.

Our main technical result is a safety theorem stating that no assertions fail when running a well-typed program.