A Calculus for Modeling Floating Authorizations

TL;DR

This paper introduces a process calculus model for floating authorizations in distributed systems, capturing domain, accounting, and delegation, with semantics and typing to ensure systems do not get stuck due to authorization issues.

Contribution

It presents a novel calculus for floating authorizations, including semantics and a typing discipline to prevent deadlocks caused by missing authorizations.

Findings

Operational semantics in two forms clarify authorization nature

Typing discipline ensures systems are not stuck due to authorization issues

Model effectively captures floating license dynamics in distributed systems

Abstract

Controlling resource usage in distributed systems is a challenging task given the dynamics involved in access granting. Consider, for instance, the setting of floating licenses where access can be granted if the request originates in a licensed domain and the number of active users is within the license limits, and where licenses can be interchanged. Access granting in such scenarios is given in terms of floating authorizations, addressed in this paper as first class entities of a process calculus model, encompassing the notions of domain, accounting and delegation. We present the operational semantics of the model in two equivalent alternative ways, each informing on the specific nature of authorizations. We also introduce a typing discipline to single out systems that never get stuck due to lacking authorizations, addressing configurations where authorization assignment is not statically prescribed in the system specification.