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

Int. J. of Information and Computer Security, Vol. x, No. x, xxxx

A holistic approach for access control policies: From formal specification to aspect-based enforcement Slim Kallel*, Anis Charfi and Mira Mezini Software Technology Group, Darmstadt University of Technology Hochschulstr. 10, 64289 Darmstadt, Germany E-mail: {kallel,charfi,mezini}@st.informatik.tu-darmstadt.de E-mail: [email protected] *Corresponding author

Mohamed Jmaiel ReDCAD Laboratory, University of Sfax B.P. 1173, 3038 Sfax, Tunisia E-mail: [email protected]

Andreas Sewe Software Technology Group, Darmstadt University of Technology Hochschulstr. 10, 64289 Darmstadt, Germany E-mail: [email protected] Abstract: We present in this paper a novel approach to non-functional safety properties, combining formal methods and Aspect-Oriented Programming. 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 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: Access control policies, formal specification, aspectoriented programming, runtime monitoring, enforcement, code generation Reference to this paper should be made as follows: Kallel, S., Charfi, A., Mezini, M., Jmaiel, M., and Sewe, A. (xxxx) ‘A holistic approach for access control policies: From formal specification to aspect-based enforcement’, Int. J. of Information and Computer Security, Vol. x, No. x, pp.xxx–xxx. c 2009 Inderscience Enterprises Ltd. Copyright

1

2

S. Kallel et al. Biographical notes: Slim Kallel received his Master degree in Computer Science in 2005 and started in 2006 his PhD work at the National School of Engineers in Sfax (Tunisia) and Darmstadt University of Technology (Germany). This work focused on the specification and the enforcement of safety properties using formal methods and aspect-oriented programming. Since September 2009, he joined the Faculty of Economics and Management of Sfax as an assistant professor. Anis Charfi obtained his Diploma in Computer Science in 2003 from Technical University Munich and his PhD in 2007 from Darmstadt University of Technology with a dissertation on aspect-oriented workflow languages. After finishing his PhD he joined SAP Research Darmstadt where he is currently leading a research project in the area of service engineering. His current research areas include Software and Service Engineering as well as Model-Driven Software Development. Mira Mezini is full professor of computer science with the Faculty of Computer Science at Darmstadt University of Technology in Germany, where she leads the software technology group. A significant part of her research focuses on programming languages and tools with strong support for software modularity and variability. She has been actively involved in object-oriented and aspect-oriented software development communities. She is currently chairing AOSA (AspectOriented Software Association), is a member of AITO (Association Internationale pour les Technologies Objets) and of the editorial board of Transactions on Aspect-Oriented Software Development. Mira is author of about 80 articles in high quality journals and conference proceedings. Mohamed Jmaiel obtained his diploma of engineer in Computer Science from Kiel (Germany) University in 1992 and his Ph.D. from the Technical University of Berlin in 1996. He is now full Professor at the National School of Engineers of Sfax (Tunisia). His current research areas include software engineering of distributed systems, formal methods in model-driven architecture, component oriented development, self-adaptive and pervasive systems, autonomic middleware. He published about 100 regular papers in many international conferences and journals on these subjects. Andreas Sewe received a Diplom degree in mathematics from Darmstadt University of Technology in 2007 and thereafter became a Ph.D. candidate in computer science. His current research, conducted at the Center for Advanced Security Research Darmstadt (CASED), focuses on virtual machine support for runtime monitoring, policy enforcement, and aspect-oriented programming.

From formal specification to aspect-based enforcement

3

1 Introduction Non-functional safety properties of software applications include all properties which are not directly related to the functionality provided by the application. Yet specifying and enforcing these properties is important to ensure that bad things such as faults, deadlocks, etc. do not happen. Unfortunately, application designers and developers often focus on the functionality only and do not directly address non-functional properties including safety ones. Providing capabilities for the specification of various types of non-functional properties early in the development process and their automated enforcement are major challenges for software systems. However, the state-of-the-art in addressing the specification and runtime enforcement of non-functional properties have several limitations. First, often not all steps in the process of implementing non-functional safety properties are covered; these properties are not specified in the early phases of software development but rather added later, which negatively affects the application code’s quality. Second, several approaches use informal or semi-formal languages such as UML as well as different extensions to it for specifying non-functional properties. Such specifications have three problems. The specification cannot be verified formally. Further, the OCL language which is often used with UML for specification has a limited expressiveness and cannot be used to specify complex properties. Finally, the specification language may not cover all aspects of non-functional properties, for instance UML lacks means to express temporal non-functional properties. Third, the code implementing non-functional properties is mostly written in and integrated manually with the functional application code. As a result, there is no guarantee that the code implementing these properties conforms to the formal specification. In addition, errors and contradictions may be introduced by the programmer when mapping a specification to code although these errors do not exist in the formal specification. Fourth, the code responsible for enforcing properties, be it manually written or generated from specifications, is not encapsulated in separate modules; it is scattered across the application modules and tangled with the functional application code. This lack of modularity leads to maintainability problems in the case of manually written enforcement code; each change of a non-functional property requires the programmer to find all places in the implementation related to that property and update them accordingly. These observations have motivated our work on the Seven-pro approach to specifying and enforcing non-functional safety properties. It is based on three principal steps: In the first step the non-functional safety properties are specified using appropriate formal languages. In the second step, these formal specifications are verified. This step may also verify general properties using theorem proving or model checking tools. In the third and final step the specified non-functional properties are enforced by modular aspect code that is generated automatically from their formal specification. Seven-pro covers both structural and behavioral non-functional properties. Hereby, we mean by structural properties those properties related to the structure and architecture of a component-based application. In this context, we proposed in (Kallel et al., 2007) the specification and enforcement of architectural invariants.

