Formale Spezifikation, Verifikation und Umsetzung von rollenbasierten Sicherheitsrichtlinien
Final Report Abstract
Informationssysteme von Organisationen wie z.B. Unternehmen, Banken, Krankenhäusern und Behörden müssen bestimmte gesetzliche Regelungen wie z.B. Datenschutzgesetze oder Compliance-Anforderungen erfüllen. Solche organisatorischen Regeln lassen sich gut durch rollenbasierte Sicherheitsrichtlinien (RBAC policies) abbilden. Allerdings können diese Sicherheitsrichtlinieh gerade in größeren Organisationen schnell komplex werden. Mit der Komplexität ist die Gefahr von Sicherheitslücken in diesen Regelwerken gegeben, so dass die gesetzlichen Anforderungen möglicherweise verletzt werden. Aus diesem Grunde ist eine systematische Methodik wünschenswert, mit welcher die rollenbasierten Sicherheitsrichtlinien definiert, analysiert und anschließend umgesetzt werden können. Im Projekt ForRBAC sind daher verschiedene Methoden für die Spezifikation, Validierung und Umsetzung der rollenbasierten Sicherheitsrichtlinien untersucht worden. Mit Hilfe von UML (Unified Modeling Language) und OCL (Object Constraint Language) konnten statische rollenbasierte Sicherheitsrichtlinien spezifiziert und anschließend mit dem OCL-Werkzeug USE validiert und umgesetzt werden. Für dynamische rollenbasierte Sicherheitsrichtlinien, wie sie etwa in Workflows auftreten, wurde ein Validierungsverfahren auf der Grundlage eines Modellprüfers verwendet. Hierdurch kann geprüft werden, ob ein Ausführungspfad eines Workflows vorher festgelegten rollenbasierten Sicherheitsrichtlinien genügt. Um darüber hinaus fundamentale Sicherheitseigenschaften von rollenbasierten Sicherheitsrichtlinien formal beweisen zu können, wurde ein Ansatz auf Basis des Theorembeweisers Isabelle gewählt. Rollenbasierte Sicherheitsrichtlinien werden hier in einer linearen Temporallogik erster Stufe formuliert. Beweise von Sicherheitseigenschaften dieser Spezifikationen können dann mit Hilfe von Isabelle formal nachvollzogen werden.
Publications
- A model-checking approach to analysing organisational controls in a loan origination process. In Proceedings of the 11th ACM Symposium oh Access Control Models and Technologies, Lake Tahoe, CA, 2006
A. Schaad, V. Lotz, K. Sohr
- A workflow instance-based model-checking approach to analysing organisational controls in a loan origination process. 1st International Workshop on Secure Information Systems (SIS '06). Wisla, Polen, 2006
A. Schaad, K. Sohr
- A Workflow-based Model-checking Approach to Inter- and Intra-analysis of Organisational Controls in Service-oriented Business Processes, Journal of Information Assurance and Security, Volume 2, Issue 1, 2007
A. Schaad, K. Sohr, M. Drouineaud
- Analyzing and Managing Role-Based Access Control Policies., IEEE Transactions on Knowledge and Data Engineering, Vol. 20, No. 7, 2008
K. Sohr, M. Drouineaud, G.-J. Ahn, M. Gogolla
- Eriforcing Role-Based Access Control Policies in Web Services with UML and OCL, 24th Annual Computer Security Applications Conference, Anaheim CA, Dezember 2008
K. Sohr, T. Mustafa, G.-J. Ahn, X. Bao
- Implementing Advanced RBAC Administration Functionality with USE. 8th OCL Workshop at the UML/MoDELS Conferences, Toulouse, Oktober 2008
T. Mustafa, K. Sohr, D.-H. Dang, M. Drouineaud, S. Kowski
- Supporting Agile Development of Authorization Rules for SME Applications. 3rd Workshop on Trusted Collaboration (TrustCol-2008), Orlando, Florida, 2008
S. Bartsch, K.Sohr. C. Bormann
