Article Preview
TopIntroduction
The design of today’s information systems (IS) must not only take into account the expected functionalities of the system, but also various kinds of non-functional requirements. Security is one of these non-functional requirements. Security policies are designed to fulfil requirements such as confidentiality, integrity and availability. Security policies are usually expressed as abstract access control rules, independently of target technologies. In the past, various access control models have been proposed. In this paper, we focus on role-based access control models (RBAC) (Ferraiolo, Kuhn, & Chandramouli, 2003), including evolutions such as SecureUML (Basin, Doser, & Lodderstedt, 2006; Basin, Clavel, & Egea, 2011). An important feature of such models is the notion of role: permissions are granted to roles which represent functions in an institution. Each role corresponds to several users and users may play several roles with respect to the secure system.
Advanced RBAC models allow the specification of constraints such as Separation of Duty (SoD) properties (Clark & Wilson, 1987), and other properties on roles (e.g. precedence, presented in the next section). For information systems, contextual information may also be taken into account when granting permissions. This contextual information may correspond to the current state of the information system, or to the history of interactions with the system. This has led to the notion of authorisation constraint in SecureUML. An authorisation constraint combines functional and security concerns to grant a permission. This reveals the need to link the security model of the application to the functional model of the information system, often expressed as UML diagrams. Therefore, SecureUML (Basin et al., 2006) groups UML diagrams of the application with security information describing the access control rules. In the remainder, we will refer to the UML diagrams of the application as the functional model. The term security model will refer to the access control model. Other approaches have integrated security concerns into UML diagrams. Fernández (2004) proposes to address security concerns through the whole software development and builds on UML and patterns to structure his approach. UMLsec (Jürjens, 2004; Jürjens, Schreck, & Bartmann, 2008) is a methodology that annotates UML diagrams with security stereotypes which allow to perform security analyses with respect to a given attacker profile.
Contextual constraints give flexibility to describe security policies, but the resulting models are more complex to validate. Validation checks that the policy corresponds to the user’s requirements. Animation of the model can play a significant role in this validation activity, playing scenarios or answering questions about the consequences of the model. Animation also brings a limited level of verification: traces demonstrate that constraints are not contradictory.
When systems become complex, separation of concerns is often perceived as a good strategy to master complexity. In our context, this means that functional and security models should be validated separately. This explains why most existing works are mainly interested by the security part. Although it is definitely useful to first analyse both models in isolation, interactions between these models must also be taken into account. Such interactions result from the fact that constraints expressed in the security model also refer to information of the functional model. Hence, evolutions of the functional state will influence the security behaviour. Conversely, security constraints can impact the functional behaviour. For example, it is important to consider both security and functional models in order to check liveness properties on the information system. Indeed, it can be the case that security constraints are too strict and block the system.
In a previous version of this paper (Ledru, Idani et al., 2011), we have discussed the need to take into account functional models in the validation of security policies and we advocated for a formal approach to express these contextual constraints and validate them. In this paper, we extend this discussion by presenting the details of our formal approach, a tool support and its application to a case study, taken from a real medical emergency information system.