Article Preview
TopIntroduction
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.