Pierre Konopacki

Marc Frappier
email: marc.frappier@usherbrooke.ca

Régine Laleau
email: laleau@univ-paris12.frpierre.konopacki

Expressing access control policies with an event-based approach

Keywords: Access Control, Formal Security Methods, Security Models

In this paper, we introduce EB 3 SEC. This language is used to express access control policies in information systems. Permissions and prohibitions are expressed with a class diagram. EB 3 SEC also includes a process algebra. This process algebra allows one to express specific constraints over permissions and prohibitions. Organizational constraints such as obligation and separation of duty are also supported by process algebra. Separation of duty constraints can be expressed at a workflow process level. Standards such as RBAC or OrBAC can be used to express the access control policy, but their derivatives can also be used. EB 3 SEC provide a formal language with a high level of expressiveness to describe access control policies.

Introduction

Information Systems (IS) are widely used in various economical and social areas. They contain private and valuable data for their owners. In an IS security is enforced by many mechanisms, such as secured protocols used between clients and servers or between servers in a distributed architecture. The most used architecture to develop IS is the Service Oriented Architecture (SOA). Many mechanisms have also been developed to secure different components of an IS build with this architecture, or to secure communication between those components [START_REF] Gutiérrez | Towards a process for web services security[END_REF]. All those tools deserve one purpose : to enforce an access control (AC) policy. The AC policy is the part of the security policy that deals with authorizations granted to users. An AC policy badly defined can lead to major issues for the company that uses the IS : as an example we can cite banks that lost billiards since a trader used more authorization that he should have been granted.

Security is an important goal for IS designers. In IS, data integrity is insured by an access control (AC) policy which is implemented in the software and enforced by mechanisms like encryption, secure data transfer protocols and authentication protocols. Furthermore, in some domains, IS security is regulated by laws. As an example, in the financial domain, we can cite the Sarbane-Oxley law in the United-States [START_REF] Sarbanes | Sarbanes-oxley act[END_REF] and the Mer law in France [START_REF] Mer | loi de sécurité financière[END_REF]. In health care area, we can cite the PIPEDA law in Canada [START_REF] Government | Personal information protection and electronic documents act[END_REF]. These laws aim to protect information by regulating their access. Organisations have to prove that the AC policy used by their IS comply with these laws. In this paper we propose a new formal method which aims to model AC policies.

Our project is conducted with an industrial partner from the banking industry in Canada. The management of security policies in an industrial context is a highly complex task. Security policies are informally described using plain English and adhoc diagrams, and then they are implemented into concrete programs, in various components. Generally, the AC policy is implemented directly in the individual services, mixed with the business logic of the IS. The traceability between the natural language specification and the implementation code is hard to maintain. Thus, modifying and validating an AC policy is a hard task. A small change in AC policy may easily take up to a month of effort for implementation. With the current turmoil about security in the industry, security policies are bound to be frequently changed, which induces high maintenance costs for organisations.

Our goal is to streamline the management of AC policies. In this paper, we define EB 3 SEC: a simple, abstract, formal specification language to describe AC policies. To describe the use of EB 3 SEC we give some example of how common AC constraints can be expressed in EB 3 SEC. The idea is to develop security filter based on EB 3 SEC modeling. The first step to achieve this this goal is to show a prototype of tool using EB 3 SEC. We choose to present an interpretor that uses an EB 3 SEC specification to grant or refuse incoming events.

The paper is structured as follows. Section 2 explains the problem addressed by EB 3 SEC. Section 3 presents the EB 3 SEC language and the constraints that can be expressed in an EB 3 SEC model. The expressiveness of the language is illustrated with an example presented in 3.1. After a discussing about choices during the modeling in 4, we present a possible implementation of an EB 3 SEC interpretor in 5. In 6, we present future works related to EB 3 SEC, before comparing EB 3 SEC to other similar tools in 7.

PROBLEM DEFINITION -PROBDEF

We aim to create a language to model AC policies. A lot of methods with the same purpose already exist. These methods have a state based approach [START_REF] El Kalam | Organization based access control[END_REF]. In other words, expressing an AC constraint only implies the current state of the system. Other methods, which are not state based, focuses on a particular kind of constraint [START_REF] Liu | An access control model for web services in business process[END_REF][START_REF] Emin | An access control language for web services[END_REF]. Case studies depicting AC policies used by our industrial partners imply business processes and constraints over actions ordering. Due to the variety of constraints that can be found in the case studies, the language we have to create must have a high level of expressiveness.

In order to ease the modeling of these case studies, we propose a different approach based on events accepted by the system, but with keeping a formal aspect. To do so, we want to express an AC policy, by describing constraints it involves on events accepted by the system.

MODELING ACCESS CONTROL POLICIES -MODACCCONT-POL

In this section we present some notations and assumptions used in EB 3 SEC. The denotational semantics of an EB 3 SEC specification is given by a relation R defined on T (main) × O, where T (main)

denotes the traces accepted by main and O is the set of output events. The operational behaviour of main is defined as follows. Let trace denote the system trace, which is a list comprised of valid input events accepted so far in the execution of the system. Let t::σ denote the right append of an input event σ to trace t, and let [ ] denote the empty trace. We assume that to execute an action in the system, a user must be logged in. Thus, for each events, we know the person trying to execute it, the role this person played, the place and the time it happened. We introduce the notion of security events, which are n-tuples. The last element of the n-tuple is the event itself, the other elements contains values of some parameters. For this paper, we choose to use 5-tuples :

σ = p, r, o,t, evt
. The definition of the 5-tuple is given by : p, r, o,t, evt with: p ∈ personId and r ∈ roleId and o ∈ orgId and t ∈ Timestamp and label(evt) ∈ action In this definition U ser.name() is the set containing all values available for users during the login step ; by the same way we describe Role.name(), Branch.name() and Action.label() which respectively contain all the values of roles, organizations and actions. In our definition, we consider that the time is represented by an integer which means the timestamp of the moment the action is performed. As evt is an event we use the function label which return the name of the action instantiated. evt, the last part of a security event, is an instantiation of (the input parameters of) an action. The signature of an action a is given by a declaration a(q 1 : T 1 , . . . , q n : T n ) : (q n+1 : T n+1 , . . . , q m : T m ) where q 1 , . . . , q n are input parameters of types T 1 , . . . , T n and q n+1 , . . . , q m are output parameters of types T n+1 , . . . , T m . A security event p, r, o,t, a(t 1 , ...,t n ) also constitutes an elementary process expression. The special symbol " " may be used as an actual parameter of an action, to denote an arbitrary value of the corresponding type.