4

S. Kallel et al.

We used in that work a combination of Z notation and Petri nets to formally specify the architectural properties and style, the dynamic reconfiguration of software architecture, and the coordination protocol describing the execution order of the reconfiguration operations. In the second step of our approach, we used the Z/EVES theorem proving tool to formally verify the specification’s consistency. In the third step, this specification of the architectural invariants was translated automatically to AspectJ code. Under behavioral properties we understand properties related to the behavior of the application, e.g., temporal constraints on certain operations of the application, or constraints on permitted operation sequences. We distinguish two kinds of behavioral properties: qualitative and quantitative properties. As an example of quantitative properties, we applied the Seven-pro approach to temporal properties for Web service composition in (Kallel et al.(b), 2009). For the specification of these properties, we introduced XTUS-Automata, a formal specification language combining timed automata with the XTUS language, which allows to formally specify absolute and relative time properties. Further, we defined specification patterns that facilitate the specification of complex temporal properties and allow an automated translation to aspect code in AO4BPEL. These aspects can be integrated with BPEL processes at runtime and enforce the respective properties. In this paper, we apply the Seven-pro approach to qualitative properties. We address the specification and enforcement of security policies that are enforceable by runtime monitoring as characterized by (Schneider, 2000). More specifically, we propose an “end-to-end” approach to runtime verification of access control policies. Our approach consists of three building blocks. The formal specification end of the solution is covered by a new formal specification language called TemporalZ, which was introduced in (Regayeg et al., 2006). On the the runtime enforcement end of the solution, we propose to encode the enforcement logic as aspects in the Alpha language (Ostermann et al., 2005). The third important building block that makes our approach “end-to-end” is the automated mapping of formal specifications to aspect-based enforcement code. The remainder of the paper is organized as follows: Sec. 2 presents a running example and briefly introduces RBAC, SoD, and delegation policies, as well as TemporalZ and Alpha. Sec. 3.1 explains the use of TemporalZ for the formal specification of the aforementioned policies. Sec. 3.2 presents the formal verification and conflicts resolution. Sec. 3.3 explains the automatic mapping from formal specifications to Alpha aspects. Sec. 4 reports on related work while Sec. 5 concludes the paper and presents areas of future work.

2 Prerequisites In this section, we first introduce a simple loan approval process (LAP) in a bank that will be used throughout this paper for illustration. Then, we briefly introduce RBAC including delegation and separation of duty (SoD) policies. Thereafter, we introduce the formal language TemporalZ and the aspect-oriented programming language Alpha.

From formal specification to aspect-based enforcement

5

2.1 Loan Approval Process Case Study Initial application: Together with the customer a teller identifies an appropriate loan program and then verifies the application data. Rating process: Two types of rating are performed: An internal rating performed by a financial clerk who verifies that the customer situation fits into the loan program being applied for. An external rating performed by a teller involves an external agency to check whether the customer has financial problems with other companies. Finally, a supervisor verifies both ratings to reduce the risk of errors and frauds. Bank decision: Based on both ratings, a supervisor takes a decision on the application. If it is approved, he gives the order to create the contract; otherwise, the process is canceled. Sign contract: After the loan has been approved, a contract is sent to the manager and to the customer for signature. Loan closing: The teller who entered the application data transfers the money to the customer’s account. To avoid errors, a supervisor verifies this step.

2.2 RBAC, Delegation and Separation of Duties Role-Based Access Control (Ferraiolo et al., 2007) is an authorization mechanism in which access decisions are based on the users’ roles in their organization. The permissions to execute a set of operations are grouped in roles and users are assigned to one or more roles. For example, the security administrator of the banking software may define the following roles for LAP: Teller , FinancialClerk , Supervisor , Manager , and Customer . Delegation is a further extension to RBAC which allows users to assign some or all of their permissions to others. Most delegation models are characterized by the totality property, which leads to two delegation types: permission delegation and role delegation. In the first type, the delegator delegates a part of his individual access permissions. In the second type, the delegator delegates his role, which allows the delegatee to assume this role. Additionally, the delegation types user-touser and user-to-role can be distinguished. In user-to-user delegation the delegator can delegate his rights at the same time to a set of users, whereas in user-torole delegation the delegator delegates his rights to a role. The monotonicity characteristic refers to whether roles/permissions are kept after delegation or not. Two types of delegation exist: grant delegation and transfer delegation. During grant delegation, the delegator maintains the permissions that he delegated after the delegation step. During transfer delegation, however, the delegator looses the delegated permissions after the delegation step. The level of delegation defines whether the delegated role/permission can be further delegated. Hereby, singlestep delegation means that the delegated right cannot be delegated multiple times, which is allowed by multi-step delegation. Separation of duty policies reduce the risk of frauds and errors in business processes by a fine-grained control over the privileges for workflow tasks. Two main categories are distinguished: static and dynamic separation of duties (Gligor et al., 1998).

6

S. Kallel et al.

Static SoD (SSoD): This class of separation of duty policies specifies that two mutually exclusive roles must never be assigned to the same user simultaneously, e.g., a bank employee cannot, at the same time, be assigned the roles Supervisor and Manager. Dynamic SoD (DSoD): This class of policies take the dynamics of the system execution into account for managing roles and role membership. Four variations of dynamic SoD are distinguished in the literature: Simple Dynamic SoD (SDSoD): two mutually exclusive roles must never be simultaneously activated by a user, e.g., a bank employee can be statically assigned both roles Teller and FinacialClerk, but cannot activate them at the same time. Object-Based SoD (ObjDSoD): a user can simultaneously activate two exclusive roles, but he cannot act upon the same object via both roles. Such a constraint can, e.g., prevent in LAP that a user who can be both Supervisor and Teller would then be able to execute the operations of the role Teller and verify his own work using the Supervisor role. Operational SoD (OpDSoD): a user can activate two exclusive roles at the same time, but cannot have all required authorizations to execute all tasks in a workflow process. In LAP, e.g., the critical sub-processes (e.g., enterApplicationData, verifyRating, verifyTransfer ) cannot be executed by the same employee. Operational Object-Based SoD (OpObjDSoD): a user can activate two exclusive roles at the same time and can have the authorizations to execute all tasks in a workflow process, as long as these do not act upon the same object. (Combines ObjDSoD and OpDSoD.)

