A Type Discipline for Authorization Policies

Cedric Fournet; Andrew D. Gordon; Sergio Maffeis. A Type Discipline for Authorization Policies. ESOP 2005.

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a new dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

Another "extreme" use of static typing...

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This Reminds Me of...

...Soutei, another of Oleg Kiselyov's projects.

Update: I should have mentioned that it also reminds me of Flow Caml, especially when you consider the research prompted by the paper I mentioned here.