A Typed Model for Dynamic Authorizations

TL;DR

This paper introduces a typed pi-calculus-based model for dynamic authorization in distributed systems, enabling secure communication and delegation with a novel scoping and typing discipline to prevent authorization errors.

Contribution

It presents a new model with authorization scoping and delegation primitives, ensuring safety through a typing system that prevents authorization errors during process execution.

Findings

The model supports dynamic authorization delegation.

The typing discipline guarantees error-free authorization handling.

Authorization boundaries are explicitly specified with new scoping constructs.

Abstract

Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to enrich communication-based systems with authorization specification and delegation; here authorizations regard channel usage and delegation refers to the act of yielding an authorization to another party. Our model includes: (i) a novel scoping construct for authorization, which allows to specify authorization boundaries, and (ii) communication primitives for authorizations, which allow to pass around authorizations to act on a given channel. An authorization error may consist in, e.g., performing an action along a name which is not under an appropriate authorization scope. We introduce a typing discipline that ensures that processes never reduce to authorization errors, even when authorizations are dynamically delegated.