Title: A holistic approach for access control policies: from formal specification to aspect-based enforcement

Authors: Slim Kallel, Anis Charfi, Mira Mezini, Mohamed Jmaiel, Andreas Sewe

Addresses: Software Technology Group, Darmstadt University of Technology, Hochschulstr. 10, 64289 Darmstadt, Germany. ' Software Technology Group, Darmstadt University of Technology, Hochschulstr. 10, 64289 Darmstadt, Germany. ' Software Technology Group, Darmstadt University of Technology, Hochschulstr. 10, 64289 Darmstadt, Germany. ' ReDCAD Laboratory, National School of Engineers of Sfax, University of Sfax, B.P. 1173, 3038 Sfax, Tunisia. ' Software Technology Group, Darmstadt University of Technology, Hochschulstr. 10, 64289 Darmstadt, Germany

Abstract: We present in this paper a novel approach to non-functional safety properties, combining formal methods and Aspect-Oriented Programming (AOP). The approach supports both the formal specification and the enforcement of such properties through runtime monitoring. We apply our approach for security policies and especially Role-Based Access Control (RBAC) policies including application-specific constraints such as separation of duties and delegation. For formal specification, we introduce TemporalZ, a formal language based on Z and temporal logic, which provides domain specific predicates for expressing RBAC policies. For the enforcement, we generate automatically modular enforcement code out of the formal specification using the aspect-oriented language ALPHA.

Keywords: information security; computer security; access control policies; formal specification; AOP; aspect-oriented programming; runtime monitoring; enforcement; code generation.

DOI: 10.1504/IJICS.2009.031044

International Journal of Information and Computer Security, 2009 Vol.3 No.3/4, pp.337 - 354

Published online: 18 Jan 2010 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article