A Valid and Correct-by-Construction Formal Specification of RBAC

A Valid and Correct-by-Construction Formal Specification of RBAC

Hania Gadouche (LIMED Laboratory, Faculty of Exact Sciences, University of Bejaia., Bejaia, Algeria), Zoubeyr Farah (LIMED Laboratory, Faculty of Exact Sciences, University of Bejaia., Bejaia, Algeria) and Abdelkamel Tari (LIMED Laboratory, Faculty of Exact Sciences, University of Bejaia., Bejaia, Algeria)
Copyright: © 2020 |Pages: 21
DOI: 10.4018/IJISP.2020040103

Abstract

Controlling access to data is one of the primary purposes of security, especially when it comes to dealing with safety critical systems. In such systems, it is of paramount importance to rigorously define access control models. In this article, a correct-by-construction specification of RBAC using the Event-B formal method is proposed. The specification defines closely the model properties with the behavior aspect of RBAC as guards of events, which allows applying a priori verifications. Accordingly, the resulted specification is correct-by-construction and avoids the combinatorial explosion problem. As well, a number of refinement operations are performed leading to a specification with several abstraction levels, where each level implements selected RBAC entities. The approach is illustrated by an instantiation of a healthcare system.
Article Preview
Top

Introduction

Access control is a security mechanism that is used to grant or deny, to users, access rights to resources. In safety critical systems (healthcare systems, air traffic control, railway systems, nuclear engineering …), guaranteeing a correct specification of access control models is crucial, due to the delicate nature of the field. Hence, an access control model must be rigorously specified, validated and verified before its deployment. The validation task includes ensuring validity of the declarative aspect (i.e. entities typing and relations definition between them), whereas the verification concerns the specification consistency (i.e. correctness of the behavioral aspect). This paper addresses the Role-Based Access Control model (RBAC) (American National Standards Institute (ANSI), 2012) which is widely used for its simplified access concept: permissions are granted to roles.

In the literature, several RBAC model specifications have been proposed (Dia & Farkas, 2013; Ferrari, 2005; Hu, Kuhn, & Yaga, 2017; Omran, Grandison, Nelson, & Bokma, 2013). Regardless of used formalisms, the validation and verification of RBAC models are generally based on checking process that uses a posteriori verification (Al-Hadhrami, Aziz, & ben Othmane, 2016; Shafiq, Masood, Joshi, & Ghafoor, 2005). A posteriori verification includes solutions that are based on model checking, testing or simulation. However, the increasing complexity of systems makes the checking process more difficult and can be adversely affected by the combinatorial explosion problem. Furthermore, the solutions that are based on a posteriori verification are less appropriate for safety critical systems where access control must be rigorously defined. Some works have attempted to overcome these limitations by using formal methods to specify access control (Ferrier-Belhaouari, Konopacki, Laleau, & Frappier, 2012; Hu & Ahn, 2008; Huynh, Frappier, Mammar, Laleau, & Desharnais, 2016; Li, Byun, & Bertino, 2007; Yuan, Y.He, J.He, & Zhou, 2006). Most of these solutions define a specification that integrates both a priori (formal) and a posteriori verification in order to support large-scale systems.

In this paper, a correct-by-construction solution using the Event-B method is proposed. Several works in the literature have used Event-B to specify RBAC (Al-Hadhrami et al., 2016; Hoang, Basin, & Abrial, 2009; Huynh et al., 2016). However, most of these approaches deal only with the declarative (static) aspect of RBAC without covering the behavioral (dynamic) features. The proposed solution deals with both of the declarative and the behavioral aspects.

The Event-B formal method is used since it allows systems specification according to a correct-by-construction methodology, additionally, it provides a large selection of tools and techniques for specifying, validating and checking properties of systems.

Complete Article List

Search this Journal:
Reset
Open Access Articles
Volume 14: 4 Issues (2020): 2 Released, 2 Forthcoming
Volume 13: 4 Issues (2019)
Volume 12: 4 Issues (2018)
Volume 11: 4 Issues (2017)
Volume 10: 4 Issues (2016)
Volume 9: 4 Issues (2015)
Volume 8: 4 Issues (2014)
Volume 7: 4 Issues (2013)
Volume 6: 4 Issues (2012)
Volume 5: 4 Issues (2011)
Volume 4: 4 Issues (2010)
Volume 3: 4 Issues (2009)
Volume 2: 4 Issues (2008)
Volume 1: 4 Issues (2007)
View Complete Journal Contents Listing