|
Résumé :
|
Cette thèse aborde le problème de la modélisation/vérification formelles des politiques de sécurité dans le cloud computing. En effet, nos recherches portent sur la modélisation et la vérification des politiques de contrôle d’accès à l’aide de réseaux de Petri colorés (RdPCs). En raison de sa capacité à réduire la complexité, le modèle de contrôle d’accès basé sur le rôle (RBAC) était l’un des modèles prédominants pour le contrôle d’accès et la spécification de politiques de sécurité. Dans sa version originale, RBAC ne prend pas en compte plusieurs événements importants; par conséquent, TRBAC (Temporal RBAC) a été proposé comme une extension de RBAC. Cette thèse fournit trois contributions de base. Dans la première contribution, le formalisme HTCPNs (Réseaux de Petri Colorés Temporisés et Hiérarchiques) est utilisé pour modéliser les politiques TRBAC (Timed RBAC), puis l’outil CPN est exploité pour analyser les modèles obtenus. En effet, l’aspect temporisé dans HTCPN nous permet de gérer les contraintes temporelles dans TRBAC, et l’aspect hiérarchique du formalisme rend le modèle TRBAC “gérable”, malgré la complexité de la politique. Les systèmes RBAC et TRBAC présentent plusieurs inconvénients dans les réseaux à grande échelle, comme dans le cas de could computing. Bien que le modèle de contrôle d’accès basé sur les attributs (ABAC) gère certains inconvénients du RBAC, celui-ci manque les avantages du RBAC. Par consequence et comme une deuxième contribution, nous proposons un nouveau modèle de contrôle d’accès dit FRABAC (Contrôle d’accès basé sur les attributs et les rôles) qui offre une évolutivité, une flexibilité et une granularité fine dans l’environnement cloud. FRABAC combine et étend les deux modèles RBAC et ABAC. Afin de démontrer les avantages du nouveau modèle proposé, une étude empirique est réalisée. Dans cette étude, le nouveau modèle proposé est comparé à trois autres modèles existants, en utilisant des métriques spécifiques. Les résultats démontrent que le nouveau modèle FRABAC est plus approprié que les modèles existants. Enfin et comme une troisième contribution, nous avons réalisé une spécification/vérification formelle de FRABAC à l’aide du formalisme HTCPN et de l’outil CPN-tool.
|
