Detail

A Type System for Access Control in an Object-Oriented Language

Access control to objects in traditional object-oriented languages consists of
visibility modifiers, such as “public” and “private”. Similar solutions are
statically verified at compile time, but once an access policy is
established, it cannot be modified at runtime.

However, in most applications, more flexible access control mechanisms are
required, enabling, for example, dynamic modification of a principal’s access
privileges. It would be desirable to check such dinamically imposed access
control policies also statically, at least partially.

In this work, we introduce User Views – object references that have information
about the current privileges (a policy) held by a principal to a given
object. To support dynamic modification of a user view’s policy, we introduce
first class Authorizations, allowing different aliases to have different
policies over the same object. To demonstrate our concepts, we have developed
a core language, equipped with a provably correct type and effect system
capable of detecting unauthorized method calls at compile time.

We have also implemented a typechecking algorithm, resulting in a tool to
verify the integrity of protected objects in a system designed with the core
language.