Automated Security Analysis of Authorization Policies with Contextual Information

Role-Based Access Control (RBAC) has made great attention in the security community and is widely deployed in the enterprise as a major tool to manage security and restrict system access to unauthorized users. As the RBAC model evolves to meet enterprise requirements, the RBAC policies will become complex and need to be managed by multiple collaborative administrators. The collaborative administrator may interact unintendedly with the policies, creates the undesired effect to the security requirements of the enterprise. Consequently, researchers have studied various safety analyzing techniques that are useful to prevent such issues in RBAC, especially with the Administrative Role-Based Access Control (ARBAC97). For critical applications, several extensions of RBAC, such as Spatial-Temporal Role-Based Access Control (STRBAC), are being adopted in recent years to enhance the security of an application on authorization with contextual information such as time and space. The features, which proposed in STRBAC for collaborative administrators, may interact in subtle ways that violate the original security requirements. However, the analysis of it has not been considered in the literature.

In this research, we consider the security analysis technique for the extension of STRBAC, named Administrative STRBAC (ASTRBAC), and illustrate the safety analysis technique to detect and report the violation of the security requirements. This technique leverages First-Order Logic and Symbolic Model Checking (SMT) by translating the policies to decidable reachability problems, which are essential to understand the security policies and inform policies designer using this model to take appropriate actions. Our extensive experimental evaluation demonstrates the correctness of our proposed solutions in practice, which supports finite ASTRBAC policies analysis without prior knowledge about the number of users in the system.