A correct-by-construction model for attribute-based access control
- PDF / 1,082,910 Bytes
- 12 Pages / 595.276 x 790.866 pts Page_size
- 20 Downloads / 227 Views
(0123456789().,-volV)(0123456789(). ,- volV)
A correct-by-construction model for attribute-based access control Illustration: web-based healthcare services Hania Gadouche1
•
Zoubeyr Farah1 • Abdelkamel Tari1
Received: 4 May 2019 / Revised: 4 May 2019 / Accepted: 16 August 2019 Ó Springer Science+Business Media, LLC, part of Springer Nature 2019
Abstract In this paper, a formal specification approach of the attribute-based access control (ABAC) is proposed using the Event-B method. We apply an a priori formal verification to build a correct model in a stepwise manner. Correctness of the specification model is insured during the construction steps. The model is composed of abstraction levels that are generated through refinement operations. A set of ABAC properties is defined in each level of refinement starting from the highest abstract level to the most concrete one. These properties are preserved by proofs with the behavior specification. The approach is illustrated in healthcare web services. Keywords ABAC Correct-by-construction Event-B Formal methods Proof and refinement Specification and validation A priori verification Web services Healthcare systems
1 Introduction In safety-critical systems, serious vulnerabilities can result from incorrect access definition to sensitive data. Access control policies (ACP) are a common solution for controlling access to resources. Hence, several access control models have been proposed in the literature [10, 18, 21, 26], namely the mandatory access control (MAC), the discretionary access control (DAC), the role based access control (RBAC) and the attribute based access control (ABAC). Each access model has been designed to meet specific security requirements. Moreover, research on the MAC, DAC, RBAC and ABAC has proven that an access control model, which can express the RBAC policies is also capable of enforcing both MAC and DAC
policies, as long as ABAC can express RBAC policies. The ABAC model improves RBAC since it enables fine-grained access control by defining the notion of attributes. The additional use of attributes when defining access control rules may enforce the met shortcomings and make the handled objects more reachable in a secured way. Validating and ensuring correctness of ACP specifications generally involve the use of systematic verification [11] which consists of checking absence of inconsistency and incompleteness in the built model. Regardless of used formalism, many specification and verification approaches are based on testing, simulation or model checking. These latter implement an a posteriori verification techniques [7] but are generally restricted to the following limitations:
& Hania Gadouche [email protected]
– The state-space explosion problem, – The checking is performed when the model instantiation is achieved.
Zoubeyr Farah [email protected] Abdelkamel Tari [email protected] 1
Medical Computing Laboratory(LIMED), Computer Science Department, Faculty of Exact Sciences, University of Bejaia, Bejaia, Algeri
Data Loading...
