Specification and verification of an attribute-based usage control approach for open and dynamic computing environments

Abstract

Computing systems are always evolving in order to keep pace with the requirements posed by their users. For example, widespread of networking technologies has resulted in the transition from the standalone computer model to the client-server computer model. Moreover, social trends as frequent travelling and social networking, led to the creation of small-sized computing devices that are equipped with sensors to recognize their surrounding environment and adapt accordingly to it. Therefore, novel computing environments were emerged, as ubiquitous computing, grid - cloud computing systems and the Internet of Things. The aforementioned computing environments set new requirements in several areas, including the very important area of security. Specifically, from a computer security, and particularly from an access control point of view, the evolution of computing systems induces the creation of Open and Dynamic Computing Environments (ODCE). These environments are characterized as open since there are no boundaries between the legitimate and illegal users of a system. And they are characterized as dynamic since their configuration is constantly changing. Nevertheless, existing access control approaches are not designed for application in ODCE and thus, they cannot fully support the unique requirements posed by ODCE. Consequently, an exhaustive requirements analysis regarding access control models that are targeted to ODCE is required, which will subsequently help in the definition of proper access control approaches for application in ODCE.In this dissertation, we analyze existing access and usage control approaches to identify a number of unique requirements posed by ODCE. Secondly, we formally define an attribute based usage control model for ODCE that is designed based on the identified requirements. Last but not least, we check the proposed model for its correctness, i.e., the adherence of the model to its initially defined specifications.Specifically, we provide information on the RBAC, ABAC and UCON access/usage control models, which are mostly applicable in the examined case of ODCE. Moreover, we present information regarding the modeling of concurrent systems, as the access control systems. The aforementioned information helps in the identification of the demanded specifications in the context of access/usage control models in ODCE. Moreover, state-of-the-art verification techniques are described since it is required to check the correctness of the newly defined models in respect to their initial specifications. In turn, we highlight through representative usage scenarios the challenging issues and limitations that are introduced when attempting to utilize the UCON family of models in modern computing environments. Based on the requirement analysis results of access control in ODCE, we propose a formal specification of UseCON model using the Temporal Logic of Actions (TLA+) formal language. Consequently, we evaluate UseCON, which incorporates a number of significant features compared with existing access/usage control models. The proposed model, firstly, results in support of extended expressiveness over the existing usage control models. This extended expressiveness of UseCON stems from the utilization, during the creation of usage allowance decision, of information originating from either a single or a set of both direct and indirect entities. Secondly, UseCON inherently supports the utilization of historical information of usages through the automatic management of use entities. Additional advantages of the proposed model are considered to be its support for simplified policy administration processes, and additional unique features like the negotiation of actions etc. In order to prove the correctness of the defined UseCON model we contacted research on formal verification techniques, thus, resulting in the definition of a set of safety and liveness properties. The verification of the defined set of properties was performed by applying a model checking technique with the TLC model checker. We conclude this dissertation by providing additional information regarding the TLC verification process, and further discuss our findings, pointing to the contributions of this research work and to possible future research directions, as well

