A holistic approach for access control policies: from formal specification to aspect-based enforcement
Slim Kallel, Anis Charfi, Mira Mezini, Mohamed Jmaïel, Andreas Sewe · International Journal of Information and Computer Security · 2009
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.