2.3 Formal Language TemporalZ TemporalZ (Regayeg et al., 2006) is a formal language that integrates linear temporal logic with the Z framework and that we use for specifying models for RBAC as well as for delegation and separation of duties. We now formally define the syntax and semantics of TemporalZ. First, we define the syntax of the temporal formulas, which combine temporal operators with the security predicates required to specify temporal constraints. A TemporalZ formula is either a domain specific predicate, or composed of other formulas by the temporal operators. The semantics of these formulas are defined by evaluation with respect to a temporal model, specified as an abbreviation function from a time point t to the set of specific predicates that hold at t. We define three axiomatic functions, which allow the evaluation of the temporal formulas at different abstraction levels. EvalMT interprets each formula in the model m at a given time point t. EvalMT evaluates domain-specific predicates without temporal operators to True (E1), if the predicate holds at time point t according to m. For composite formulas a variant of EvalMT is defined for each temporal operator; for brevity, only the evaluation of formulas composed with eventually 3 (E2) is shown below. Then, we generalize our evaluation by abstracting over the time parameter and obtain a new function EvalM that evaluates temporal formulas according to the model (E3). After that, we define a second generalization by abstracting over the model and obtain the evaluation function Eval (E4). Finally, we define equivalences between each

From formal specification to aspect-based enforcement

7

temporal operator and its evaluation definition as shown below for the temporal operators Eventually (E5) and Until (E6). Model == Time → F Formula

Time == x : N

EvalMT : P(Formula × Model × Time) ∀ a : SecurityPredicate;m : Model;t : Time • EvalMT (a, m, t) ⇔ a ∈ m(t)

[E1]

∀ f : Formula; m : Model; t : Time

3(f )), m, t) ⇔ (∃ t1 : Time •| t1 ≥ t • EvalMT (f , m, t1)

• EvalMT ((

[E2]

... EvalM : P(Formula × Model) ∀ f : Formula; m : Model • EvalM (f , m) ⇔ (∀ t : Time • EvalMT (f , m, t))

[E3]

Eval : P Formula ∀ f : Formula • Eval(f ) ⇔ (∀ m : Model • EvalM (f , m))

3f ) = True ⇔ 3f

[E4]

∀ f : Formula • Eval(

[E5]

∀ f , g : Formula • Eval(U (f , g)) = True ⇔ f U g

[E6]

...

2.4 Aspect-Oriented Programming and Alpha Aspect-oriented programming (AOP) (Kiczales et al., 1997) facilitates the modularization of crosscutting concerns, whose implementation cannot cannot be localized in a specific module by conventional techniques, but rather is scattered over several modules and tangled with the code implementing other concerns. The enforcement of security policies is an example of such concerns. The aspect-oriented programming language Alpha belongs to the family of AO languages that use logic queries (a subset of Prolog) as pointcuts to reason about actions in the program execution. In addition to its powerful pointcuts, Alpha has a rich joinpoint model, encompassing the static program structure, the complete history of the execution, and the object store at each moment in execution. The availability of the execution trace is one of the features that distinguishes Alpha from other AO languages. The execution trace can be thought of as a list containing representations of all joinpoints that occurred in the execution of the program so far. In Alpha, this list structure is only implicit; instead, all joinpoint representations carry a time stamp which corresponds to their position in that list. There are different types of joinpoints corresponding to different types of execution events of an object-oriented program, such as method calls, or field accesses. For each type of joinpoint, there is a relation which has a time stamp as its first argument, the joinpoint specific information as further arguments. Method calls, e.g., are stored in the database as pairs of calls/51 and endCall/3 facts denoting the beginning resp. the end of a method call. For example, calls(ID, ExpID, Receiver, Method, Arg) describes a method call execution action that occurred at time stamp ID, the method Method is called on

8

S. Kallel et al.

the receiver Receiver with Arg as the input argument; ExpID identifies the lexical position of the expression that caused the action. The unary relation now/1 has – at every point in the execution – only one fact in the database that contains the current time stamp as its argument. The relation before/2: T → T holds if the first time stamp corresponds to an execution action that occurred before the one corresponding to the second time stamp.

3 SEVEN-PRO for Access Control Policies To support the design and implementation of secure software applications, we applied the Seven-pro approach to access control policies. The instantiation of the approach in this context gave rise to a three-steps approach for the development of secure applications. First, the security designer specifies formally the RBAC model and the different policies and constraints on top of it using TemporalZ. Then, he verifies the consistency of the formal specification by using the tool Z-EVES for theorem proving. After that, the application developer implements the functional code of the application using Java. Thereby, the functional code does not contain any logic for authorization, i.e., if the application implements a certain workflow process then any user will be able to execute any task in the workflow. Once the application logic is implemented and the security policies are specified, the developer can use our aspect generator, which generates the security module of the application by translating the authorization policies formally specified in TemporalZ to separate Alpha aspects. During execution of the application these aspects will be triggered at appropriate points and the respective advice will enforce the RBAC constraints.

3.1 Formal Specification & Verification 3.1.1 TemporalZ for access control policies In order to employ TemporalZ for the formal specification of RBAC models and stateful access control such as the separation of duty and delegation policies, we extend the language’s syntax and semantics (cf. Section 2.3) with domain-specific security predicates. The syntax definition of these predicates is shown in Fig. 1 below whereas their semantics definition is shown in Fig. 2.

SDPredicate ::= includehhUSER × ROLE ii | activehhUSER × ROLE ii | execOphhUSER × ROLE × OPERATION ii | execOpObj hhUSER × ROLE × OPERATION × OBJECT ii | execSeqOphhUSER × seq OPERATION ii | execSeqOpObj hhUSER × seq OPERATION × OBJECT ii

Figure 1: Syntax of Security Predicates

From formal specification to aspect-based enforcement

9

E7: ∀ m : Model; t : Time • ∀ u : USER; r : ROLE • EvalMT ((include(u, r )), m, t) ⇔ E8:

(∃ system : RBAC • u ∈ system.users ∧ r ∈ system.roles ∧ u ∈ system.RoleUser (| {r } |)) ∀ m : Model; t : Time • ∀ u : USER; r : ROLE • ∃ s : SESSION • EvalMT ((active(u, r )), m, t) ⇔ (∀ system : RBAC • EvalMT ((include(u, r )), m, t)

E9:

∧ s ∈ system.sessions ∧ s ∈ system.UserSession(| {u} |) ∧ s ∈ system.RoleSession(| {r } |)) ∀ m : Model; t : Time • ∀ u : USER; r : ROLE ; op : OPERATION • EvalMT ((execOp(u, r , op)), m, t) ⇔ (∀ system : RBAC • EvalMT ((active(u, r )), m, t)

E10:

∧ op ∈ system.operations ∧ op ∈ system.RoleOperation(| {r } |)) ∀ m : Model; t : Time • ∀ u : USER; r : ROLE ; op : OPERATION ; obj : OBJECT • EvalMT ((execOpObj (u, r , op, obj )), m, t) ⇔ (∀ system : RBAC • EvalMT ((execOp(u, r , op)), m, t)

E11:

∧ obj ∈ system.objects ∧ obj ∈ system.OperationObject(| {op} |)) ∀ m : Model; t : Time • ∀ u : USER; Sop : seq • EvalMT ((execSeqOp(u, Sop)), m, t) ⇔ (∀ i : N | 1 ≤ i ≤ #Sop • (∃ r : ROLE • EvalMT ((

3(execOp(u, r , (Sop(i))))), m, t)))

