AbstractsComputer Science

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

by Christos Grompanopoulos

Institution: Πανεπιστήμιο Μακεδονίας
Year: 2014
Keywords: Ασφάλεια πληροφοριών; Έλεγχος πρόσβασης; Έλεγχος χρήσης; Μοντελοποίηση; Τεχνικές επαλήθευσης; Ανοιχτά και δυναμικά υπολογιστικά περιβάλλοντα; Έλεγχος πρόσβασης βασιζόμενος σε χαρακτηριστικά; Computer security; Access control; Usage control; Modeling; Verification techniques; Open and dynamic computing environments; Attribute based access control
Record ID: 1155653
Full text PDF: http://hdl.handle.net/10442/hedi/34804


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…