ALPS: An Action Language for Policy Specification and Automated Safety Analysis

Authorization conditions of access control policies are complex and varied as they might depend, e.g., on the current time, the position of the users, selected parts of the system state, and even on the history of the computations. Several models, languages, and enforcement mechanisms have been proposed for different scenarios. Unfortunately, this complicates the verification of safety, i.e. no permission is leaked to unauthorized users. To avoid these problems, we present an intermediate language called Action Language for Policy Specification. Two desiderata drive its definition: (i) it should support as many models and policies as possible and (ii) it should be easily integrated in existing verification systems so that robust techniques (e.g., model checking or satisfiability solving) can be exploited to safety. We argue (i) by using selected examples of access control models and policies taken from the literature. For (ii), we prove some theoretical properties of the language that pave the way to the definition of automatic translations to available verification techniques.