| Titre : | Formal modelling and verification of security policies in cloud computing |
| Auteurs : | Hasiba Benattia, Auteur ; Laïd Kahloul, Directeur de thèse ; Saber Benharzalah, Directeur de thèse |
| Type de document : | Thése doctorat |
| Editeur : | Biskra [Algérie] : Faculté des Sciences Exactes et des Sciences de la Nature et de la Vie, Université Mohamed Khider, 2019 |
| Format : | 1 vol. (102 p.) / 30 cm |
| Langues: | Anglais |
| Mots-clés: | Access Control,Security Policy,RBAC,ABCA,FRABAC,Formal Modelling,Formal Analysing,Petri nets,Cloud Computing. |
| Résumé : |
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 thecomplexity 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 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. |
| Sommaire : |
General Introduction 10 I Security, Security Policies and Formal Methods (Coloured Petri Nets) 14 I.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 I.2 Security Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 I.3 Security Policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 I.4 History of access control policies . . . . . . . . . . . . . . . . . . . . . . 16 I.5 Access Control policies . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 I.5.1 Mandatory Access Control (MAC) . . . . . . . . . . . . . . . . . 18 I.5.2 Discretionary Access Control Policies (DAC) . . . . . . . . . . . 19 I.5.3 Role Based Access Control (RBAC) . . . . . . . . . . . . . . . . 20 I.5.4 Attribute-Based Access Control (ABAC) . . . . . . . . . . . . . 24 I.6 Formal Analysing and Verification methods . . . . . . . . . . . . . . . . 24 I.6.1 Hierarchical Timed Coloured Petri Nets . . . . . . . . . . . . . . 25 I.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 II First Contribution: Using Hierarchical Timed Coloured Petri Nets in the Formal Study of TRBAC Security Policies 31 II.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 II.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 II.3 Modelling and Analysis of TRBAC policy using Hierarchical Timed-CPN 35 II.3.1 The Illustrative example: The Algerian justice information system policy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 II.3.2 The global TRBAC model . . . . . . . . . . . . . . . . . . . . . 40 II.3.3 Modelling of role-enabling and role-disabling events . . . . . . . 41 II.3.4 Modelling of role-“assignment/deassignment” events and role-“activation/deactivation” events . . . . . . . . . . . . . . . . 44 II.3.5 Formalisation and verification of properties . . . . . . . . . . . . 50 II.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 III Second Contribution: Fine-grained Role-Attribute based Access Control model (FRABAC ): A New Hybrid Access Control Model 59 III.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 III.2 Related work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 III.3 A new hybrid access control model . . . . . . . . . . . . . . . . . . . . . 61 III.3.1 Requirements for a suitable access control model . . . . . . . . . 61 III.3.2 Principle of the proposed model . . . . . . . . . . . . . . . . . . 62 III.3.3 Collaborative Cloud Services case in the proposed model . . . . . 63 III.3.4 The security policy under the proposed model . . . . . . . . . . . 65 III.4 Evaluation of the new proposed model: empirical comparison with existing models III.4.1 Metrics used in the empirical comparison approach . . . . . . . . 70 III.4.2 The illustrative example . . . . . . . . . . . . . . . . . . . . . . 70 III.4.3 RBAC configuration evaluation . . . . . . . . . . . . . . . . . . 71 III.4.4 ABAC configuration evaluation . . . . . . . . . . . . . . . . . . 74 III.4.5 AERBAC configuration evaluation . . . . . . . . . . . . . . . . . 76 III.4.6 Evaluation of the new proposed model . . . . . . . . . . . . . . . 77 III.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 IV Third Contribution: Using Hierarchical Coloured Petri Nets in the Formal Study of FRABAC Security Policies 80 IV.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81 IV.2 Specification of the request evaluation process . . . . . . . . . . . . . . . 81 IV.2.1 Required types for the HCPN model . . . . . . . . . . . . . . . . 82 IV.2.2 Modelling the identification process . . . . . . . . . . . . . . . . 83 IV.2.3 Modelling the evaluation process . . . . . . . . . . . . . . . . . 84 IV.3 Formal verification using CPN-tool of the HCPN models . . . . . . . . . 89 IV.3.1 Formalization and verification of properties on the request identification IV.3.2 Formalization and verification of properties on the request evaluation IV.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 General Conclusion 93 |
| En ligne : | http://thesis.univ-biskra.dz/id/eprint/4368 |
Disponibilité (1)
| Cote | Support | Localisation | Statut |
|---|---|---|---|
| TINF/138 | Théses de doctorat | bibliothèque sciences exactes | Consultable |
