A holistic approach for access control policies: from formal specification to aspect-based enforcement. (19th January 2010) - Kallel, Slim; Charfi, Anis; Mezini, Mira; Jmaiel, Mohamed; , Andreas Sewe
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.