Complex EB 3 SEC process expressions can be constructed from elementary process expressions (instantiated actions) using the following operators: sequence ( ), choice (|), Kleene closure ( * ), interleaving ( ), parallel composition ( , i.e., CSP's synchronisation on shared actions), guard ( =⇒ ), process call, and quantification of choice (| x ∈ T : . . .) and interleaving ( X ∈ T : . . .). The EB 3 SEC notation is similar to CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] but the main differences between EB 3 SEC and CSP are: i) EB 3 SEC allows one to use a single state variable, the system trace, in predicates of guard statements (as we shall see below); ii) EB 3 SEC uses a single operator, concatenation (as in regular expressions), instead of prefixing and sequential composition, which makes specifications easier to read and write.

In the following we use this process algebra to express AC policies. We give now the kind of constraints that can be expressed in an AC policy modeled in EB 3 SEC. Those constraints will be more precisely described in the following of the document.

Permission allows the execution of an action.

Prohibition forbids the execution of an action.

Obligation forces the user to execute an action after an event

Separation of duty are used to forbid an execution of an action for a user after an event. Now, we discuss about each of these kinds of constraints, after introducing a running example to illustrate our discussion.

THE RUNNING EXAMPLE : THE CHECK DEPOSIT -RUNEX

Our industrial partner provides us some case studies to work on. These case studies deal with check deposit in a bank branch. Thus, as in [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF] and [START_REF] Sandhu | Transaction control expressions for separation of duty[END_REF] we illustrate our work on check deposit example.

We consider here the following process of the check deposit : Assuming that the client already has an account in the company, he brings a check to the branch where he is affiliated. A bank employee makes the check deposit effective in the IS. Thus, this deposit could be canceled, or validate, in the second case, the account of the client has to to be credited.

The main difference with [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF] and [START_REF] Sandhu | Transaction control expressions for separation of duty[END_REF] was to consider an access control policy over different bank branches. As an example, permissions given to users are different from each other depending on where the branch is located. Considering a procedure of check deposit, generally it has to be validated by a supervisor, the number of required validations depends on the amount of the check deposit, and this value fluctuates depending on the state where the procedure takes place. In order to be more precise and understandable we stipulate in the following access control rules taking place in the example. rule 4 : The validation or the cancellation of a deposit can not be done by the same person that did the check deposit.

rule 5 : If the value of a check deposit exceed an amount, the check deposit must be validated by two different persons including the chief agency. In Quebec this amount equals 10 000 $ whereas in Ontario this amount equals 8 000 $.

rule 6 : The modification of the bank account of the customer must be done by the same employee that did the check deposit effective.

In this example, we use four different actions which are deposit, cancel, validate credit. Those actions have three arguments which refer to the customer, the number of the check and the value of the check deposit. In our model, we use integer for the value of the check, this assumption could be easily understand, as a value of a check has only two digits after the coma. In this example, people can play four different roles : customer, clerk, banker and chie f agency. We also assume that we have at least two bank branches one in Montreal, QC and the other in Toronto, ON.

PERMISSION

When giving a permission, we want to allow someone to do something, but we want the security environment to comply with a specific pattern. Thus, dealing with permission, means to establish pattern for the security environment for each event. By pattern, we mean that in order to be executed, an event must have a security environment that respect some specific value.

The EB 3 SEC language allows the modeler to express the AC policy he wishes. This policy can comply with an existing AC model as RBAC which is an ANSI standard [START_REF]ANSI) for Information Technology. Role Based Access Control[END_REF]. The modeler can also use a hand made model. To model the running example, we use the second method. In fact, the example centralizes in a unique model AC policies of different branches. However, AC policy used in each branch is quietly similar to the others, it slightly differ. To achieve this task we add to the RBAC standard, the notion of organization which was first created in the OrBAC model [?]. Generally by organization, people think of AC constraints involved in SoD problems. In the OrBAC model, it deals with the location. As an example, it could be used to model different branches of the system. In order to be more readable, we use the term Branch in our model in place of organization. In comparison to the RBAC standard, this notion of branch/organization avoid us to multiply the number of instances of actions and role. For example if we did not used this concept we had to create two different roles for customer : one for each branch.

In order to express permissions, we have the 5-tuple, but we need to introduce four more operators.

• The Kleene closure written * is used to iterate a process expression an arbitrary number of time.

• The choice which is denoted by | and expresses that one of two process expressions can be executed.

• The quantified choice is a variant of the previous operator. When a process expression depends on the value a free variable, we can use a quantified choice to express the fact we can execute this process expression for a specific value of the free variable. We note it : | x ∈ ens : a ( x ), and it means that a ( x ) is executed with a specific value of x taken in the set ens.

• The wildcard is a syntax shortcut used instead of a quantified choice. As an example, a( )

means | x ∈ ens : a ( x )
In our work, we consider that security events are not necessarily correct : in fact we have in our modeling to verify that the user can for example play the role in the bank branch, both given by the security environment. Now, we introduce a process expression permissionA and explain it.

permissionA ( ) ( agatha, banker, , , deposit( , ) | boris, , , , cancel( , ) | chris, clerk,toronto, , credit( , ) ) *
This process expression, contains a Kleene closure over a choice of three actions. Thus, each event received must be compatible with one of this three action. The first action agatha, banker, , , deposit( , ) describes that if the event is an instance of deposit, thus the role mentioned in the security environment must be banker and the user must be agatha. This pattern of permission, is the same as those used in RBAC : permission to execute an action are given to a user playing a role. The second action boris, , , , cancel( , ) describes that if the event is an instance of cancel, thus the person mentioned in the security environment must be boris. This pattern of permission is the same as those used in Bell et LaPadula [START_REF] Bell | Secure computer systems: Mathematical foundations and model[END_REF] : permission are given to users. The third action chris, clerk,toronto, , credit( , ) describes that if the event is an instance of credit, thus the user, the role and the organization mentioned in the security environment must be respectively chris, clerk and toronto. This pattern of permission is the same as those used in OrBAC : permissions are given to a user playing a role in a bank branch. This PE shows the different ways that can be used in an EB 3 SEC modeling to express permission, as a matter of fact it does not depict our running example. Now, we give a new process expression called permissionB, that is a first PE that depict our running example. Going through the six rules of our running example, we only keep in mind the three first rules. In fact, those three rules are the only rules dealing with permissions. The three rules does not depend on the branch, but only on roles played by users during the action. The first rule states that each clerk and each banker must be allowed to perform the action deposit( . ) The second rule states that each banker and chief agency must be allowed to perform actions validate( a )nd cancel( . ) The third rule states that each banker and clerk are allowed to perform the action credit( . In a sake of concision, we only instantiate one permission for each couple of role and action. As a fact, we assume that there is more than one user of each role, so we have to add the substantial number of lines for each user of the system.

)
In case studies provided by our industrial partner, we must keep in mind that the IS is used by a great number of users. Thus, it becomes quickly tedious to express permissions for each user in a process expression. In order to ease this task, EB 3 SEC provides a class diagram. As a fact, for each security event received we have to check if it complies with at least one permission described in the modeling. PE are not designed for this kind of task, as they are no ordering constraints over actions. Thus the class diagram is used to defined class and relation useful to express permissions. So, for each security event received we have to check if it complies with permissions expressed in the class diagram.

In the following, we describe the kind of permissions we used in our example, and thus how we check the complying of security events with permissions described in the class diagram.

To describe the permission pattern used in our approach, we have have to keep in mind that they have to be easily used with case studies provided by our industrial partner. A first approach would have been to use a standard as RBAC [START_REF]ANSI) for Information Technology. Role Based Access Control[END_REF] and used it. A first problem occurs, when we noticed that the AC policy derived from the case studies has to deal with a geographic context : for example the validation procedure of a check deposit differs from branches to branches if they are not grounded in the same state. Furthermore, in other part of the case studies permissions granted to a role are different if the role is played in branches of different states. To ease the modeling of permission we used another AC model : OrBAC [?]. This model, includes the notion of organization in the pattern used to describe permissions. This pattern will be explained in the following. In a sake of readability, we used the name of each instance as a key. We keep in mind that this method allows the example to be more readable. The class Branch is instanced for each branch of the running example : Montreal and Toronto. The class Action is instantiated for each action aimed by the AC policy : deposit, cancel, validate and credit. The class Role is instantiated for each role that can be played in the IS : customer, clerk, banker and chief agency. The relation Play is instantiated to express role given to each role in a branch for an action. In our example, permissions are the same in both branch. But in case studies supplied by our partner, permissions differ from branches to branches. The class User is instantiated for each user of the system. The relation Play is instanced in order to expressed roles played users in branches. Now, for each event received, we want to check if the security environment corresponds to the class diagram. To do so, we use a static predicate which is a first order logic predicate. And we have to check if this predicate holds for each event received.

sp(p, r, o,t, e) = p, r, o ∈ Play ∧ r, o, e ∈ Permission

Permissions can be expressed by two ways : by using a class diagram or a process expression. Our experience shows that the class diagram is generally used to express permissions that fit well with the AC model express in the class diagram. Thus, process expression are used for permissions that are slightly exotic. For example, let suppose we have a superuser called damien that can execute the action cancel in both branches. As, we do not have any exotic rule in our example, we use the class diagram and the process expression used for permission, is empty :

permission ( ) ( λ ) *
Now, we use the same approach to show how EB 3 SEC can be used to express prohibitions.

PROHIBITION -PROHI

When setting a prohibition, we want to express security environments that are not allowed to execute an action. To do so, we use the same approach as previously performed for permissions : we use a process expression, to describe the pattern of security environment prohibited for each action. In order to achieve, we must introduce a new operator. This PE does not models our running example, it is only used to illustrate the concept of prohibition and the way they are modeled in EB 3 SEC. In this process we use guards to avoid explicit values for some parameters of the security environment. In the first part, the prohibitions avoid the person called elisa to execute the action cancel in all possible cases. In the second part we avoid the action validate to be performed in Toronto.

