Towards Run-Time Verification in Access Control

The notion of "session" created a considerable debate in access control. Recent research demonstrated that many access control constraints can not be verified statically at design time. The user behavior during an active session is uncertain, sessions are concurrent and some authorization decision parameters (i.e. conditions) are only available at runtime. However, similarly to what is done in software verification, it is possible to give static indications about the run-tim behavior of the access control system, by analyzing a finite number of approximations that model both the user behavior and the decision parameters. Moreover, constraints (e.g. history-based ones) can be analyzed in combination rather than individually. In this paper, we present a framework tailored to the verification of run-time constraints and security properties (e.g. mutually exclusive roles) for role based access control systems. Our framework employs actors to mimic active entities at runtime and creates stochastic activity entropies from a set of permission and role activations. A security administrator can obtain a set of run-time trajectories with a finite number of simulations that can be used to verify the desired properties.