Access control requirements engineering, modeling and verification in multi-domain grid and cloud computing systems

Abstract

Grid and Cloud computing paradigms consist of modern distributed and collaborative systems, which became the de facto platforms for the development of a variety of applications. Despite being different in nature, several requirements and principles remain the same in both of them. Security is an essential principle that is required to be maintained during collaboration among domains. Nevertheless, few proposals have addressed the problem of how to maintain security among domains where each implements its own access control (AC) policy, and with the majority of them being static and not suitable for the examined systems.In this dissertation, the notions of AC requirements engineering, AC modeling and verification of security properties are fully integrated within a common systems engineering methodology. The contribution of this dissertation is multifold: we describe a systems engineering methodology for the development of AC systems; we describe our proposed steps; we define an AC model; and lastly, we define a technique for the verification of security properties. Looking towards a holistic approach on the definition of AC requirements, we propose a four-layer conceptual categorization and an evaluation framework for AC approaches. A comparative review of the examined AC models and mechanisms exposes their pros and cons. Apart from mapping the AC area in Grid and Cloud computing systems, the given comparison renders valuable information for further enhancement of current approaches.Moreover, we define an enhanced Role-Based Access Control (RBAC) model entitled domRBAC, based on the ANSI INCITS 359-2004 AC model. domRBAC intrinsically inherits RBAC’s virtues such as ease of management, and Separation of Duties (SoD) with the latter also being supported among multiple domains. The domRBAC model is capable of differentiating the security policies enforced in each domain and supports collaboration under secure inter-operation. Cardinality constraints along with the new element of containers are incorporated to provide simple usage management of resources for the first time in an RBAC model. Secure inter-operation is maintained among collaborating domains gradually and automatically. An implementation of a simulator based on the definitions of domRBAC helped to conduct with experimental results regarding the model’s performance. Concluding, we provide a formal definition of secure inter-operation properties in temporal logic, which can be verified using model checking techniques. The proposed technique consists of a generic one, and thus, can be used in any RBAC model to verify indirectly the correctness of the secure inter-operation functions that implement the global security policy. Finally, we provide examples that illustrate the verification of the defined secure inter-operation properties in RBAC policies, and an analysis of the proposed technique.

Τα Grid και Cloud υπολογιστικά συστήματα αποτελούν σύγχρονα κατανεμημένα και συνεργατικά συστήματα, τα οποία θεωρούνται ως οι εξ ορισμού πλατφόρμες για την ανάπτυξη μια πληθώρας διαφορετικών εφαρμογών. Παρά το γεγονός ότι αποτελούν διαφορετικού τύπου συστήματα, πολλές απαιτήσεις και αρχές παραμένουν κοινές. Η ασφάλεια αποτελεί μια βασική αρχή που πρέπει να διατηρείται κατά τη διάρκεια συνεργασίας μεταξύ διαφορετικών τομέων. Παρ' όλα αυτά, λίγες προτάσεις αντιμετωπίζουν το πρόβλημα της διατήρησης ασφάλειας μεταξύ διαφορετικών τομέων, όπου κάθε τομέας εφαρμόζει τη δική του πολιτική ελέγχου, με την πλειοψηφία των προτάσεων να αποτελούν στατικές προσεγγίσεις, οι οποίες κρίνονται μη κατάλληλες για εφαρμογή στα εξεταζόμενα συστήματα.Στην παρούσα διδακτορική διατριβή, οι έννοιες της μηχανικής απαιτήσεων ελέγχου πρόσβασης (ΕΠ), η μοντελοποίηση ΕΠ και ο έλεγχος ιδιοτήτων ασφαλείας έχουν ενσωματωθεί πλήρως στο πλαίσιο μιας μεθοδολογίας μηχανικής συστημάτων. Η συνεισφορά της παρούσας διπλωματικής εργασίας είναι πολύπλευρη: περιγράφουμε μια μεθοδολογία μηχανικής συστημάτων για την ανάπτυξη συστημάτων ΕΠ, περιγράφουμε τα προτεινόμενα βήματα, ορίζουμε ένα μοντέλο ΕΠ, και τέλος ορίζουμε μια τεχνική ελέγχου ορθότητας των ιδιοτήτων ασφαλείας.Στοχεύοντας σε μια ολιστική προσέγγιση όσον αφορά στον προσδιορισμό των απαιτήσεων ΕΠ, προτείνουμε μια εννοιολογική κατηγοριοποίηση τεσσάρων επιπέδων, καθώς και ένα μηχανισμό αξιολόγησης προσεγγίσεων ΕΠ. Σε μια συγκριτική επισκόπηση των εξεταζόμενων μοντέλων και μηχανισμών ΕΠ αποτυπώνονται τόσο τα πλεονεκτήματα όσο και τα μειονεκτήματα τους. Εκτός από την χαρτογράφηση της περιοχής ΕΠ στα Grid και Cloud υπολογιστικά συστήματα, η αποτύπωση τους λειτουργεί βοηθητικά στην περαιτέρω εξέλιξη των προσεγγίσεων ΕΠ.Εν συνεχεία, ορίζουμε το domRBAC το οποίο αποτελεί μια επέκταση του ANSI INCITS 359 - 2004 μοντέλου ΕΠ. Το domRBAC, κληρονομεί εγγενώς όλα τα πλεονεκτήματα του RBAC, όπως αποτελούν τα: ευκολία διαχείρισης, και η υποστήριξη πολιτικών διαχωρισμού καθηκόντων, με το τελευταίο να υποστηρίζεται και μεταξύ διαφορετικών τομέων. Το μοντέλο domRBAC είναι σε θέση να διαφοροποιεί τις πολιτικές ασφαλείας που εφαρμόζονται σε κάθε τομέα ενός συνεργατικού περιβάλλοντος εξασφαλίζοντας την ασφαλή δια-λειτουργικότητα μεταξύ τους. Η εφαρμογή περιορισμών πληθικότητας σε συνδυασμό με το νέο στοιχείο του περιέκτη προσδίδει στο domRBAC τη δυνατότητα απλής διαχείρισης χρήσης των πόρων, για πρώτη φορά σε ένα RBAC μοντέλο. Η ασφαλής δια-λειτουργικότητα υποστηρίζεται μεταξύ των συνεργαζόμενων τομέων σταδιακά και αυτόματα. Η υλοποίηση ενός εξομοιωτή βασισμένου στους ορισμούς του domRBAC οδήγησαν στην εξαγωγή πειραματικών αποτελεσμάτων όσον αφορά στην απόδοση του μοντέλου.Ολοκληρώνοντας, προτείνεται ένας φορμαλισμός των ιδιοτήτων της ασφαλούς δια-λειτουργικότητας σε temporal logic, των οποίων η ορθότητα μπορεί να ελεγχθεί κάνοντας χρήση model checking τεχνικών. Η προτεινόμενη τεχνική αποτελεί μια γενική προσέγγιση, και ως εκ τούτου, μπορεί να χρησιμοποιηθεί σε οποιοδήποτε μοντέλο RBAC με σκοπό να επαληθεύει έμμεσα την ορθότητα των μηχανισμών ασφαλούς δια-λειτουργικότητας που υλοποιούν τις καθολικές πολιτικές πρόσβασης. Τέλος, παρουσιάζονται παραδείγματα όσον αφορά στον έλεγχο ορθότητας των προτεινόμενων ιδιοτήτων σε RBAC πολιτικές, και αναλύεται η απόδοση της προτεινόμενης τεχνικής.