Previously we have used the concept of permission to model the three first rules of our running example. In the following we use the concept of prohibition to make this modeling. As a fact for each role we have to express a prohibition for each action and role that are not explicitly written in the example. As for permission we first begin with a PE.

| , r, , , credit( , ) | | r ∈ Role.name() : r = clerk =⇒ , r, , , cancel( , ) | , r, , , validate( , ) | | r ∈ Role.name() : r = chie f agency =⇒ , r, , , deposit( , ) | , r, , , credit( , ) ) *
Still considering the fact that we are dealing with IS and a larger number of user, we choose to express prohibition with the class diagram (ref). As a fact we assume that a prohibition is defined for a role to execute an action in a branch. Here we finish to instantiate the class diagram by giving the instance of the class Prohibition.

Our goal is to enforce this prohibition expressed by a class diagram. To do so, we slightly change the static predicate in order to care about the relation Prohibition.

sp(p, r, o,t, e) = p, r, o ∈ Play ∧ r, o, e ∈ Permission ∧ r, o, e ∈ Prohibition

Then the process expression corresponding to prohibition is transformed in the empty PE. In the system, we want that both permissions and prohibitions are applied simultaneously. Thus, we use a specific process expression called main that represents the global behaviour of the AC policy.

A FIRST VERSION OF THE MAIN PROCESS EXPRESSION -MAIN1

In the main expression, we want that all aspects (i.e.:permissions, prohibitions . . . ) are applied simultaneously to all event received by the IS. In the following we will introduce a first version of the main process expression. This version will allows permissions and prohibitions to be checked for each received event. To do so, we introduce a new operator.

• The parallel operator depicted as a b allows one to execute two actions without specifying the order in which they have to be executed.

main ( ) permission ( ) prohibition ( )

In other words, we can say that the process expression permission and prohibition have to be executed, but they must synchronise on actions they have in common. We give there a few examples of events which are accepted or not, and the reason it is so.

• adrian, banker, Montreal, deposit( zoe, 124 ) is not accepted : In fact, adrian is not allowed to be a banker in Montreal

• boris, banker, Montreal, deposit( zoe, 24 ) is allowed : In fact it refers only to permission and not to prohibition, as it complies with permissions modeled, the security event is accepted.

• adrian, clerk, Montreal, deposit( yves, 123 ) is allowed : In fact, it appears in Permission and prohibition and complies with both of them.

When an event is globally refused by main, the state of both process expression permission and prohibition does not change.

OBLIGATION

In AC policy, the notion of obligation is an organizational constraint that apply to user. As an example, we can express an obligation for a user to execute an action of acknowledgement after performing an action. Typically, it is the kind of constraint expressed in the sixth rule. Sometimes, the obligation takes effect between the user who performed the first action, and a member of a group which contains the first user for the performing of the second action.

In EB 3 SEC, an obligation explains that two security events of the trace are linked together by the value of the requester of the security event. To express an obligation we use process expressions (PE) containing these operators in addition to operators previously explained.

• The sequence denoted by a b allows one to execute the process expression b after the execution of the process expression b

• The interleaving denoted by a b allows process expressions a and b to be executed in parallel without any synchronisation, even if they have common actions.

• The quantified interleaving is denoted by p ∈ ens : exp ( p ). It corresponds to the interleaving of process expressions exp ( p ) for all values of p contained in the set ens.

In our running example the sixth rule is an example of obligation. We introduce a new process expression that model this rule.

obligation ( ) c ∈ U ser.name() : d ∈ int : m ∈ int : | p ∈ U ser.name() : ( p, , , , deposit( c, d, m ) p, , , , credit( c, d, m ) ) *
This PE models the sixth rules. In fact, as argument are explicitly written in deposit and credit, in the trace of the system, these actions are executed for particular value of a customer, a check number and an amount of a check. Now we suppose that the security event adrian, clerk, Montreal, deposit( zoe, 1, 23 ) is already executed. Thus, a security event corresponding to the event credit( zoe, 1, 23 ) can not be performed unless the requester is adrian.

Our PE only express that the two actions have to be done by the same user. But as a fact the system can not physically force the user to perform the second action after executing the first one. A way to enforce the obligation is to forbid any action for the user after he executed the first one. We show another PE modeling obligation this way.

