In computer security, resources can be protected by the enforcement of a formally specified access control policy. Policy enforcement implies interaction between a policy specification and program behaviour. We propose to model this interaction with type theory, and present a pure, functional programming language in which access control policies are intrinsic and statically enforced. In addition, we develop a call-by-name operational semantics, and prove progress and type preservation. The underlying type system incorporates constructive authorization logic into contextual modal type theory. As a result, ordinary computation interacts with a policy expressed in authorization logic. Policy enforcement is thus integrated into the software development process, and the secure behaviour of programs is established at compile time.
Full Text.