Automated Analysis of Access Control Policies Based on Model Checking
- PDF / 2,415,094 Bytes
- 16 Pages / 595.276 x 790.866 pts Page_size
- 16 Downloads / 233 Views
ORIGINAL RESEARCH
Automated Analysis of Access Control Policies Based on Model Checking Anh Truong1 Received: 16 April 2020 / Accepted: 23 August 2020 © Springer Nature Singapore Pte Ltd 2020
Abstract Access control is becoming increasingly important for today’s ubiquitous systems which provide mechanism to prevent sensitive resources against unauthorized users. In access control models, the administration of access control policies is a task of paramount importance for distributed systems. A crucial analysis problem is to foresee if a set of administrators can give a user an unauthorized access permission. In this paper, we consider the analysis problem in the context of the administrative role-based access control (ARBAC) and its extension, the administrative temporal role-based access control (ATRBAC). More details, we present how to design analysis techniques, namely asasp2.1 and asaspTIME2.0 for ARBAC and ATRBAC, respectively, which are based on the ideas of a framework to analyze infinite state-transition systems. Moreover, we describe how we design heuristics to enable the analysis techniques to scale up to handle large and complex authorization policies. An extensive experimentation shows that the proposed techniques are scalability and the heuristics play a key role in the success of the analysis tools over well-known analysis techniques. Keywords Access control · Security analysis · Automated verification · Model checking · Role-based access control · Temporal role-based access control · Administration
Introduction Modern information systems contain sensitive information and resources that need to be protected against unauthorized users who want to steal it. The most important mechanism to prevent this is access control [1] which is thus becoming increasingly important for today’s ubiquitous systems. In general, access control systems protect the resources of the systems by controlling who has permission to access what objects/resources. In access control, the administration of access control policies is a task of paramount importance for the flexibility and security of many distributed systems [2–8]. For flexibility, administrative actions are carried out by several
This article is part of the topical collection “Future Data and Security Engineering 2019” guest edited by Tran Khanh Dang. * Anh Truong [email protected] 1
HoChiMinh City University of Technology, VNU-HCM, Ho Chi Minh City, Vietnam
security officers. For security, the capabilities of performing such operations must be limited to selected parts of the access control policies, since officers can only be partially trusted. Indeed, flexibility and security are opposing forces, and avoiding under- or over-constrained specifications of administrative actions is of paramount importance. In this respect, it is crucial to foresee if a user can get a certain permission by a sequence of administrative actions executed by a set of administrators (i.e., the reachability problem). Since it is difficult to take into account the effect of all pos
Data Loading...