∧ (∀ i : N | 1 < i ≤ #Sop • ((∃ r 1 : ROLE • EvalMT ((execOp(u, r 1, (Sop(i)))), m, t)) E12:

3

⇒ (∃ r 2 : ROLE • EvalMT ((− (execOp(u, r 2, (Sop(i − 1))))), m, t)))) ∀ m : Model; t : Time • ∀ u : USER; Sop : seq OPERATION ; obj : OBJECT • EvalMT ((execSeqOpObj (u, Sop, obj )), m, t) ⇔ (∀ i : N | 1 ≤ i ≤ #Sop

3(execOpObj (u, r , (Sop(i)), obj ))), m, t)))

• (∃ r : ROLE • EvalMT ((

∧ (∀ i : N | 1 < i ≤ #Sop • ((∃ r 1 : ROLE • EvalMT ((execOpObj (u, r 1, (Sop(i)), obj )), m, t))

3

⇒ (∃ r 2 : ROLE • EvalMT ((− (execOpObj (u, r 2, (Sop(i − 1)), obj ))), m, t))))

Figure 2: Semantics of Security Predicates The predicate include(u,r) (Fig. 2, E7) tells whether u is one of the users assigned to the role r, whereas the predicate active(u,r) (Fig. 2, E8), tells that u has actuallly activated the role r, i.e., the user should be already in the role r and should have connected to that role within a session s. The predicate execOp(u,op) (Fig. 2, E9) tells whether the user u has already executed the operation op by verifying whether u has activated a role that includes op. The predicate execOpObj (Fig. 2, E10) refines execOp by checking whether u has already executed op with obj as parameter. Finally, the predicates execSeqOp and execSeqOpObj (Fig. 2, E11 and E12), introduce the concept of an ordered operation sequence. Hereby, execSeqOp(u,sop) tells whether the user u executes the sequence of operations sop in the order defined by the sequence. The predicate execSeqOpObj(u,sop,obj) refines execSeqOp(u,sop) by constraining all operations to the same object obj.

3.1.2 Specification of the RBAC model The specification of the RBAC system in TemporalZ is shown in the Z Schema RBAC in Fig. 3. The upper part defines sets of roles, operations, and objects, as well as relations between them. Each role has a set of operations associated with it, defined by RoleOperation [D1]. A user should have the role, as defined by the relation RoleUser [D2], to be allowed to execute the operations of that role. A session is a mapping of a user to a subset of his roles as defined by ([D3], [D4], [C2], and [C3]). The relation OperationObject [D5] maps operations to objects

10

S. Kallel et al.

they operate on. The lower part of Fig. 3 defines constraints on the ranges and domains of the relations defined in the upper part [C1],[C2] and RBAC constraints ([C3]). Further, constraints on RBAC concepts and their relationships are specified in terms of first-order predicates. The designer can also specify constraints that depend on the application, e.g., by restricting the number of the roles and users in the application. In addition, the designer can specify the administrative operations using Z operation schema. E.g., assignUserToRole corresponds to the operation that assigns a new user to a role.

RBAC roles : F ROLE ; users : F USER; sessions : P SESSION operations : F OPERATION ; objects : F OBJECT RoleOperation : ROLE ↔ OPERATION

[D1]

RoleUser : ROLE ↔ USER

[D2]

RoleSession : ROLE ↔ SESSION

[D3]

UserSession : USER ↔ SESSION

[D4]

OperationObject : OPERATION ↔ OBJECT

[D5]

dom RoleOperation ⊆ roles

[C1]

ran RoleOperation ⊆ operations

[C2]

∀ u1, u2 : users | u1 6= u2 • ∃ s : sessions

[C3]

• (u1, s) 6∈ UserSession ∨ (u2, s) 6∈ UserSession

Figure 3: RBAC Model

3.1.3 Specification of SoD Properties In the following, we present examples of formal specification of SoD for LAP using TemporalZ. Using the predicate include (Fig. 2, E7), the specification StaticSoD states that an employee in LAP cannot be a Manager and a Supervisor at the same time. StaticSoD RBAC ExclusiveRole(Supervisor , Manager ) ⇔ ∀ u : USER • ¬ include(u, Supervisor ) ∨ ¬ include(u, Manager )

The specification DynamicSoD uses the predicate active (Fig. 2, E8) to state that an employee can be a Teller and a FinancialClerk, but not simultaneously. DynamicSoD RBAC ∀ u : USER •

2(¬ (active(u, teller ) ∧ active(u, financialClerk )))

Using the predicates execOp and execOpObj (Fig. 2, E9 and E10), the specification ObjectBasedSoD states that a user who has executed

From formal specification to aspect-based enforcement

11

checkInternalRating in the FinancialClerk role can never in the future execute verifyRating in the Supervisor role for the same customer cst. ObjectBasedSoD RBAC ∀ u : USER; cst : Customer •

2((execOpObj (u, financialClerk , checkInternalRating, cst)) ⇒ (¬ (3(execOpObj (u, supervisor , verifyRating, cst)))))

The specification OperationalSoD uses execSeqOp (Fig. 2, E11) to prohibit an employee from executing the critical sequence (enterApplicationData, verifyRating, verifyTransfer ). The specification OperationalObjectBasedSoD uses execSeqOpObj (Fig. 2, E12) to disallow executing the operations of the rating subprocess (checkInternalRating, checkExternalRating, verifyRating) on the same customer application ctr. OperationalSoD

OperationalObjectBasedSoD

RBAC

RBAC

SeqOp : seq OPERATION

SqOO : seq OPERATION

∀ u : USER

∀ u : USER; ctr : Customer

| SeqOp = henterApplicationData,

| SqOO = hcheckInternalRating,

verifyRating, verifyTransfer i

checkExternalRating, verifyRatingi

•

2(¬ (execSeqOp(u, SeqOp)))

•

2(¬ (execSeqOpObj (u, SqOO, ctr )))

3.1.4 Specification of delegation policies Several delegation models have been proposed on top of RBAC so that a user can assign all or a part of his permissions to other users. In the rest of the paper, we call the user who performs the delegation task “delegator”, and the user who receives the access right “delegatee”. Our delegation approach is composed of two parts. In the first one, we extend the RBAC model by the delegation concepts. We specify the different types and characteristics of delegation using Z schema. In the second part, we define the delegation operations which correspond to the actions executed by the delegator at runtime. Our approach supports user-to-user (U2U) and user-to-role (U2R) delegation combined with permission (PD) and role delegation (RD). Our approach supports also monotonicity and delegation levels. We specify a Z schema RBACDelegation which contains the four types of delegation. In the declaration part, we specify the relations which connect the delegator, the delegated permission/role, and delegating user/role. In the predicative part, we specify the constraints that should be satisfied during the delegation operation. We specify the delegation operations which correspond to the actions executed by the delegator at runtime. The designer should specify each delegation operation by means of a Z operation schema and define pre- and post-conditions. The preconditions are constituted by the constraints defined in the operation schema and the constraints related to the operations which are defined in the delegation

12

S. Kallel et al. RBACDelegation RBAC U 2R4PD : USER × ROLE × OPERATION ↔ ROLE TransferPD : USER ↔ OPERATION MultiStepPD : USER ↔ OPERATION GrantPD : USER ↔ OPERATION SingleStepPD : USER ↔ OPERATION ... ∀ u1 : users; r 1 : roles; op1 : operations; r 2 : roles | (r 2, op1) 6∈ RoleOperation ∧ (r 2, u1) 6∈ RoleUser • ((u1, r 1, op1), r 2) ∈ U 2R4PD ...

Figure 4: Permission Delegation Schema schema. Delegation operations are executed only if their preconditions are satisfied. The post-conditions are the conditions which should be satisfied after executing the delegation operation. The designer should first update the delegation system by defining the new state of the delegation relation. Second, the designer should choose the type of delegation by updating the relations dealing with the delegation characteristics monotonicity and delegation level.

U 2R PD ∆RBACDelegation u1? : USER; op1? : OPERATION ; r 1? : ROLE ; r 2? : ROLE (r 1?, r 2?) ∈ ExclusiveRole

[PreC1]

(r 1?, op1?) ∈ RoleOperation

[PreC2]

∨ ((u1?, op1?) ∈ MultiStepPD

[PreC3]

∨ (∀ r : roles | (r , op1?) ∈ RoleOperation • (u1?, r ) ∈ MultiStepRD)

[PreC4]

((u1?, op1?) 6∈ TransferPD

[PreC5]

∨ (u1?, r 1?) 6∈ TransferRD)

[PreC6]

U 2R4PD 0 = U 2R4PD ∪ {((u1?, r 1?, op1?), r 2?)}

[PostC1]

GrantPD 0 = GrantPD 0 ∪ {(u1?, op1?)}

[PostC2]

Figure 5: Delegation Operation Schema We present in Fig. 5 the operation schema U 2R PD, which specifies the operation user to role for permission delegation. The defined preconditions verify whether the delegator is allowed to delegate the corresponding permissions. First, we verify that the role containing the delegator and the delegating role are defined as exclusive roles in a static separation of duties property (cf. Sec. 3.1.3) [PreC1]. Second, we verify that the user (delegator) is the owner of the delegated permissions [PreC2], or he already received, in a multi-step manner,

From formal specification to aspect-based enforcement

13

the corresponding permission or any whole role containing that permission [PreC3, PreC4]. We verify also that the delegator does not delegate, in a transfer manner, the corresponding permission and any whole role containing that permission [PreC5, PreC6]. For the post-conditions [PostC1, PostC2], the designer updates the system state and specifies that the current operation is transferred in a grant manner.

3.2 Ensuring Consistency and Conflict Resolution To ensure consistency, we verify that the specification of the basic RBAC and its constraints does not contain any contradiction by proving with Z-EVES an initialization theorem, which states the existance of a state SystemInit of the RBAC system and RBAC extension for delegation that fulfills all constraints. We also verify the preservation of the consistency of the RBAC delegation system after a delegation operation using pre-condition theorem. One may still argue that SoD constraints can introduce other inconsistencies. However, as we use a prohibitionbased approach (Ahn, 2003) (defined by the axioms ¬ ϕ and ϕ ⇒ ¬ ψ . . . ), SoD constraints, which are safety properties, cannot introduce any inconsistencies into the already consistent RBAC system. If a SoD constraint evaluates to True, the user is prohibited from executing the respective operation. The specification of the separation of duty properties on top of the RBAC can conflict with a model allowing for the delegation of authority through role and permission transfer (Schaad, 2001). As a simple example, assume that the users u1, u2 already hold respectively the role manager and supervisor . We specify SSoD between these two roles. The delegation of the role or part of the role of the user u1 to the user u2 would result in a conflict with the SoD property. Our solution is based on stating that separation of duties properties always have precedence over other properties (Schaad, 2001). There are two types of conflicts that should be detected and resolved: The first is related to the static separation of duties (as the example presented above). We propose to verify before each delegation operation that the role of the delegator and the delegated role are not defined as mutually exclusive roles; this gives rise to a pre-condition defined in the delegation operation Z schema. For dynamic separation of duties, we present as an example the simple dynamic SOD. Suppose that we define a simple dynamic SoD constraint between the role r 1 and r 2. At runtime a user u1 delegates his role r 1 to the user u2 that belongs to the role r 2. A conflict is detected, the user u2 can execute the operation of the role r 1 and r 2 in the same time. In the enforcement of simple dynamic SOD, we identify the operations executed by u2 which are delegated by u1. For that, we add a new definition of the query verifyRoleAccess defined in Alpha library to consider the delegated operation.

3.3 Aspect-based Security Monitors In this section, we present the mapping from formally specified security policies to enforcement aspects. First, we present the mapping of TemporalZ predicates into domain-specific Alpha predicates used in the pointcuts of enforcement aspects. Then, we outline the generation schema of aspects that enforce SoD and delegation

14

S. Kallel et al.

policies. We developed a prototype implementation that incorporates the presented mapping and generates enforcement aspects from the formal specification and deploys them into the Alpha runtime.

3.3.1 Mapping TemporalZ Predicates to Domain Specific Alpha Predicates A library of domain specific Prolog predicates has been defined in Alpha to ease the mapping of formal specifications to enforcement aspects; it includes one predicate for each temporal operator as well as several RBAC- and SoD-specific predicates. For example, the temporal operator 3 − is mapped to the Prolog predicate before/2. Similarily, the operator 3 is mapped to the Prolog predicate eventually/2 which verifies that the first time stamp corresponds to an action after the action corresponding to the second time stamp. There is also a mapping of the logical conjunctives, e.g., the formal conjunction operation (∧) is mapped to the and operator (,) of Prolog. Any universally quantified (∀) parameter in the formal specification is translated to a Prolog variable.

3.3.2 Aspects for Object-Based SoD Property For each formally specified SoD property, an Alpha aspect is generated. This aspect uses an around advice to stop the execution if the property does not hold. Due to space-constraints only the enforcement of object-based SoD is presented. The enforcement schema of the others SoD properties can be found in (Kallel et al.(a), 2009) The specifications of ObjSoD properties use the formal predicate execOpObj (u, r , op, obj ). In Sec. 3.1.3, this predicate is used twice in ObjectBasedSoD (with concrete bindings of op to checkInternalRating, resp. verifyRating and of r to financialClerk, resp. supervisor ). The evaluation of execOpObj (u, r , op, obj ) to true (E10 in Sec. 3.1.1) requires that execOp(u, r , op) evaluates to true for any obj in the set of objects on which op operates (obj ∈ OperationObject(op)); The predicate execOp(u, r , op), in turn, is true if active(u, r ) is true and op is one of the operations assigned to r (E9 in Sec. 3.1.1). Following this reduction of the evaluation of execOpObj to active, the two uses of execOpObj in ObjectBasedSoD are mapped to the conjunction of Alpha predicates shown, e.g., in lines 4–5 and 7–8 of List. 1. The condition obj ∈ OperationObject(op) used in execOpObj is mapped to having the calls predicates in the pointcut explicitly relate op and obj . 1 2

class ObjDynamicSoD { void around

3

calls(T1,_,_,checkInternalRating,Customer), callingUser(T1,User), verifyRoleAccess(User,financialClerk,checkInternalRating),

4 5 6

now(T2), calls(T2,_,_,verifyRating,Customer), callingUser(T2,User), verifyRoleAccess(User,supervisor,verifyRating),

7 8 9

%checkInternalRating is called before verifyRating eventually(T2,T1). { System.out.print("Violation of a ObjDSoD property");

10 11 12

}

13 14

}

Listing 1: Aspect for ObjDSoD

From formal specification to aspect-based enforcement

15

This listing shows the aspect generated for the ObjectBasedSoD property specified in Sec. 3.1.3: a user who has executed checkInternalRating as a FinancialClerk thereafter cannot execute verifyRating for the same customer as a Supervisor. The pointcut is triggered whenever a user in a supervisor role is about to verify the rating (at the present time T2) and the same user has checked the internal rating of the same Customer as a financial clerk at T1 in the past (eventually(T2,T1)); in this case, the advice signals a violation and truncates the execution (no proceed ). Note that concrete operation names are used in List. 1 to reflect the fact that execOpObj in ObjectBasedSoD refers to concrete operations. Also, in addition to the User variable, the Customer variable is used in the calls predicate in List. 1 to express that the property should hold for any customer object.

3.3.3 Aspects for delegation policy There is one aspect for each delegation operation which enforces the corresponding pre-conditions and delegation constraints. Listing 2 shows the overall structure of such an aspect. The Alpha predicate calls constitutes the pointcut (line 2) used to intercept calls in the functional code which corresponds to the formally specified delegation operation. The advice (lines 2–15) associated with the pointcut has the type around, i.e., it is executed instead of the intercepted method calls. (Kallel et al., 2008). In the advice body, each Z constraint is translated to a conditional. In order to easily translate the Z constraints to Java conditions, we have implemented a Z-based Java library. It contains the implementation of the most used Z operators and mathematical objects as Java methods. Two types of conditions are generated depending on the Z constraints: Simple conditions, generated from formal constraints without quantification, are checked by calling the corresponding method in the Java Z library zOperatorMethod (line 5), which takes the system state as parameter. Helper methods, denotated by the constraint i, are generated for each formal constraint that uses a quantification operator (lines 6 and 16). 1 2

class DelegationOperation { void around calls (N, _, _, delegateOperation,obj){

3

//Evaluate pre-condition (operation schema) and constraints (delegation schema) if (zOperatorMethod(parameters, systemState)){ ... } if (constraint_i()) { ... }

4 5 6 7

//Evaluate all defined conditions if (allConstraints) { //Execute of the delegation Operation proceed(); updateSystemState(); } else{ ... }

8 9 10 11 12 13 14

} public boolean constraint_i() { ... } public void updateSystemState() { ... }

15 16 17 18

}

Listing 2: Template of aspect generation If all generated conditions are fulfilled (line 9), the intercepted operation will be executed using the keyword proceed (line 11). Otherwise, the aspect prohibits the

16

S. Kallel et al.

execution of the operation (line 14). In addition, the generated aspect comprises a method (line 17) to update the system state according to the specification of the post-conditions. If the generated preconditions are fulfilled this method is called after the proceed (line 12).

4 Related Work In this section, we discuss the most related work on the enforcement of the security policies and especially on RBAC, separation of duties and delegation policies. Work such as (Basin et al., 2006) addresses the translation of access control properties to enforcement code using a UML-based security modeling language and transformation functions that map such models to particular technologies for access control in application platforms, such as J2EE. At the specification level, temporal constraints (including SoD) are not supported because of OCL limitations. At the implementation level, the code generated is not modular and also incomplete (only code skeletons). In (Colcombet and Fradet, 2000), an approach to enforce trace properties by program transformation is presented. A transformation takes the original program and the properties which will be enforced in input and generates an equivalent program that enforces the specified properties. That approach is based on graphs and automaton transformation. It is related to our work because the properties that should be enforced are specified formally and declaratively. However, the generated programs are not modular since the code enforcing the formal properties is mixed with the functional code. In (Kim et al., 1999), the authors propose a monitoring and checking framework to monitor the execution of a real-time system. At runtime, the system checks events for compliance with a formal specification, from which appropriate enforcement components are generated. Compared to our approach, this framework is similar as it uses a formal specification language and generates runtime monitoring code. However, the formal language used in (Kim et al., 1999) is not suitable for specifying security policies and for verifying the consistency of the specification using theorem proving. In addition, the generated enforcement code is not modular. Erlingsson (2004) proposes an approach for enforcing security policies based on transforming JVML code. Unlike our approach, formal specification and verification of security policies as well as the modularity of the generated enforcement code are not in focus in (Erlingsson, 2004). Stolz and Bodden (2006) propose a runtime verification tool based on LTL and the AO language AspectJ, which uses LTL expressions over joinpoints for specifying the properties to verify at runtime. The lack of a rich joinpoint model and the restricted expressiveness of AspectJ’s pointcut language lead to complex aspects, since logic for simulating the automata corresponding to LTL formulas has to be encoded. Like Alpha this work provides expressive pointcut languages, albeit they have not been employed to enforce security policies so far. In (Verhanneman et al., 2005) aspect-oriented techniques are used to model and enforce access control policies. This work supports only simple access control constraints defined in either Ponder or XACML; SoD properties and

From formal specification to aspect-based enforcement

17

administrative operations are unsupported. In addition, compared to Alpha, the aspect languages used are based on less powerful pointcut languages, resulting in less modular aspects when enforcing temporal constraints. Few works have been done on enforcing delegation policies with AOP. In (Chen, 2005), the author extends his access control framework for Strutsbased Web applications to include delegation of access rights; the aspect language AspectWerkz is used to enforce delegation policies. Compared to our approach, the automatic generation of delegation aspects from formal specification allows the user to easily specify the delegation model and its characteristics and bridge the gap between specification and implementation. In addition, our approach supports different types and characteristic of delegation that are not considered in (Chen, 2005), such as user-to-role delegation.

5 Conclusion In this paper, we applied our Seven-pro approach to non-functional safety properties for security policies in general and access control policies in particular. Our approach covers the formal specification and enforcement of RBAC policies and their constraints, including SoD and delegation policies. Hereby, the use of TemporalZ allows for reliable and high-level specifications and the use of aspects, facilitated by the automatic translation of the TemporalZ specifications into Alpha code, makes the policy enforcement code well-modularized and separated from the application business logic. As future work, we will investigate the extension of our approach to support edit automata (Ligatti et al., 2005). In addition, we intend to cover other policies of access control such as Chinese Wall. Moreover, we will improve the performance of our implementation.

Acknowledgements This work was supported by CASED (www.cased.de).

References Ahn, G.-J. (2003) ‘Specification and classification of role-based authorization policies’, In Proceedings of the 12th International Workshop on Enabling Technologies (WETICE 2003), Linz, Austria, pp. 202, IEEE Computer Society. Basin, D., Doser, J. , and Lodderstedt T. (2006) ‘Model driven security: from UML models to access control infrastructures’, ACM Transactions on Software Engineering and Methodology, Vol. 15, No. 1, pp.39–91. Chen, K. (2005) ‘Using dynamic aspects for delegating fine-grained access rights’, In Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), Taipei , Taiwan, pp.783–789, IEEE Computer Society. Colcombet, T. and Fradet, P. (2000) ‘Enforcing trace properties by program transformation’, : In Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL 2000), pp.54–66, ACM.

18

S. Kallel et al.

Erlingsson, U. (2004) The Inlined Reference Monitor Approach to Security Policy Enforcement, Ph.D. thesis, Cornell University. Ferraiolo, D., Kuhn, R. and Sandhu, R. (2007) ‘RBAC Standard Rationale: Comments on “A Critique of the ANSI Standard on Role-Based Access Control”’, IEEE Security and Privacy, Vol. 5, No. 6, pp.51–53. Gligor, V. D., Gavrila S. I. , and Ferraiolo, D. (1998) ‘On the formal definition of separation-of-duty policies and their composition’, In Proceedings of IEEE Symposium on Research in Security and Privacy, Oakland, California, IEEE Computer Society. Kallel, S., Charfi, A., Mezini, M., and Jmaiel, M.(2007) ‘Combining formal methods and aspects for specifying and enforcing architectural invariants’, In Proceedings of the 9th International Conference on Coordination Models and Languages (Coordination 2007), Paphos, Cyprus, pp.211–230, Vol. 4467 of LNCS, Springer. Kallel, S., Charfi, A., Mezini, M., and Jmaiel, M. (2008) ‘Aspect-based enforcement of formal delegation policies’, In Proceedings of the 3th International Conference on Risks and Security of Internet and Systems (CRiSIS 2008), Tozeur, Tunisia, pp.9–19, IEEE. Kallel, S., Charfi, A., Dinkelaker, T., Mezini, M., and Jmaiel, M. (b) (2009) ‘Specifying and monitoring temporal properties in web services compositions’, In Proccedings of the 7th IEEE European Conference on Web Services (ECOWS 2009), to appear, Eindhoven, The Netherland, IEEE Computer Society. Kallel, S., Charfi, A., Mezini, M., Jmaiel, M. and Klose, K. (a) (2009). ‘From formal access control policies to runtime enforcement aspects’, In Proceedings of the 1st International Symposium on Engineering Secure Software and Systems (ESSoS 2009), Leuven, Belgium, pp.16–31, Vol. 5429 of LNCS, Springer. Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C. V., Loingtier,J.-M., and Irwin, J. (1997) ‘Aspect-Oriented Programming’, In Proceedings of the 11th European Conference on Object-Oriented Programming, Finland, pp.220–242., Vol. 1241 of LNCS, Springer. Kim, M., Viswanathan, M., Ben-Abdallah, H., Kannan, S., Lee, I. and Sokolskyz, O. (1999) ‘Formally specified monitoring of temporal properties’, In Proceedings of the 11th Euromicro Conference on Real-Time Systems (ECRTS 1999), York, England, pp.114-122, IEEE. Ligatti, J., Bauer, L., and Walker, D., (2005) ‘Enforcing non-safety security policies with program monitors’, In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS 2005), pp.355–373, Vol. 3679 of LNCS, Springer. Ostermann, K., Mezini, M., and Bockisch, C., (2005) ‘Expressive pointcuts for increased modularity’, In Proceedings of the 19th European Conference on Object-Oriented Programming, Glasgow, UK, pp.214–240, Volume 3586 of LNCS, Springer. Regayeg, A., Kallel, S. Hadj-Kacem, A., and Jmaiel, M. (2006) ‘ForMAAD Method: an experimental design for air traffic control’, International Transactions on Systems Science and Applications, Vol. 1, No. 4, pp.327–334. Schaad, A. (2001) ‘Detecting conflicts in a role-based delegation model’, In Proceedings of the 17th Annual Computer Security Applications Conference (ACSAC 2001), New Orleans, Louisiana, pp.117, IEEE Computer Society. Schneider, F. B. (2000) ‘Enforceable security policies’, ACM Transactions on Information and System Security, Vol. 3, No. 1, pp.30–50. Stolz, V. and Bodden E. (2006) ‘Temporal assertions using AspectJ’, Electronic Notes in Theoretical Computer Science, Vol. 144 , No. 4, pp.109–124.

From formal specification to aspect-based enforcement

19

Verhanneman, T., Piessens, F., De Win, B., Truyen, E., and Joosen W. (2005) ‘Implementing a modular access control service to support application-specific policies in CaesarJ’, In Proceedings of the 1st workshop on Aspect oriented middleware development (AOMD 2005), Grenoble, France, ACM.