Τα υπολογιστικά συστήματα εξελίσσονται συνεχώς προκειμένου να αντεπεξέλθουν στις απαιτήσεις που θέτουν οι χρήστες τους. Η εξάπλωση των τεχνολογιών δικτύου οδήγησε στη μετάβαση από το μοντέλο αυτόνομου υπολογιστή στο μοντέλο εξυπηρετητή – πελάτη. Επιπρόσθετα, κοινωνικές τάσεις όπως η συχνή μετακίνηση και η κοινωνική δικτύωση οδήγησαν στη δημιουργία υπολογιστικών συσκευών μικρών σε μέγεθος, οι οποίες είναι εξοπλισμένες με αισθητήρες προκειμένου να αναγνωρίζουν το περιβάλλον και να προσαρμόζουν αντίστοιχα τη λειτουργία τους σε αυτό. Κατά συνέπεια, προέκυψαν καινούργια υπολογιστικά περιβάλλοντα όπως το περιβάλλον διάχυτης υπολογιστικής (ubiquitous computing), τα περιβάλλοντα πλαισίου (grid) – σύννεφου (cloud) και το διαδίκτυο των πραγμάτων (Internet of Things). Τα προαναφερόμενα υπολογιστικά περιβάλλοντα δημιουργούν νέες απαιτήσεις σε διάφορους τομείς, συμπεριλαμβανομένου και αυτού της ασφάλειας, της οποίας ο ρόλος είναι εξέχουσας σημασίας. Συγκεκριμένα, όσον αφορά την ασφάλεια υπολογιστών και ειδικότερα τον έλεγχο πρόσβασης, η εξέλιξη των υπολογιστικών συστημάτων συνετέλεσε στη δημιουργία των Ανοιχτών και Δυναμικών Υπολογιστικών Περιβαλλόντων (ΑΔΥΠ). Τα ΑΔΥΠ χαρακτηρίζονται ως ανοιχτά μιας και δεν υπάρχει σαφές όριο ανάμεσα στους εξουσιοδοτημένους και τους παράνομους χρήστες του συστήματος. Επίσης χαρακτηρίζονται ως δυναμικά καθώς η σύνθεσή τους συνεχώς μεταβάλλεται. Επιπρόσθετα, οι υπάρχουσες προσεγγίσεις ελέγχου πρόσβασης δεν έχουν σχεδιαστεί για την εφαρμογής τους στα ΑΔΥΠ, γεγονός που μας οδηγεί στο συμπέρασμα ότι δεν μπορούν να ικανοποιήσουν πλήρως τις μοναδικές απαιτήσεις που τα ίδια θέτουν. Κατά συνέπεια, απαιτείται μια ενδελεχής ανάλυση των απαιτήσεων αναφορικά με τα μοντέλα ελέγχου πρόσβασης που στοχεύουν στα ΑΔΥΠ, η οποία επακόλουθα θα βοηθήσει στον ορισμό κατάλληλων προσεγγίσεων ελέγχου πρόσβασης για την εφαρμογή τους σε αυτά.Σε αυτή τη διατριβή αναλύουμε τις υπάρχουσες προτάσεις ελέγχου πρόσβασης και χρήσης, με σκοπό να αναγνωρίσουμε έναν αριθμό μοναδικών απαιτήσεων που θέτουν τα ΑΔΥΠ. Κατά δεύτερο λόγο, ορίζουμε φορμαλιστικά ένα μοντέλο ελέγχου χρήσης βασιζόμενοι σε χαρακτηριστικά για τα ΑΔΥΠ, το οποίο σχεδιάστηκε βάσει των απαιτήσεων που εντοπίστηκαν. Τελευταίο μα όχι λιγότερο σημαντικό, ελέγχουμε το προτεινόμενο μοντέλο για την ορθότητά του, δηλαδή την προσήλωσή του στις αρχικά οριζόμενες απαιτήσεις.Συγκεκριμένα, παρουσιάζουμε πληροφορίες για τα RBAC, ABAC, και UCON μοντέλα, τα οποία κατά κόρον εφαρμόζονται στην εξεταζόμενη περίπτωση των ΑΔΥΠ. Επίσης, αναφέρουμε πληροφορίες σχετικές με τη μοντελοποίηση παράλληλων συστημάτων, όπως τα συστήματα ελέγχου πρόσβασης. Οι προαναφερόμενες πληροφορίες συνεισφέρουν στην αναγνώριση των προδιαγραφών στο πλαίσιο της μοντελοποίησης των μοντέλων ελέγχου πρόσβασης/χρήσης στα ΑΔΥΠ. Επιπρόσθετα, περιγράφουμε σύγχρονες τεχνικές επαλήθευσης, καθώς απαιτείται ο έλεγχος της ορθότητας των εκ νέου οριζόμενων μοντέλων σε σχέση με τις αρχικά οριζόμενες προδιαγραφές τους. Στη συνέχεια, τονίζουμε μέσω αντιπροσωπευτικών σεναρίων χρήσεων τις προκλήσεις και τους περιορισμούς που ενυπάρχουν κατά την προσπάθεια αξιοποίησης της οικογένειας μοντέλων UCON στα σύγχρονα υπολογιστικά περιβάλλοντα.Με σκοπό να ικανοποιήσουμε τις απαιτήσεις που θέτουν τα ΑΔΥΠ προτείνουμε και ορίζουμε μια αυστηρά φορμαλιστική περιγραφή του μοντέλου UseCON χρησιμοποιώντας την Temporal Logic of Actions (TLA+) γλώσσα φορμαλισμού. Στη συνέχεια πραγματοποιούμε μια αποτίμηση του UseCON, το οποίο εμπεριέχει έναν αριθμό σημαντικών χαρακτηριστικών συγκρινόμενο με τα υπάρχοντα μοντέλα ελέγχου πρόσβασης/χρήσης. Καταρχάς, το προτεινόμενο μοντέλο παρουσιάζει επαυξημένη εκφραστικότητα συγκρινόμενο με τα υπάρχοντα μοντέλα ελέγχου χρήσης, εξαιτίας της ικανότητάς του να αξιοποιεί πληροφορία προερχόμενη είτε από μία είτε από ένα σύνολο από άμεσες και έμμεσες οντότητες κατά τη διάρκεια της δημιουργίας απόφασης για επιτρεπόμενη πρόσβαση. Κατά δεύτερο λόγο, το UseCON εγγενώς υποστηρίζει την αξιοποίηση της πληροφορίας που αφορά ιστορικό χρήσεων διαμέσου της αυτοματοποιημένης διαχείρισης των χρήσεων. Επιπρόσθετα πλεονεκτήματα του προτεινόμενου μοντέλου είναι η δυνατότητα υποστήριξης απλοποιημένης διαδικασίας διαχείρισης πολιτικών και η υποστήριξη επαυξημένων κανόνων πολιτικών όσον αφορά την εκφραστικότητά τους.Με στόχο την απόδειξη της ορθότητας του μοντέλου UseCON που ορίσαμε πραγματοποιούμε έρευνα σχετική με τεχνικές φορμαλιστικής επαλήθευσης, που έχει ως αποτέλεσμα τον ορισμό ενός συνόλου ιδιοτήτων ασφάλειας και ζωτικότητας. Η επαλήθευση αυτού του συνόλου ιδιοτήτων πραγματοποιήθηκε με την εφαρμογή μιας τεχνικής ελέγχου μοντέλων που χρησιμοποιεί τον TLC. Τέλος, ολοκληρώνουμε αυτή τη διατριβή με την παράθεση επιπρόσθετων πληροφοριών αναφορικά με τη διαδικασία επαλήθευσης με τη χρήση του TLC και αναλύουμε περαιτέρω τα ευρήματά μας καθορίζοντας τις συνεισφορές αυτής της ερευνητικής εργασίας καθώς και τις πιθανές μελλοντικές κατευθύνσεις έρευνας.