A holistic approach for access control policies: from formal specification to aspect-based enforcement. (19th January 2010)

• Record Type: Journal Article
• Authors: Kallel, Slim; Charfi, Anis; Mezini, Mira; Jmaiel, Mohamed; , Andreas Sewe
• Is Part Of: International journal of information and computer security. Volume 3:Number 3/4(2009)
• Page Start: 337
• Page End: 354
• Publication Date: 2010-01-19
• Subjects: information security -- computer security -- access control policies -- formal specification -- AOP -- aspect-oriented programming -- runtime monitoring -- enforcement -- code generation; Computer security -- Periodicals; Information systems management -- Security measures -- Periodicals; Computer networks -- Security measures -- Periodicals; Information technology -- Security measures -- Periodicals; 005.805
• Languages: English
• ISSNs: 1744-1765

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.