Formal Modelling and Verification of Security Policies in Cloud Computing

Abstract

This thesis tackles the problem of formal modelling and verification of security policies in cloud computing. Indeed, our research focuses on the modelling and the verification of access control policies using Coloured Petri Nets (CPNs). Due to its ability to reduce complexity, Role Based Access Control (RBAC) model was one of the predominant models for access control and the specification of security policies. In its original version, RBAC does not consider several important events, thus, TRBAC (Temporal RBAC) was proposed as an RBAC extension. This thesis provides three basic contributions. In the first contribution, HTCPNs (Hierarchical Timed Colored Petri Nets) formalism is used to model the TRBAC (Temporal Role Based Access Control) policy, and then the CPN-tool is exploited to analyse the obtained models. Indeed, the timed aspect in HTCPN allows us to deal with temporal constraints in TRBAC. The hierarchical aspect of HTCPN makes the TRBAC model “manageable”, despite the complexity of the policy. RBAC as well as TRBAC suffer from several drawbacks in large scale networks as the case of cloud environment. Although Attribute Based Access Control (ABAC) model handles some RBAC drawbacks, ABAC misses RBAC advantages. Hence, as a second contribution, we propose an access control model FRABAC (Fine-Grained Role Attribute Based Access Control) that provides scalability, flexibility, and fine granularity in the cloud environment. FRABAC combines and extends, basically, two models RBAC and ABAC. In order to demonstrate the advantages of the new proposed model, an empirical study is realised. In this study, the new proposed model is compared versus three existing models, using specific metrics. The results demonstrate that the new proposed model is more suitable than existing ones. As a third contribution, we provide a formal specification/ verification of FRABAC using HTCPN formalism and CPN-tool.