TU Darmstadt / ULB / TUbiblio

Aspect-based Enforcement of Formal Delegation Policies

Kallel, Slim and Charfi, Anis and Mezini, Mira and Jmaiel, Mohamed (2008):
Aspect-based Enforcement of Formal Delegation Policies.
IEEE, In: Third International Conference on Risks and Security of Internet and Systems (CRiSIS '08), Tozeur, Tunisia, 28.-30. Okt. 2008, [Conference or Workshop Item]

Abstract

Delegation is a powerful concept in access control systems, which allows users to assign all or part of their permissions to other users. Several types of delegation models for role-based access control have been proposed so far. However, most existing works focus on the specification of delegation policies and there is very little work on the monitoring and enforcement of such policies at runtime. In this paper, we use a security approach combining formal methods and aspect-oriented programming for specifying and enforcing delegation policies. In our approach, delegation models and their characteristics are specified formally using TemporalZ, which is a combination of Z notation and temporal logic. Then, we verify the formal specification to ensure consistency using theorem proving. Finally, we generate automatically a set of aspects in the aspect-oriented language ALPHA from the TemporalZ specifications. These aspects enforce the specified delegation policies at runtime.

Item Type: Conference or Workshop Item
Erschienen: 2008
Creators: Kallel, Slim and Charfi, Anis and Mezini, Mira and Jmaiel, Mohamed
Title: Aspect-based Enforcement of Formal Delegation Policies
Language: English
Abstract:

Delegation is a powerful concept in access control systems, which allows users to assign all or part of their permissions to other users. Several types of delegation models for role-based access control have been proposed so far. However, most existing works focus on the specification of delegation policies and there is very little work on the monitoring and enforcement of such policies at runtime. In this paper, we use a security approach combining formal methods and aspect-oriented programming for specifying and enforcing delegation policies. In our approach, delegation models and their characteristics are specified formally using TemporalZ, which is a combination of Z notation and temporal logic. Then, we verify the formal specification to ensure consistency using theorem proving. Finally, we generate automatically a set of aspects in the aspect-oriented language ALPHA from the TemporalZ specifications. These aspects enforce the specified delegation policies at runtime.

Publisher: IEEE
Divisions: 20 Department of Computer Science > Software Technology
20 Department of Computer Science
Event Title: Third International Conference on Risks and Security of Internet and Systems (CRiSIS '08)
Event Location: Tozeur, Tunisia
Event Dates: 28.-30. Okt. 2008
Date Deposited: 14 Sep 2009 07:15
Identification Number: doi:10.1109/CRISIS.2008.4757459
Export:

Optionen (nur für Redakteure)

View Item View Item