obligationP ( ) c ∈ U ser.name() : d ∈ int : m ∈ int : | p ∈ U ser.name() : ( p, , , , deposit( c, d, m ) ( p, , , , credit( c, d, m ) | FALSE =⇒ p, , , , , deposit( , , ) | FALSE =⇒ p, , , , , cancel( , , ) | FALSE =⇒ p, , , , , validate( , , ) ) *
In this PE, after performing the action deposit, the user have the choice between four actions. Three of this four actions are blocked by a guard that will never hold. Thus, the user can perform only the action deposit for the check deposit he performed. As it is not mentioned that other action are disabled during the obligation we use the first PE for our modeling.

A REFINEMENT OF THE MAIN PROCESS EXPRESSION

As we have described new constraints on our system, we have to integrate them in the main process expression that describes the global AC policy behaviour.

We put the process expression obligation in parallel with permission and prohibition. main ( ) permissions ( ) prohibition ( ) obligation ( )

SEPARATION OF DUTY

SoD (Separation of duty) is a security requirement that divide a task in subtasks and rely the execution of these subtasks to different users [START_REF] Ferraiolo | Role-Based Access Control[END_REF]. Thus, the security of the process has less chances to be corrupted by a single user who could execute all the subtasks by himself.

In RBAC, the problem of SoD is generally statically resolved : the permission of executing subtasks are given to different roles, and users are not allowed to play conflicting roles. We can use these approach in EB 3 SEC by checking the instance of the class diagram.

Another approach used to solve SoD is called dynamic SoD. For two actions, with SoD constraints, dynamic SoD forbid the user to execute the second action, once the first action is executed. To achieve dynamic SoD, the method used must keep an instance of tasks already performed. In, EB 3 SEC, instances of workflows and their executions are saved by the PE. This will be shown in the following.

Fourth and fifth rules deal with SoD constraints. We give in the following a PE modeling these constraints and then we explain them.

separation ( ) c ∈ U ser.name() : d ∈ int : m ∈ int : | p ∈ U ser.name() : | p ′ ∈ U ser.name() : ( p, , , , deposit( c, d, m ) p = p ′ =⇒ p ′ , , , , validate( c, d, m ) | p ′ , , , , cancel( c, d, m ) ) * c ∈ U ser.name() : d ∈ int : m ∈ int : | p ∈ U ser.name() : | o ∈ Branch.name() : | p ′ ∈ U ser.name() : ( p, , o, , deposit( c, d, m ) m > o.limit =⇒ p = p ′ ∧ p = p ′′ ∧ p ′ = p ′′ =⇒ p ′ , , , , validate( c, d, m ) p ′′ , chie f agency, , , validate( c, d, m ) | m ≤ o.limit =⇒ λ ) *
In the first part of this PE, we expressed the fourth rule. We used a quantification over p and p ′ in order to achieve that the executer of deposit and validate or cancel must be different. Furthermore, we made a quantification over c, d and m to explicitly describe our workflow process. In fact, since the argument are explicitly written, the user who did the deposit for a check can still validate or cancel another check.

The second part of the PE models the fifth rule. For checks that value exceed the branch limit we must make two validate. Other wise the λ reminds that there is no special procedure to execute and only the fourth rule applies. The constraint used in this example for the check value is modeled in the PE by the expression m > o.limit used in a guard. Furthermore, we still explicitly write the arguments of the actions in order to model workflows. Thus, the user who make a deposit can still make a cancel or a validate for another check.

In EB 3 SEC, SoD constraints are defined at a workflow process level. As an example, for a user making the deposit of a check can still do other deposit but won't be able to make the validate or the cancel for the check for which he made the deposit. We illustrate this on the first part of the SoD : separationP. This PE shows that, by now, the user adrian can not execute validate, neither cancel for the check deposit 1. But the user adrian can still do other check deposit and cancel or validate other check deposit.

separationP

A NEW REFINEMENT OF THE MAIN PROCESS EXPRESSION

As SoD is a component of our AC policy we want to incorporate it the main process expression. We achieve this by using a parallel with the older version of main main ( ) permissions ( )

prohibition ( ) obligation ( ) separation ( )

DISCUSSION OF OUR MODELING

The first point we want to discuss about is the equivalence of using a PE or the class diagram to describe permissions and prohibitions. Prohibitions and permissions have to be checked for each security event received. Using PE or a static predicate with the class diagram are totally equivalent on a formal point of view. But, our experience shows that using the class diagram make the modeling more readable for human. On an implementation point of view, our goal is to use an interpretor to execute PEs with an access to a database in order to keep an updated version of the instance of the class diagram. As we aim to secure IS involving large number of users, we think that using static predicates could be a way to optimize the execution of the interpreter. But PEs can still be used. In this paper we described how to use permissions and prohibition. But we never force someone to use both in the same model. As permissions and prohibitions that can be found in requirements can be tedious to understand, we think that using both permissions and prohibitions can lead to deadlock.

The concept of branch used in our class diagram is very powerful on case studies provided by our partner. In the permission and prohibition it was not very useful, but it helped a lot when we had to model constraints over SoD.

The way we used to model the example, was directed by the fact we wanted to show how someone can model permissions, prohibitions, obligations and SoD in EB 3 SEC. We also use another approach that consists to product a PE for each rule of the requirement.

Using PEs in EB 3 SEC allows one to product a AC model that contains SoD and obligations rules, that are really accurate. As an example, we were able to express SoD rules with constraints and taking into account workflow processes. The EB 3 SEC language uses the same process algebra than the EB 3 method, with adding the notion of security environment. EB 3 is implemented in a platform called APIS that allow its interpretation.

IMPLEMENTATION

Components of this platform can be reused to create a Policy Decision Point (PDP), which can be used in an SOA architecture. Figure 4 illustrates the architecture of the PDP. It is based on the APISplatform and reuses some of its components. EB 3 PAI [START_REF] Fraikin | Efficient symbolic execution of large quantifications in a process algebra[END_REF][START_REF] Fraikin | Efficient symbolic computation of process expressions[END_REF] is an interpreter for EB 3 process expressions. It can be used to run EB 3 SEC process expressions by translating security actions into normal actions. Process expressions can contain predicates referring to attributes of the requirements class diagram and the security class diagram. We suppose that each class diagram is implemented in its own relational database. To implement the security class diagram, we use EB 3 TG [START_REF] Gervais | Generating relational database transactions from EB 3 attribute definitions[END_REF] to generate a relational database schema and update programs to implement attribute definitions. Update programs are used by EB 3 PAI to maintain the database in a consistent state while security events are executed. The module EB 3 GG [START_REF] Konopacki | Synthèse automatique de guarde EB3[END_REF] is used to generate a guard evaluator program which contains procedures that are used by EB 3 PAI to determine if a guard holds. It generates SQL requests on the database to obtain attribute values of entities. These procedures can refer to security database and the IS database.

If an event is refused by EB 3 PAI, the error message generator [START_REF] Milhau | Automatic Generation of Error Messages for the Symbolic Execution of EB 3 Process Expressions[END_REF] is used to generate an adapted error message. EB 3 PAI can execute arbitrary process expressions and uses an object-oriented database (OODB) to persistently store the state of process expressions. It can efficiently execute quantified expressions over arbitrary large sets (both choice and interleave) by using optimization techniques [START_REF] Fraikin | Efficient symbolic execution of large quantifications in a process algebra[END_REF][START_REF] Fraikin | Efficient symbolic computation of process expressions[END_REF]. Its main weaknesses are that its OODB is rather slow and its execution cannot be easily distributed over several processors. For high throughput banking applications, this is not sufficient. Hence, we are currently working on a new process algebra interpreter which will be restricted to deterministic and optimizable process expressions. These process expressions can be translated into an algebraic state transition diagram (ASTD) [START_REF] Frappier | Extending statecharts with process algebra operators[END_REF]. The execution of an ASTD is easier to distribute over several processors, thereby exploiting parallelism in the processing of events. The state of an ASTD is more compact than the one used in EB 3 PAI and can be easily stored into a relational database. The use of ASTDs will also enable the use of state-based techniques like B and Event-B to prove properties about a security policy.

FUTURE WORK

The next step in our work will be to include the capabilities of making model checking over EB 3 SEC models. As EB 3 SEC is very similar to EB 3 we plan to reuse results and tools developed for EB 3 . As a result, Alloy will surely be the tools we will use. The first step will be to transform EB 3 SEC models into Alloy model. The first step will be to define how to transform the static part of an EB 3 SEC model (i.e. : class digram, permissions and prohibitions) into an alloy model. At this step we will be able to verify the consistency between permissions rules and prohibition rules. After, we will need to transform the dynamic part (i.e. : obligation, SoD and more generally all PEs) in an Alloy model. Thus, we will be able to verify that dynamic and static parts are coherent.

Furthermore, if the functional part of the IS is also formally modeled we will be able to check the coherence between the functionnal and the security parts.

The implementation previously presented is also a fuure work. In order to integrate tools of the APIS platform for EB 3 SEC we plan to develop a prototype made in OCaml and SQL. In the project lead with our industrial partner, we plan to implement a platform based on EB 3 SEC and usable in a real life platform. This platform has to be integrated in an SOA architecture.

RELATED WORK

In order to compare related work, we use the approach describe in [START_REF] Alm | A classification framework designed for advanced role-based access control models and mechanisms[END_REF]. This approach describes a framework that allows one to express characteristics of AC model. This approach leads to thirty different comparison points encompassed in eight categories. As we present here only the EB 3 SEC language and not the full EB 3 SEC project led with our industrial partner, we only mention a few comparison points and categories. We apply this approach to our work and then to other related work:

• In [START_REF] Basin | Model driven security: From uml models to access control infrastructures[END_REF], the authors show a method aiming to solve AC problems by including a RBAC model in the UML design design of the application

• In [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF], the authors show a method helping to create a language to express SoD express in CSP with an RBAC model in order to be used with an enforcement point

• [START_REF] Moses | eXtensible Access Control Markup Langage (XACML) Version 2.0[END_REF] proposes a non formal language to express AC policies. In fact the problem is that contradictory decision can be taken for a request by the same policy. Several works as [START_REF] Kolovski | Analyzing web access control policies[END_REF] presents a formalisation of policies expressed in XACML in order to avoid the problem. [START_REF] Anderson | XACML Profile for Role Based Access Control (RBAC)[END_REF] presents a profile made in XACML of the RBAC model including mechanisms to use SoD. In the following, we consider this set of works as a unique work called XACML considered as formal and able to express SoD. Here, the SoD is used for a session during which a user can not trigger conflicting role in the same time.

Now, we deal with the few comparison points from (ref ORKA).

rule 1 :

 1 Only clerk and banker are allowed to make check deposit effective.

rule 2 :

 2 Only banker and chief agencies are allowed to cancel or validate a check deposit.

rule 3 :

 3 Only clerk and banker are allowed to modify the amount of a bank account.

Figure 1 :

 1 Figure 1: Class diagram used to express OrBAC style permissions

Figure 2 :

 2 Figure 2: Instance of the class diagram used for the running example

Figure 3 :

 3 Figure 3: Instance of the class diagram used for the running example

(

  [c := zoe, d := 1, m := 123, u := adrian])| p ∈ U ser.name() : | p ′ ∈ U ser.name() : ( p, , , , deposit( c, d, m ) p = p ′ =⇒ p ′ , , , , validate( c, d, m ) | p ′ , , , , cancel( c, d, m ) ) *

Figure 4 :

 4 Figure 4: Architecture of the PDP

  We present those permissions, in PE called permissionB.

permissionB ( ) ( adrian, clerk, , , deposit( , ) boris, banker, , , deposit( , ) | boris, banker, , , cancel( , ) | calvin, chie f agency, , , cancel( , ) | boris, banker, , , validate( , ) | calvin, chie f agency, , , validate( , ) | boris, banker, , , credit( , ) | adrian, clerk, , , credit( , ) ) *

  To express this permission we could use this PE in addition to the class diagram :

	User
	name		Role
	adrien		name
	boris		customer
	calvin		clerk
	daria		banker
	elisa		chief agency
	franck
				Action
	Branch		name
	name limit		deposit
	Montreal	10 000$	cancel
	Toronto	8 000$	validate
				credit
			Play
	User	Role	Organisation
	adrian	clerk	Montreal
	boris	banker	Montreal
	calvin	chief agency	Montreal
	daria	clerk	Toronto
	elisa	banker	Toronto
	franck	chief agency	Toronto
		permission
		role	branch	action
		clerk	Montreal	deposit
		clerk	Montreal	credit
	banker	Montreal	deposit
	banker	Montreal	cancel
	banker	Montreal	validate
	banker	Montreal	credit
	chief agency	Montreal	cancel
	chief agency	Montreal	validate
		clerk	Toronto	deposit
		clerk	Toronto	credit
	banker	Toronto	deposit
	banker	Toronto	cancel
	banker	Toronto	validate
	banker	Toronto	credit
	chief agency	Toronto	cancel
	chief agency	Toronto	validate
	permissionC ( )
	(
		damien, , , , cancel( , )

  , , , deposit( c, d, m) p = p ′ =⇒ p ′ , , , , validate( c, d, m ) | p ′ , , , , cancel( c, d, m ) ) *We suppose now we received the security event adrian, clerk, Montreal, 1234, deposit( zoe, 1, 123 ) . We apply the transition rules to separationP and show what it becomes :

	separationP' ( )
	c ∈ U ser.name()\{zoe} : m ∈ f loat\{123} :
	| p ∈ U ser.name() : | p ′ ∈ U ser.name() :
	(	p, , , , deposit( c, m )
		p = p ′ =⇒
		p ′ , , , , validate( c, m )
		| p ′ , , , , cancel( c, m ) ) *

( ) c ∈ U ser.name() : d ∈ int : m ∈ int : | p ∈ U ser.name() : | p ′ ∈ U ser.name() : ( p,

model specification

The first point to consider in this category is the level of abstraction that can be used in the model. With EB 3 SEC or [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF], we deal with a high level of abstraction, for example in a SOA architecture we deal with web-services. In [START_REF] Basin | Model driven security: From uml models to access control infrastructures[END_REF] amd XACML, we deal with object and operation that are implemented in the code of the software.

In [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF], XACML and EB 3 SEC the underlying model of the specification is formal. However if we consider the XACML with only the standard it is non formal whereas [START_REF] Basin | Model driven security: From uml models to access control infrastructures[END_REF] is structured and semiformal; it is structured as it is using schemas and UML notation and semi-formal as it is using for example first order predicates to express constraints for permissions.

All of these four method have the same purposed : they are used to enforce a AC policy in a IS. They also tends to have the same using area : IS built on a SOA architecture.

In [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF], [START_REF] Basin | Model driven security: From uml models to access control infrastructures[END_REF] and XACML the underlying model of the specification is a RBAC model. In other word, AC authorizations have to comply with the RBAC model. In EB 3 SEC, the underlying model, is chosen by the person who models the policy. In this paper, we choose a model derived from the OrBAC methods, but in other cases we could use a RBAC model or a home made model designed to ease the modeling step.

Policy expressiveness

[3] allows one to express permissions with constraints on the model. [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF] allows one to express permission and SoD constraints at the workflow level. XACML allows one to express permissions, prohibitions and Sod constraints on the model. EB 3 SEC allows one to to express permissions and prohibitions with constraints, obligations and Sod at a workflow level on the model.

In EB 3 SEC and [START_REF] Basin | Dynamic enforcement of abstract separation of duty constraints[END_REF] the model includes workflow routing concepts such as serialization, selection, iteration, and parallelization of steps and is able to control the order of events in a fine-grained manner.

In this paper we present only the EB 3 SEC language. Thus, we do not mention the other comparison point of [START_REF] Alm | A classification framework designed for advanced role-based access control models and mechanisms[END_REF] which deals with our future work or with other parts of our project. Compared to the three other methods, EB 3 SEC seems to be a language more powerful in term of expressiveness : In fact, it had the particularity of allowing the modeler to use a standard model or a home made model and also to allow him to express different constraints as permissions, prohibitions, obligations and SoD on a finned grained level. All of these constraints are not allowed at the same time by a unique method at a time.


Abderrahman Matoussi
email: abderrahman.matoussi@univ-paris12.fr

Régine Laleau
email: laleau@univ-paris12.fr

A Survey of Non-Functional Requirements in Software Development Process

Keywords: Requirements engineering, Non-functional requirements, Software development process

Due to the enormous pressure towards deploying software as fast as possible, functional requirements have been the main focus of software development process at the expense of implementing non-functional requirements (NFRs) such as performance and security. Thus, in practice, NFRs have been observed to be frequently neglected or forgotten in the software development process. However, NFRs is an important concept in requirements engineering which plays an essential role in the success or the failure of systems. NFRs introduce quality characteristics, but they also represent constraints under which the system must operate. So, the chances of success for the software system are maximized when NFRs are modeled since the initial phases of the development process. This article reviews the NFR concepts, relates them to the overall software development process and identifies new areas of further work.

Introduction

It is clear that the primary measure of success of a software system is the degree to which it meets the purpose for which it was intended. In this sense, requirements engineering is the process of discovering that purpose by identifying stakeholders and their needs. Several definitions of requirements engineering have been proposed in the literature. The most used one is the one proposed by [START_REF] Zave | Classification of Research Efforts in Requirements Engineering[END_REF] "Requirements engineering is the branch of software engineering concerned with the real-world goals for, functions of, and constraints on software systems. It is also concerned with the relationship of these factors to precise specifications of software behavior, and to their evolution over time and across software families". It is judicious to affirm that it is an attractive definition for a number of reasons, related especially to the notion of precise specifications. These last ones provide the basis for analysing requirements, validating them, defining what designers have to build and verifying that they have done so correctly upon delivery. Thus, requirements specification is a critical task because if we introduce mistakes , it is difficult and expensive to remove them afterwards. For that, it is important to be interested in the way these requirements are specified. There are two extreme ways of specifying software requirements: a complete formal specification and an informal specification. There also exist some intermediate representations that have shown to be useful in communication between users and specialists. In spite of it offers better results, formal specification has been often neglected in the literature because it is still perceived as more difficult and expensive (time and expert person). We think that is crucial to define the notion of formal specification in order to emphasis its importance into the requirements engineering. Hence, we note that formal specification is the expression, in some formal language and at some level of abstraction, of a collection of properties some system should satisfy. Moreover, we can note that the act of formalization in itself has been widely experienced to raise many questions and detect serious problems in original informal formulations. According to [START_REF] Van Lamsweerde | Formal Specification: a Roadmap[END_REF], a specification is formal if it is expressed in a language made of three components: (i) rules for determining the grammatical of sentences (the syntax); (ii) rules for interpreting sentences in a precise (the semantics); (iii) rules for inferring useful information from the specification (the proof theory). It is also important to indicate that there are different levels in the software lifecycle at which formal specification may enter the picture: when modelling the domain, when designing a functional model for the software, when designing the software architecture or when modifying or re-engineering the software.

Non-functional requirements is another important concept in the requirements engineering which plays an essential role in the success or the failure of systems. The NFRs concept has been widely studied by the community. Several definitions of NFR exists in the literature. IEEE defines Non-Functional Requirements as "a software requirement that describes not what the software will do, but how the software will do it, for example, software performance requirements, software external interface requirements, design constraints, and software quality attributes". In order to better understand the concept of NFR, [START_REF] Glinz | On Non-Functional Requirements[END_REF] constitutes an excellent reference which surveys all the definitions of the NFR term in the last 20 years and discusses all the limits of these definitions. The variety of the researches which deal with NFRs allow us to affirm that they are now part of several requirements engineering syllabus. Up to now, the majority of these researches have not focused on NFRs as first class requirements. In fact, incorporating NFRs into the different phases of the software life-cycle is a very hard task. Researchers face many challenges including great diversity of NFRs, NFRs subjective nature, formally specifying requirements, incorporating these requirements into models used for specifying functional requirements and resolving conflicts among NFRs. The latter is a very important challenge. Indeed, requirements do not manifest in isolation and normally satisfying one NFR may affect negatively the satisfaction of another. For instance, when we decide to use a double password to ensure security (one NFR), it can impact the system performance (another NFR) because checking two different passwords slow down the system. Despite this obvious importance and relevance of NFRs, NFRs are almost always left to be verified after the implementation is finished, which means NFRs are not mapped directly and explicitly from requirements engineering to implemetnation. This leaves software development with potential exacerbation of the age-old problem of requirements errors that are not detected until very late in the process. The authors of [START_REF] De | Non-Functional Requirements for Object-Oriented Modeling[END_REF] enumerate some of the well-known problems of the software development due of the NFRs omission: cost and schedule overruns, software systems discontinuation and dissatisfaction of software systems users. For all that, it is important to affirm that NFR should affect all levels of software life cycle and shall be identified as soon as possible and their elicitation must be accurate and complete. In the rest of the paper, we are going to review the background information on especially existing NFR related work at the requirements analysis and specification level, the design level and the implementation level.

The remainder of the paper is organized as follows. Section 2 reviews the state of the art that handles NFRs in the areas of requirement analysis and specification. Section 3 focuses on the design level. Section 4 concentrate on the implementation level. Section 5 highlights the complete approaches that consider NFRs through the whole process of software development. Finally, Section 6 draws some conclusions and highlights current limits.

Requirements analysis and specification level

It is clear that a current industrial practice is to specify only functional requirements at the first levels of software development and the NFRs at the implementation level. Consequently, initial levels (analysis and specification) of a software system may not reflect the NFRs properly and may lead to a failed product. In order to resolve this problem, international standard are recommending the consideration of NFRs during its development process, beginning from the step in which requirements are specified in detail. Different approaches have been proposed ranging from unstructured and informal text to highly formal mathematical approaches. The approach used in each case depends on the goals of the project and the available resources.

Informal and semi-formal approaches

The main interest of informal and semi-formal approaches is that they don't need a high personal expertise. Thus, it is easy to use these approaches. However, these approaches provide very little support for system analysis; i.e. there is no certainty that the obtained specifications are complete or no ambiguous. A survey of the literature found that most people use informal or semi-formal approaches to specify NFRs because the formal ones are still perceived as more difficult and expensive. In what follows, we present some informal and semi-formal methods presented in the literature to analyze and specify both NFRs and functional requirements.

The NFR Framework [START_REF] Chung | Non-Functional Requirements in Software Engineering[END_REF] is the most popular work in this topic. It treats NFRs as soft goals (goals that are hard to express) to be addressed during the development process. NFRs, design decisions and their relations are captured in a goal graph where the nodes are either NFRs or design decisions. Goals in NFR Framework can be refined into detailed concrete goals. NFR Framework makes the relationships between NFRs and intended decisions explicit. This helps better understand the impact of every design decision; i.e. typically one design decision may impact multiple NFRs positively or negatively. The main interest of this framework is that it can reused by other models to handle NFRs. For instance, [START_REF] Kassab | Scope Management of Non-Functional Requirements[END_REF] presents a systematic and precisely semi-formal model that extends the taxonomy of the NFR Framework by integrating the concept of "hard goals NFRs" within the requirements engineering process. This model details the sequence of systematic activities towards an early consideration of identifying, specifying and separating FRs and NFRs: (i) requirements elicitation that aims to discover the requirements for the system; (ii) analysis and crosscutting realization; (iii) composing requirements that integrate identified crosscuttings (both functional and non-functional) with the use-case model and the domain model.

In [START_REF] Haruhiko | Refining Behavioral Specification for Satisfying Non-functional Requirements of Stakeholders[END_REF], the authors present a new informal procedure for requirements engineers to elicit requirements specification with its evaluation of stakeholders. Since many kinds of stakeholders participate in one system development, some stakeholder requirements conflict with others. To coordinate the requirements among stakeholders or to find a trade-off, criteria shared by the stakeholders are required. [START_REF] Haruhiko | Refining Behavioral Specification for Satisfying Non-functional Requirements of Stakeholders[END_REF] affirm that NFRs can play this role because they influence the concerns of most of stakeholders. Hence, NFRs are used for checking stakeholders satisfaction. With this procedure, stakeholder-dissatisfaction can be reduced and new possibilities to satisfy or dissatisfy other stakeholders can be found. The outputs of this procedure are the refined specifications written in a sequence diagram and evaluation tables which are used to store the evaluations of each stakeholder. The rows in an evaluation table correspond to requirements types. The columns of the table correspond to the kinds of stakeholders. Each cell in the table shows a stakeholders evaluation by the type of requirement. Each cell is labeled by three attributes: a reference of a refined specification, a score and the content of the evaluation. We think that the notation of this procedure is simple but useful for stakeholders to validate the correctness of specifications on the spot. However, this procedure is not suitable for the cases where requirements engineers can not interactively elicit requirements from stakeholders. We think also that priority or bias should be given to some kind of NFRs, or to some kind of stakeholders, when a specific analysis is needed.

The quality attributes taxonomy [START_REF] Barbacci | Quality Attributes[END_REF] is another semi-formal work which is the result of CMU SEI's research work on how quality attributes impact a software architecture. The interest of this work is that the terminology used in the taxonomy can serve as a vocabulary to specify NFRs and then drive the design of the architecture. The taxonomy is divided into four areas: performance, dependability, security, and safety. All quality attributes are analyzed through three dimensions: concerns, factors, and methods. Firstly, concerns or requirements are the parameters by which the attributes of a system are specified. Secondly, factors are the properties of the system and its environment that have an impact on the concerns. Factors might not be independent and might have cause/effect relationships. Thirdly, methods specify how to address the concerns.

The quality attributes taxonomy has inspired many other works. For instance, [DKKP03] presents a semi-formal approach for eliciting and documenting efficiency requirements (a type of NFRs) with use cases and a high-level architecture. This approach uses quality attributes and also quality models to capture general knowledge on NFRs, while specific NFRs are captured in a template. The interest of this approach is that it uses a generalized metamodel and a quality model that can then be used for other NFRs.

Agile development methods are often criticized for not having explicit practices for eliciting NFRs [START_REF] Paetsch | Requirements Engineering and Agile Software Development[END_REF]. However, [START_REF] Ho | On Agile Performance Requirements Specification and Testing[END_REF] discuss an agile approach to address the specification and testing of performance which is an important type of NFRs. Thus, [START_REF] Ho | On Agile Performance Requirements Specification and Testing[END_REF] proposes an evolutionary model called software performance requirements evolution model PREM). Using the model as a guideline, a development team can identify and specify performance requirements incrementally, starting with casual descriptions, and refine them to a desired level of detail and precision.

Misuse cases [HP05, [START_REF] Sindre | Eliciting Security Requirements with Misuse Cases[END_REF][START_REF] Firesmith | Security Use Cases[END_REF] are other approaches, based on UML, to handle NFRs such as security requirements. Misuse cases are the inverse of use cases and describe functions that the system should not allow. In [START_REF] Herrmann | Quality Misuse[END_REF], the authors outline concepts for an analysis of NFRs of a software system and develop a misuse based method for deriving detailed NFRs but also functional requirements. The authors believe that the analysis of NFRs in terms of assets, threats, misusers and countermeasures helps to complement software and project requirements. The approach presented in [START_REF] Firesmith | Security Use Cases[END_REF] differentiate between misuse cases that are more appropriate for analyzing and specifying security threats and security use cases that should be used to analyze and specify security requirements (see Figure 1). Misuse cases and security use cases inherit the simplicity and popularity as well as the semantic inconsistencies of UML. KAOS(Knowledge Acquisition in autOmated Specification) [START_REF] Van Lamsweerde | Goal-Oriented Requirements Engineering: A Guided Tour[END_REF][START_REF] Letier | Reasoning About Agents in Goal-Oriented Requirements Engineering[END_REF] is another semi-formal approach for eliciting, analyzing and modeling essentially functional requirements. KAOS requirements model is based on first-order temporal logic and it is composed of several sub-models related through inter-model consistency rules. [START_REF] Van Lamsweerde | Elaborating Security Requirements by Construction of Intentional Anti-Models[END_REF] has then extended KAOS to handle NFRs such as security requirements. Thus, the author specifies some generic specification patterns for eliciting security goals such as confidentiality, integrity, availability, privacy, authentication and non-repudiation. The general method for elaborating KAOS security requirements [START_REF] Van Lamsweerde | Elaborating Security Requirements by Construction of Intentional Anti-Models[END_REF] is based on the incremental building and specification of two concurrent models: an intentional model of the system-to-be and an intentional anti-model yielding vulnerabilities and capabilities required for achieving the anti-goals of threatening security goals from the original model. The method allows threat trees to be derived systematically through anti-goal refinement until leaf nodes are reached that are either attack vulnerabilities observable by the attacker or anti-requirements implementable by this attacker. The original model is then enriched with new security requirements derived as countermeasures to the anti-model.

Formal approaches

Formal NFRs elaboration method written in a formal language became more and more a necessity. However, a familiar problem with formal methods in specifying such requirements is the high cost and difficulty of using them. Researchers justify this cost by applying formal methods only to crucial NFRs such as security requirements. Indeed, the most NFRs are critical aspects of the system that may otherwise result in huge losses in terms of time money and data when poorly specified. In the following, we present some research works on the formalization of NFRs.

Formal Design Analysis Framework (FDAF) [START_REF] Cooper | Developing a Formal Design Analysis Framework[END_REF] is intended to support the systematic design of a system that meets its NFRs such as performance, security, etc. A variety of notations have already been used to describe architectures including UML (standard, formalized, with OCL, and extended) and formal methods to support the rigorous analysis of a design. An overview of the FDAF is illustrated in Figure 2. In this figure, the FDAF is represented with a cloud surrounded by the stakeholders, inputs, and outputs of the framework. The stakeholders are the designers, requirements engineers, and formal methodologists who use the framework to develop and evaluate a system design that meets its functional and non-functional requirements. The inputs include an object-oriented design model documented in the UML notation and a requirements specification that includes the NFRs and FRs for the system. FDAF assist the user in selecting a formal method, and translates an extended semi-formal UML design into a formal notation. The major limit of FDAF is that the variety of formal notations used to formalize NFRs constitute an obstacle to study the different interactions between NFRs. Consequently, the user cannot detect conflicts between the different types of NFRs. [Aag01, Zsc04a, Zsc04b] present formal specification languages for non-functional properties of component-based systems. For instance, [START_REF] Zschaler | Formal Specification of Non-functional Properties of Component-Based Software[END_REF] shows a formal specification of timeliness properties of a component-based system, as an example for a formal approach to specifying non-functional properties. For that, the work use extended temporal logic of actions (TLA+) to describe the system. The logic is a temporal logic where states are represented as values assigned to state variables. CQML(Component Quality Modeling Language) [START_REF] Oyvind | Quality of Service Support in Development of Distributed Systems[END_REF] is another useful specification language for components QoS properties.

Another work of NFR formalization is [BBF + 01]. It present the language NoFun (acronym for NOn-FUNctional) which consists of three different parts. Firstly, software quality characteristics and attributes are defined. Secondly, values are assigned to component quality basic attributes. Thirdly, quality requirements can be stated over components, both context-free and context-dependent. The language contains structuring mechanisms, type definition elements and other constructs that give an appropriate support for defining non-trivial quality models. The work [BBF + 01] studies also how these concepts can be mapped to UML using its extension mechanisms. Recently, [KHP + 08] present a work in progress which describes the formal requirement specifications for increasing the safety and reliability of the railway system using Z notation.

Design level

The idea of incorporating NFRs with FRs in the design level is not new. A survey of the different works found that most of them use UML with some extensions to add NFRs with the functional requirements models. In the next, we are going to present the different solutions proposed in the literature that try to consider NFRs at the design level.

[SC04] presents a use case and goal-driven approach to integrate functional requirements and NFRs. It propose to associate the NFRs with four use case model elements: actor, use case, actor use case association and the system boundary. Their framework specifies the scope of each type of NFR association through the formalization of NFR scope propagation rules. This take advantage of relationships between the different elements of use case (specialization, generalization, extends, includes). Thus, the solution proposed affirms that NFRs can be integrated at the design level with FRs and can provide better understanding of the requirements model. The authors of [START_REF] Moreira | Crosscutting Quality Attributes for Requirements Engineering[END_REF] propose a new model which identify all the requirements of a system and select from those the quality attributes relevant to the application domain and stakeholders. Then, they propose a template for quality attributes and integrate them with functional requirements using an extended use case diagram. In the same way, [START_REF] Berenbach | Toward a Unified Model for Requirements Engineering[END_REF] extends UML use case diagram with some notation to express functional requirements, NFRs and the hazard (area that presents additional challenges to the requirements analyst).

[ [START_REF] Luiz | Using UML to reflect Non-functional Requirements[END_REF][START_REF] De | Non-Functional Requirements for Object-Oriented Modeling[END_REF] propose a new strategy that brings NFRs to object-oriented modeling called OONFR (Object-Oriented Non Functional Requirements). This strategy uses as input a Language Extended Lexicon of the Universe of Discourse (LEL of UofD). This latter is composed of entries, which describe symbols of the language of the UofD, through notions and behavioral responses. These entries can be classified as subject, verb, object, and state. Many others works have also studied the integration of NFRs at the design level. For instance, [START_REF] Zhu | UML Profiles for Design Decisions and Non-Functional Requirements[END_REF] propose a UML profile for modeling design decisions and an associated UML profile for modeling NFRs in a generic way. Hence, the two UML profiles consider design decisions and NFRs as first class elements. This relationship between design decisions and NFRs is modeled using specialized dependency notations in UML. [START_REF] Supakkul | A UML Profile for Goal-Oriented and Use Case-Driven Representation of NFRs and FRs[END_REF] proposes an integrating modeling language by extending UML with the NFR Framework [CNYM00] using the UML Profile. Thus, they define a meta-model to represent the concepts in the NFR Framework and they identify the extension points for integrating the two notations. [START_REF] Subrina | Towards a Framework to Incorporate NFRs into UML Models[END_REF] propose a novel framework for integrating NFRs with the UML design of a software system which can be applied during the re-engineering process of legacy systems. [START_REF] Xu | Towards Modeling Non-Functional Requirements in Software Architecture[END_REF] proposes a grouping mechanism to model NFRs in software architectures directly and explicitly. The approach proposes a conceptual architectural design model which views the traditional architecture model for software systems as the first layer. The operations of satisfying NFRs are represented as aspectual components in the second layer. [J 02] proposes UMLsec which is an extension of UML notation. UMLsec allows to express security relevant information within diagrams in a system specification. UMLsec is defined in form of a UML profile using the standard UML extension mechanisms. In particular, the associated constraints give criteria to evaluate the security aspects of a system design, by referring to a formal semantics of a simplified fragment of UML. [START_REF] Lodderstedt | SecureUML: A UML-Based Modeling Language for Model-Driven Security[END_REF] present a modeling language, based on UML, called SecureUML. It shows how UML can be used to specify information related to access control in the overall design of an application and how this information can be used to automatically generate complete access control infrastructures. [START_REF] Lodderstedt | SecureUML: A UML-Based Modeling Language for Model-Driven Security[END_REF] adapt use cases to capture and analyse security requirements. This adaptation is called an Abuse Case Model. An abuse case is defined as a specification of a type of complete interaction between a system and one or more actors, where the results of the interaction are harmful to the system, one of the actors, or one of the stakeholders of the system.

Implementation level

A survey of the literature found that current programming languages were not designed with NFRs. However, some works have tried to bridge this gap by proposing new programming styles which process NFRs at the implementation level. In the following, we review various policy mechanisms that can be used to implement NFRs. [START_REF] Bolognesi | Toward Constraint-Object-Oriented Development[END_REF] introduce a new programming style into the existing object-oriented language Java. This new method is called "Constraint and Object Oriented" programming style. So, [START_REF] Bolognesi | Toward Constraint-Object-Oriented Development[END_REF] propose to conservatively extend object-oriented decomposition by letting it affect also operations (methods). Different objects may support different parts of the same operation. The responsibility of defining an operation, in terms of enabling conditions and effects on the state, is distributed over several interacting objects, which act as constraints and express different, partial views about the system behavior. The last revision of Ada language [START_REF] Fidge | The Challenges of Non-Functional Computing Requirements[END_REF] is another example of new programming style which takes account different NFRs. Firstly, timeliness requirements will be better served by improved definitions of timeouts and a minimum run-time environment. Secondly, dependability will be assisted by the ability to attach "watchdog" timers to code blocks. Thirdly, security requirements are addressed by well established user authentication, encryption and message certification technologies. Lastly, adaptability will be addressed by the ability to change task priorities dynamically. Exception Mechanism is also another new style programming which is supported by many current programming languages like C++ and Java. This mechanism separates the normal control flow from the exceptional control flow under error conditions. This separation of concerns and centralized exception handling reduce the complexity of programming. Thus, exception mechanism can be viewed as a special form of policy because it provides a mechanism to specify the policies about how to handle faults.

They are also another type of solution proposed by many works that combines rule based techniques and object oriented programming. For example, [START_REF] Ahmed | R++ User Manual for Release 1[END_REF] present a new language, called R++ rules, which is an extension to C++. R++ rules are triggered automatically upon relevant data change. One important contribution of R++ is that it introduced rule as member class. R++ Rules are introduced as a natural extension to object-oriented classes, they support inheritance, overriding, and visibility rules. ILOG JRules is another language presented in [START_REF][END_REF]. It directly use the Java objects. Jrules are organized into groups called packets. "Packet" is represented as a property of a rule. This language supports temporal reasoning: the "wait" statement is used in the condition part of a rule. Thus, the "wait" statement allows to test if conditions become valid during a designated waiting period.

In summary, the limits of current programming languages for implementing NFRs are well-known. In order to face this problem, we think that the implementation for NFRs shall be separated (in some cases) from the implementation for the functional requirements. We think also that a strong traceability between NFRs and functional requirements can address this problem.

Complete approaches

All the above approaches present the way NFRs can be handled within a specific step of the software development process. However, some other approaches cover the whole development process, as presenting in the next.

[BL03] propose a model called FRIDA (From RequIrements to Design using Aspects) in which the key objective is to guide the developer through the basic phases of the software life cycle. FRIDA determine a way to elicit and model separately both functional and nonfunctional requirements. In order to achieve that, the FRIDA model is founded on the aspect-oriented software development. Aspects are a complementary manner to describe NFRs. In FRIDA, each NFR is represented with one or more aspects and is not restricted to a single level. Functional requirements are restricted to class hierarchies. Checklists are used to refine NFRs at early-stages of the development life cycle. The FRIDA model considers that the identification and resolution of conflicts is as important as the elicitation of NFRs at the early stages of the software development life cycle. For that, FRIDA use a conflicts matrix to automate this process whenever possible. The UML notation and extensions of it are used to determine this model and allow the modeling of both objects and aspects involved in the system. The aspect extraction and the visual modeling of aspects are very important for FRIDA because they allow the creation of models that can be reused in the future. Moreover, connections between diagrams that belong to distinct phases of software development allow a high level of traceability.

[LYL + 05] define a coherent goal-driven process applicable at the requirements level as well as the implementation level. This process (called reuse process) uses an asset library to find quality characteristics and apply them to a software functional description. [LYL + 05] shows that it is possible to store qualities, retrieve them for reuse, specialize them for different contexts and integrate them with functional descriptions.

The B method [Abr96] is a full formal method which uses set theory notations to specify, design and implement software systems. The most important feature provided by the B method is its ability to stepwise refine specifications. Refinement is a process that transforms an abstract and non-deterministic specification into a concrete and deterministic system that preserves the functionality of the original specification. A key merit of this refinement mechanism is the ability to preserve already proven system properties in higher level models.

Proof obligation are generated from B models. They guarantee correctness and effectiveness of the system development. The B method is supported by tools that guide the developer through the basic phases of the software life cycle. Recently, [START_REF] Hassan | Goal-Oriented, B-Based Formal Derivation of Security Design Specifications from Security Requirements[END_REF] present a work in progress using the B method to handle NFRs. It proposes a formal approach that derives design specifications from a set of security requirements modeled using an extension of KAOS for security. The approach provides a secure software engineering methodology that effectively integrates KAOS security extension. It is characterized by the ability to formally build a complete, consistent and clear requirements model with the B method. Figure 3 shows the main steps of this approach. The first step of the approach is to transform a KAOS security requirements model to abstract B model. The second step is to refine the model using B refinement mechanism to generate design specifications and implementation. Thus, the approach shows that KAOS could be extended with an extra step of formality in order to fully implement security requirements. This extension establishes a reasonable bridge between security requirements and design specifications. However, the approach needs to be: (i) demonstrated on a number of different case studies; (ii) generalized to other NFRs.

[MGM03a] proposes an approach that considers security concerns (a type of NFRs) as an integral part of the entire system development process. This approach integrates security and systems engineering using the same concepts and notations, throughout the entire system development process. It falls within the context of the Tropos methodology [START_REF] Castro | A Requirements-Driven Development Methodology[END_REF] that considers not only the system functional requirements but also NFRs such as security, reliability, and performance. Tropos is based on the idea of building a model of the system that is incrementally refined and extended from a conceptual level to executable artefacts, by means of a sequence of transformational steps. Tropos adopts the i* modelling framework [START_REF] Yu | Modelling Strategic Relationships for Process Reengineering[END_REF] which uses the concepts of actors, goals, tasks, resources and social dependencies for defining the obligations of actors (dependees) to other actors (dependers). In addition to the graphical representation, Tropos provides a formal specification language called Formal Tropos [START_REF] Fuxman | Model Checking Early Requirements Specifications in Tropos[END_REF]. It complements graphical Tropos by extending the Tropos graphical language with a formal specification language. The language offers a textual notation for i* models and allows the description of different elements of the specification in a first order linear-time temporal logic inspired by KAOS [START_REF] Van Lamsweerde | Goal-Oriented Requirements Engineering: A Guided Tour[END_REF][START_REF] Letier | Reasoning About Agents in Goal-Oriented Requirements Engineering[END_REF] that has formal semantics and is amenable to formal analysis. In addition, Formal Tropos serves also to verify the model of the system by employing formal verification techniques such as model checking to allow for an automatic verification of the system properties. However, both Tropos and Formal Tropos were not conceived with security on mind. [START_REF] Mouratidis | A Natural Extension of Tropos Methodology for Modelling Security[END_REF][START_REF] Mouratidis | An Ontology for Modelling Security: The Tropos Approach[END_REF] presents extensions to the Tropos ontology to enable it modeling security issues. Concepts and notations such as security constraint, secure entities and secure dependencies are introduced to the existing graphical Tropos and also Formal Tropos grammar was extended to provide formalism for our newly introduced concepts. However, this extension only apply to the first level of the Tropos ontology.

Conclusion

Despite the fact that NFRs are very difficult and expensive to deal with, the increasing software complexity and competition in the software industry has highlighted the need to consider NFRs as an integral part of software development process. For that, many works have studied them through the different phases of the software life cycle. Thus, this paper shows that NFRs obviously impinge on all the software development process. However, many problems and shortcomings still remains. Firstly, the informal treatment of NFRS since the first levels of the development chain; i.e. the requirements analysis and specification levels. Secondly, it seems difficult to define one method to cope with all NFRs due to their great diversity. Finally, few research works have focused on NFRs as first class requirements in the development process. To bridge these gaps, researchers face many challenges: (i) extending and relaxing formal methods in order to support the majority of NFRs; (ii) modeling and analyzing functional requirements and NFRs that should be considered separately; (iii) providing methodologies guidance through the whole development process.

Figure 1 :

 1 Figure1: Misuse Cases and Security Use Cases[START_REF] Firesmith | Security Use Cases[END_REF]

Figure 2 :

 2 Figure 2: Formal Design Analysis Framework [CDDD03]

  The outputs of OONFR strategy is a UML class diagram with indications of what classes, attributes, operations and relationships are responsible for satisfying NFRs. In other words, the class diagram has signals of what classes, attributes, operations, and relationships specialize satisfying strategies and satisfy NFRs. In summary, OONFR strategy consists of the following activities: build the Language Extended Lexicon of Universe of Discourse-NFR (LEL of UofD-NFR), build the scenarios and build the UML class diagram. The authors indicate that the extension of this strategy to other UML artifacts and more automation of the strategy can give it more importance.

Figure 3 :

 3 Figure 3: Formal Derivation of Security Design Specifications [HBEE08]