Project Description
A principal may represent a wide variety of elements in a computing environment: an operating system user, a piece of code, a communication channel, and so forth. In computer security, access control consists of determining whether a given principal should be trusted when issuing a request for some resource. Access control is particularly challenging in the context of distributed systems: there is no central authority to make security decisions, and mobile code may be assigned different trust-levels by different components of the system.
One can design a specialized logic
to reason about access control and enforce security policies. A natural question to ask is whether one can apply the Curry-Howard Isomorphism to such an authorization
logic, thereby yielding a type system for a programming language that can enforce access control
directly. Our goal is to design a suitable authorization logic, and thus a functional programming
language with which programmers can easily enforce and understand security policies via the type system.