Wael Kanoun

Nora Cuppens-Boulahia

Frédéric Cuppens

Samuel Dubus

Risk-aware Framework for Activating and Deactivating Policy-based Response

Keywords: Response policy, threat and response contexts, activation/deactivation, cumulative impact, success likelihood

With the growth of modern systems and infrastructures, automated and intelligent response systems become the holy grail of the security community. An interesting approach proposes to use dynamic access control policies to specify response policies for such systems. These policies should be enforced when an ongoing attack, that threatens the monitored system, is detected. However, existing work do not present a clear methodology to specify the Response policies. In particular, the deactivation issue is not yet tackled. In this paper, we first present how to specify response policies. Second, a risk-aware framework is proposed to activate and deactivate response policies. Hence, the success likelihood of the threat, and the cumulative impact of both of the threat and the response, are all considered.

I. INTRODUCTION

Information systems, critical services and infrastructure are continuously growing in size and complexity. Network operators are providing a wide range of services such as voice (VoIP) or television (TVoIP) based on these systems. Unfortunately, they remain always an attractive target for hackers and criminal organizations. The attacks may be accurately pointed, or performed at a large scale. Therefore, a proper and efficient response system becomes primordial, to insure the availability and the security of these systems and the provided services.

This interesting issue has been driving the research community to propose several intelligent response models. These response models aim to identify and select the most efficient countermeasure(s), in order to stop the detected attack or mitigate its impact. For instance [START_REF] Foo | Adepts: Adaptive intrusion response using attack graphs in an e-commerce environment[END_REF] presents an adaptive intrusion response model that considers the intrusion's spread, using intrusion graphs. On the other hand, models that adopts a cost-benefit approach have been proposed: [START_REF] Wei | Cost-benefit analysis for network intrusion detection systems[END_REF], [START_REF] Toth | Evaluating the impact of automated intrusion response mechanisms[END_REF], [START_REF] Lee | Toward costsensitive modeling for intrusion detection and response[END_REF], [START_REF] Balepin | Using specificationbased intrusion detection for automated response[END_REF], and [START_REF] Stakhanova | A cost-sensitive model for preemptive intrusion response systems[END_REF] consider the cost (or the impact) of the detected attack and the candidate countermeasure(s). [START_REF] Jahnke | Graph based metrics for intrusion response measures in computer networks[END_REF] and [START_REF] Kheir | Cost evaluation for intrusion response using dependency graphs[END_REF] consider service dependencies to calculate more accurately the impact of the attack and the candidate countermeasure(s). Moreover, [START_REF] Gehani | Rheostat : Real-time risk management[END_REF] and [START_REF] Kanoun | Advanced reaction using risk assessment in intrusion detection systems[END_REF] propose to consider the risk of the ongoing attack; in other words they combine the impact with the success likelihood of ongoing attacks to assess dynamically the risk(s).

On the other hand, a different approach has been proposed in [START_REF] Debar | Enabling automated threat response through the use of a dynamic security policy[END_REF]. The response, as presented in this paper, is based on activating and enforcing dynamic policies to counter an attack. We view this approach more global than the previous models above. While the previous models have a local and limited scope on the monitored system (i.e. tactical), the latter has a far larger scope and acts as 'strategic' response model. [START_REF] Cuppens | Expression and deployment of reaction policies[END_REF] and [START_REF] Cuppens | Web-Based Information Technologies and Distributed Systems[END_REF] show that the two approaches are complementary, and combine them in a single response workflow. Thus, response may be performed at two levels: intermediate level (i.e. tactical) and high level (i.e. strategic). The former is based upon launching single and local countermeasures, while the latter is policy-based and may affect the entire system. However, several interesting issues have been raised. First, the aforementioned papers do not consider the deactivation of these policies during specification. Second, these papers propose to activate a strategic response upon receiving and correlating the alerts that correspond to executed attacks. However these alerts may represent ongoing attacks that have a minor (or null) chance to succeed, given the attack progress and the real-time state of the monitored system. Third, previous work raise the deactivation issue, but they do not indicate how and when the strategic (i.e. policy-based) response should be deactivated. For instance, [START_REF] Debar | Enabling automated threat response through the use of a dynamic security policy[END_REF] relies on experts to assign static lifetime for the response policies, which is not satisfactory. Moreover, during the deactivation process of a strategic response, the system (or the administrator) may encounter the following cases: (i) some actions once activated, cannot be (simply) deactivated, or (ii) the expert needs to specify some actions that have to be executed only when the response is deactivated, but not before (e.g. notify the users that the service is back to normal).

In this paper, we first present how to specify response policies for complex systems, while considering the deactivation process. Then, we propose an online model with an associated architecture, which activates and deactivates response policies (i.e. strategic responses), using a risk-aware approach: the success likelihood of the ongoing threat/attack, and the cumulative impacts (i.e. cost) of the threat and the response, are all considered before activating/deactivating strategic response. This paper is structured as follows. Section II summarizes the state of the art of policy models, while Section III presents how response policies may be controlled, by proposing a response taxonomy. Section IV shows how to specify threat and response contexts. Section V defines a risk-aware framework to activate and deactivate threat contexts and response contexts. Section VI proposes an architecture to implement the activation and deactivation framework. Section VII presents a VoIP case study to illustrate our work.

II. SECURITY AND RESPONSE POLICY MODELS

To specify security and response requirements, several policy-based models may be used (e.g. RBAC [START_REF] Ferraiolo | Proposed nist standard for role-based access control[END_REF], Ponder [START_REF] Damianou | The ponder policy specification language[END_REF] and OrBAC [START_REF] El Kalam | Organization Based Access Control[END_REF]). However, RBAC and Ponder suffer from several drawbacks. First, they offer only a single dimension of abstraction, using roles assigned to subjects. Such abstraction is not offered for other entities (i.e. objects and actions). Obviously, this limitation will multiply significantly the number of security rules for a given policy. Second, RBAC does not consider the concept of organization. Therefore, the specification and the management of security policies for large and multi-regional systems, become tedious tasks. Finally, the dynamic nature of the response cannot be modeled with RBAC. For example, once an ongoing attack has been detected, a set of rules should be activated and enforced.

On the other hand, OrBAC does not suffer from the aforementioned limitations. It is expressive enough to specify a large variety of security requirements. In fact, it has been successfully applied to specify network access control policies. Moreover, translation mechanisms were defined to automatically generate firewall configuration rules that are free of inconsistency and redundancy [START_REF] Cuppens | A formal approach to specify and deploy a network security policy[END_REF]. Thus, we will use OrBAC in the remainder of this paper. We present below a brief description of the OrBAC Model. For more details and formal description, interested readers may refer to [START_REF] El Kalam | Organization Based Access Control[END_REF] and [START_REF] Cuppens | Modelling contexts in the or-bac model[END_REF].

A. The OrBAC Model

OrBAC is a security policy model centered on the concept of organization. Using OrBAC, security policies are specified at an abstract level. A concrete level policy may be inferred to enforce them in the monitored system.

Therefore, one of the OrBAC contributions is the abstraction of the traditional triples (subject, action, object) into (role, activity, view) . The entities subject, action and object are called concrete entities whereas the entities role, activity and view are called organizational (i.e. abstract) entities. A view is a set of objects that possess the same security-related properties within an organization. Thus, these objects are accessed in the same way. Abstracting them into a view avoids the need to write one rule for each of them. Another useful abstraction is that of action into activity. An activity (e.g. call) is considered as an operation which is implemented by one of the actions available in the organization (e.g. SIP call, NoE call and H323 call) 1 . Therefore, they can be abstracted with a unique activity for which we may define a single security rule.

Another main contribution of the OrBAC model is the concept of context, that reduces the applicability of the rules to some specific circumstances [START_REF] Cuppens | Modelling contexts in the or-bac model[END_REF]. Using OrBAC, the expert can specify contextual abstract security rules:

• permission(org, R, A, V, Ctx) means that in organization org, the role R is authorized to perform the activity A, on the view V, when the context Ctx is activated. • prohibition(org, R, A, V, Ctx) means that in organization org, the role R is NOT authorized to perform the activity A, on the view V, when the context Ctx is activated.

• obligation(org, R, A, V, Ctx, Ctx v ) means that in organization org, the role R MUST perform the activity A, on the view V. The obligation context Ctx represents the set of conditions for which, the obligation holds. The violation context Ctx v represents the set of conditions for which, and while the obligation holds, the obligation is violated. Interested readers may refer to [START_REF] Rakaiby | Formalization and management of group obligations[END_REF] for a complete description of obligations. For example, prohibition(vodaphone; normal client, SIP call, Internet, Response SIP DoS) means that all normal clients of Vodaphone are not authorized to call using SIP protocol, if the SIP server was the target of a DoS attack.

Once the policy has been specified at the organizational level, it can be instantiated by assigning concrete entities to abstract entities and activating the needed context(s). Three predicates have been defined (empower, consider and use) to assign respectively a subject to a role, an action to an activity, and an object to a view:

• empower(org, S, R) specifies that in organization org, subject S is empowered in role R. • consider(org, A', A) specifies that in organization org, action A' implements activity A. • use(org, O, V) specifies that in organization org, object O is used in view V. For example: empower(vodaphone, 5322@vodaphone.com, normal client) means that 5322@vodaphone.com is a normal client in the operator's network.

III. USAGE OF ORBAC FOR POLICY-BASED RESPONSE

For any system, OrBAC may be used to specify the Operational Policy (OP), and the Response Policy (RP). The former is used to specify the security rules during 'normal' circumstances. The associated contexts might be for example geographic (e.g. on site, or outside), temporal (e.g. working hours, holidays), etc. On the other hand, the RP specifies the response rules that must be activated and enforced to counter each detected threat. Thus, each context in RP is specified to handle a potential threat. In the remainder of this paper, we will refer only to the RP. The expert has to associate the appropriate response rules to each response context, which in turn is associated to a threat context. A response context is activated only if the associated threat context has been already activated. However, in a monitored system, a threat could be detected (and therefore the associated context is activated), while the associated response context remains inactive due to other reasons (e.g. the strategic response cost exceeds that of the threat; or to avoid major conflicts because another strategic response has already been activated). This point will be clarified in the remainder of the paper.

In the first section of this paper, we mentioned the deactivation issue: how and when a response policy should be deactivated? It should be noticed that the deactivation of policy-based (i.e. strategic) responses is not a trivial task. In other words, the deactivation of a response policy (or more precisely a response context) does not simply consist of deactivating the associated security rules. This can be due to several reasons: • The expert needs to launch some actions only at the activation (or only at the deactivation) of a response policy (e.g. notify a user to change his password). • Whether it is impossible, or it is considered a tedious task that may impact the OP (i.e. the expert's intervention is needed to end the response), some of the response rules or countermeasures cannot be deactivated (e.g. patch a software, patch an OS, remove permanently a client from the database). • Some of the response rules or countermeasures have a very limited lifetime, and therefore are considered as automatically deactivated (e.g. close a malicious connection, restart a server, change a password). Therefore, a simple yet efficient solution is to specify for each response context, two associated event-based contexts: Start(response context), and End(response context). They correspond respectively to the activation and the deactivation of response context. [START_REF] Preda | Semantic context aware security policy deployment[END_REF] propose an operational semantic to specify event-based contexts associated to state-based contexts using the ECA (Event-Condition-Action) formalism [START_REF] Baral | Formal characterizations of active databases: Part II[END_REF]. The formal definition of this operational semantic is not in the scope of this paper due to space limitation. Now, we will present first a taxonomy for reactions and countermeasures. This will allow us to classify them with respect to their lifetime, and whether their lifetime is controllable or not.

A. Response Taxonomy

There are many papers that present reaction and response taxonomies, like [START_REF] Stakhanova | A taxonomy of intrusion response systems[END_REF] and [START_REF] Carver | An intrusion response taxonomy and its role in automatic intrusion response[END_REF]. However, none of them mentioned the lifetime of the countermeasures, or whether they can be deactivated. We propose a taxonomy that considers the temporal dimension of the response actions. We may refer to this taxonomy (See Figure 1) to classify any reaction or countermeasure. Thus, it may be also used to classify any security rule expressed in the RP, w.r.t. their lifetime and the controllability of their lifetime.

First, considering their lifetime, countermeasures (or reactions) may be divided initially into two major classes: one-shot countermeasures and sustainable countermeasures.

1) One-Shot countermeasures: A reaction has a one-shot lifetime when its effectiveness is limited to a single attack occurrence. Once a one-shot reaction is launched, it is automatically deactivated. The effective lifetime of this class of reactions is null (or negligible). That means future attacks may occur, as if this reaction was not launched. Therefore, a one-shot response has to be launched for each occurrence of the same attack. Examples of this class include: closing a malicious connection, restarting a server, notifying the administrator, etc. Let us consider a perfect system, where A is a set of (the same) attack occurrences, and CM the associated countermeasure occurrence. We define a relation f : A → CM . This relation can be read as "an element from A is ended by an element from CM ". In a perfect system, each attack must be ended, and thus f is an application:

Hypothesis 1: ∀ a ∈ A, ∃! cm ∈ CM | cm = f (a)
For each occurrence a of the attack A, a cm is required to end the attack. Therefore a cm i that ended the attack occurrence a i , has no effect on future attack a j (j > i). One-shot countermeasure can be defined with the following proposition which demonstrates that f is injective:

Proposition 1: ∀ a i , a j ∈ A; cm i = f (a i ) and cm i = f (a j ) ⇒ a i = a j
2) Sustainable countermeasures: A reaction has a sustainable lifetime when its effectiveness is not limited to a single attack occurrence. Once a sustainable reaction is activated, it remains active against future attack occurrences. In other words, its lifetime sustains for a period of time (which may be almost infinite). Therefore, the activation of a sustainable reaction may be effective against future attack occurrences, until this reaction is deactivated. Examples of this class include: patching software, blocking a machine, deleting an account, suspending an account, etc. Let us define the same function f : A → CM . f is not injective because a sustainable countermeasure cm i can end a sequence of attack occurrences {a i , a i+1 , ...} that occur during cm i lifetime. In other words, we can have several attack occurrences that are ended by the same countermeasure occurrence:

Proposition 2: ∃ a i , a j ∈ A | (cm i = f (a i )) and (cm i = f (a j )) and (a i = a j )
Moreover, sustainable class may be divided into two subclasses: a) Defeasible: A defeasible reaction can be deactivated, and therefore its lifetime may be controlled by the administrator or the system. Examples of this class include: blocking a machine, suspending an account, dropping traffic etc. b) Indefeasible: An indefeasible reaction cannot be deactivated, or the deactivation of such reaction requires exceptional effort or policy modification(s). Examples of this class include: deleting an account, patching an OS, patching a software, etc.

IV. POLICY-BASED RESPONSE SPECIFICATION

In [START_REF] Debar | Enabling automated threat response through the use of a dynamic security policy[END_REF], response contexts were associated with an alert signatures. This would lead inevitably toward a huge number of contexts to manage. Moreover, the activation of the context is triggered with the detection of an attack, which is surely not very effective considering the high number of failed attempts to attack a complex system. Second, the same attack may be carried out using different exploits and techniques. However, the response policy against all these attacks will be the same. Moreover, even if an attack action (or step in a larger scenario) has been detected, it may be useless to launch the associated strategic response; because the attacker will not be able to achieve his goal due to other reasons (e.g. another essential attack action is not executable on the monitored system, another response is already activated). Thus a response policy may be activated, only if the associated threat context has been activated. The latter is activated if the success likelihood of the ongoing attack [START_REF] Kanoun | Success likelihood of ongoing attacks for intrusion detection and response systems[END_REF] exceeds a predefined threshold. Now we show how to define the threat contexts, and the associated response contexts.

A. Threat Specification

First, the expert identifies the threats that may violate the system's security and operation (using for instance a preliminary risk analysis). For example, a partial or total DoS, SPIT (Spam over IP Telephony) and toll fraud are identified as potential threats in a VoIP environment. For each threat, the expert creates an associated attack objective, in order to be used by alert correlation models based on attack graphs generation [START_REF] Ning | Building attack scenarios through integration of complementary alert correlation methods[END_REF] [26] [START_REF] Cuppens | Recognizing malicious intention in an intrusion detection process[END_REF]. Usually, attack objectives are the terminal nodes in an attack graph, and they violate the security and operational policy of the monitored system. They can be formally defined, using one of the attack description languages (e.g. LAMBDA [START_REF] Cuppens | Recognizing malicious intention in an intrusion detection process[END_REF]). LAMBDA uses first-order logic predicates to model the system's state, adopting a pre/postcondition approach. For instance, DNS DoS may be caused if host is a DNS server, and host is the target of a DoS attack: -Precondition: dns server(host), target(host) -Postcondition: dns dos(host)

Finally the expert has to specify, for each attack objective, two event-based contexts:

• Start(Threat i ): This context is triggered when an ongoing threat i is detected with a high success likelihood to accomplish its attack objective. • End(Threat i ): This context is triggered when an ongoing threat i disappears. The triggering mechanisms of these two contexts will be defined in Section V-A.

B. Response Specification

The expert specifies the response rules associated with each Response i , that aims to counter and handle Threat i . Similarly, Response i will be activated and deactivated:

• Start(Response i ): This context is activated when the administrator (or the system) decides to handle and counter Threat i . In consequence, all the response rules associated to Response i will be activated and deployed in the monitored system. • End(Response i ): This context is activated when the administrator (or the system) decides to cease the response.

In consequence, all the response rules that were activated previously (via Start(Response i )) will be deactivated. The triggering mechanisms of these two contexts will be defined in Section V-B.

The expert may also add explicitly 'new' response rules that will be only activated at the end of the response. These response rules should be associated to the ¬Response i context, to express the fact that they should be only enforced when Response i is deactivated (thus when End(Response i ) is triggered). Let us suppose that α is a response context, and that β = ¬α, thus:

β = ¬α ⇒ Start(β) = End(α) End(β) = Start(α) (1)
As mentioned in Section II-A, there are three types of response rules that can be associated with any response context Response i in the Response Policy (RP): permissions, prohibitions and obligations. When End(Response i ) is activated, all the permissions and prohibitions that were previously activated by Start(Response i ), are deactivated. In other words, we do not need to specify explicitly new response rules that have an opposite 'effect' on the system [START_REF] Preda | Semantic context aware security policy deployment[END_REF]. However, the case of obligations need a deeper examination, and sometimes explicit response rule(s) must be explicitly specified.

In fact, for each obligation rule associated with Response i , we have to check first the type of its activity or action, using the taxonomy presented in Section III-A. Therefore there are three types of obligations: (i) one-shot, (ii) defeasible, and (iii) indefeasible.

First, the deactivation process of defeasible obligations is possible. The associated obligations in the context ¬Response i can be expressed by another obligation obligation(org, R, A, V, ¬Response i , Response i ); where A cancels the defeasible activity (e.g. block/allow traffic, activate/deactivate a backup server)

Proposition 3: if obligation(org, R, A, V, Response i , ¬Response i ) then obligation(org, R, A, V, ¬Response i , Response i )

We notice that obligation(org, R, A, V, Response i , ¬Response i ) holds when Start(Response i ) has been activated, and the violation context of this obligation is ¬Response i : this means that this obligation must be fulfilled before the end of response i (i.e. before the triggering of End(Response i )).

On the other hand, obligation(org, R, A, V, ¬Response i , Response i ) holds when ¬Response i is activated, while its violation context is Response i : this means that this obligation must be fulfilled before another (future) start of response i.

Second, for one-shot obligations (e.g. kill shell, close connection, restart server), the deactivation is 'implicitly' performed, due to the limited lifetime of such obligations:

Proposition 4: if obligation(org, R, A, V, Response i , ¬Response i ) then no correspondent obligation has to be associated with ¬(Response i )

Finally for indefeasible obligations, no deactivation can be done (or it cannot be specified in the Security and Operational Policy). However the administrator must review (and potentially update) the system policy POL that contains the Operational Policy OP and the Response Policy RP, to take in consideration the permanent obligations that have been activated. For example, when a server is patched, the associated threat context may need to be updated. Another example, when a malicious employee John is fired, subject John is removed from the system. We consider that, so far, these updates can not be automated.

Proposition 5: if obligation(org, R, A, V, Response i , ¬Response i )) then obligation(org, admin, review, POL, ¬Response i , Response i )

V. CONTEXT TRIGGERING FRAMEWORK

In this section, we present a model that handles the activation and deactivation of threat contexts and response contexts. Therefore, we determine for each predefined context, when it should be triggered. A risk-aware approach is adopted: we consider the impact and the Success Likelihood (SL) of the ongoing threat, and the impact of the associated response.

A. Triggering Threat Contexts

The success likelihood (SL) of an attack objective i can be calculated in real-time, considering the attack progress and the state of the system. Such model was proposed in [START_REF] Kanoun | Success likelihood of ongoing attacks for intrusion detection and response systems[END_REF]: the generated attack graph is first transformed into dynamic Markov Models. Then, the Mean Time to each Attack Objective (MTAO) is calculated using the markovian transition and sojourn matrices derived from the attack graph. Afterward, the success likelihood SL of each attack objective AO i (and thus of each Threat i ) is calculated using a logarithmic scale (See [START_REF] Kanoun | Success likelihood of ongoing attacks for intrusion detection and response systems[END_REF] for more information):

SL Threati = -20 × log 10 M T AO AOi -1 M T AO AOi (2)
A high SL means that the threat is close to achieve its objective. When the SL of Threat i , calculated in real-time, exceeds a predefined threshold, Start(Threat i ) context should be activated. The expert may tune this threshold (for example using machine learning techniques).

Proposition 6: If (SL Threati > activ ) then Start(Threat i ) is true Every threat or response has an impact on the security properties of the system (i.e. confidentiality, integrity and availability). We rely on existing assessment models, which consider the assets and services dependency in the monitored system, to evaluate the impact of the attack and the response [START_REF] Jahnke | Graph based metrics for intrusion response measures in computer networks[END_REF] and [START_REF] Kheir | Cost evaluation for intrusion response using dependency graphs[END_REF]. Therefore it is possible, for each attack objective, to calculate the variation of the confidentiality level δC, integrity level δI and availability level δA in the monitored system. For instance, [START_REF] Jahnke | Graph based metrics for intrusion response measures in computer networks[END_REF] and [START_REF] Kheir | Cost evaluation for intrusion response using dependency graphs[END_REF] model first the monitored system (or service), as a set of resources R. A resource may be a service instance or a user. The existing dependencies between all the resources in R may be specified using dependency matrices. All dependency types are considered (mandatory, alternative, combined, etc.). If one resource in the system is targeted by an attack, the direct impact on this resource will propagate to other resources through the existing dependencies (thus inducing an indirect impact). These models calculate, using Breadth First Search (BFS) algorithms, the indirect impact of a given attack on the entire system. Therefore the overall impact (which is the sum of direct and indirect impacts) on confidentiality δC, integrity δI and availability δA incurred by the entire system, can be calculated. Interested readers may refer to these paper for further details. Nevertheless, we may simply rely on experts' knowledge to assign, for each threat, static (i.e. a priori) δC, δI and δA. Thus, we may consider that δC, δI and δA for each threat, as input for our triggering framework.

The impact of an attack (or a response rule), is not constant: the longer the attack lasts (or the response is enforced), the higher is its impact. Therefore when a Threat i is detected (thus Start(Threat i ) has been activated), its Cumulative Impact CI starting from the activation time T start threat , can be calculated at any time t:

CI T hreati (t) = t T start threat (δC(u) + δI(u) + δA(u)) du (3)
On the other hand, End(Threat i ) should be activated if the SL drops below another threshold deactiv . deactiv may be equal to activ ; however there is the risk of quick switching between the activation and deactivation when the SL varies continually around activ . Therefore, it is advised to set deactiv slightly lower than activ (hysteresis effect): this guarantees a fixed delay between the activation and the deactivation.

Proposition 7: if [(Start(Threat i ) is true) and (SL Threati < deactiv )] then End(Threat i ) is true

B. Triggering Response Contexts

In this Section, we define when a policy-based response should be activated or deactivated. Therefore, we have to specify, for each response context Response i associated with Threat i , when the two contexts Start(Response i ) and End(Response i ) should be activated.

First, a Response i should be activated, when Threat i is active and the associated impact exceeds a predefined impact threshold κ min that the expert may tune. A very low κ min will cause the activation of a response context even against minor attacks which may be handled by tactical response. On the other hand, a very high κ min will turn the strategic response useless or rarely applied. A good practice is to set κ min as the deployment cost of the response policy.

Proposition 8: if [(Start(Threat i ) is true) and (CI Threati > κ min )] then Start(Response i ) is true Now, we have to evaluate the policy-based response impact on the system. Given that a policy-based response is a set of response rules, we can assess the δC, δI and δA induced by each response rule, using one of the aforementioned impact assessment models (See Section V-A). Therefore, the CI of a given security rule u, starting from the activation time T start response , can be calculated at any time t:

CI SRu (t) = t T start response (δC(u) + δI(u) + δA(u)) du (4)
For example, in a VoIP service environment, let us consider an ongoing attack that threatens the users' hardphones. A simple response may consists of two response rules:

• prohibition(client, hardph call, Internet, hardph threat resp) • permission(client, softph call, Internet, hardph threat resp)

The first rule prohibits the clients from using the hardphone, and therefore induces a sharp fall in the availability level δA rule1 < 0, while there is no impact on the confidentiality or integrity level (δC rule1 = δI rule1 = 0). The second rule permits the clients to use their softphone, therefore this response rule induces a raise in the availability level δA rule2 > 0. However, the second rule cannot fully compensate the first rule, because not all the clients have an installed softphone. It is obvious that the impact metrics δC, δI and δA are proportional to the deployed response rules, which is proportional to the number of subjects (e.g. clients) affected by the response. Moreover, δC, δI and δA depend on the type of the subjects (i.e. roles); for instance the cost incurred by a loss of confidentiality is not the same for a premium user and a normal user.

We define the overall Cumulative Impact at time t, for Response i , as the summation of cumulative impact of the response rules deployed and enforced by Start(Response i ):

CI Responsei (t) = SRu∈Responsei CI SRu (t) (5)
Finally, End(Response i ) should be launched, when the associated threat i had vanished (or its SL is negligible) or the impact of response i exceeds that of the threat i:

Proposition 9: if (Start(Response i ) is true) and [(End(Threat i ) is true) or (CI Response i (t) > CI Threati (t))] then End(Response i ) is true

VI. PROPOSED ARCHITECTURE

We propose an online architecture, to activate and deactivate policy-based response using the presented model. Figure 2 illustrates the proposed architecture: a) Online Alert Correlation: This module collects the generated alerts and correlates them, to construct the graph of ongoing threats and attacks. b) Success Likelihood Assessment: This module evaluates in real-time the success likelihood of ongoing threats, using the attack graphs generated by the Alert Correlation module. For instance, the model presented in [START_REF] Kanoun | Success likelihood of ongoing attacks for intrusion detection and response systems[END_REF] can be used. c) OrBAC Security and Response Policy: This database stores the response rules of the OP and RP, which are specified as presented in Section IV.

d) Attack Impact Assessment: This modules assesses the variations of confidentiality δC, integrity δI, and availability δA levels induced by the attack. The values may be statically defined, or measured online. For instance, the models presented in [START_REF] Jahnke | Graph based metrics for intrusion response measures in computer networks[END_REF] or [START_REF] Kheir | Cost evaluation for intrusion response using dependency graphs[END_REF] can be used.

e) Response Impact Assessment: Similarly to the previous module, this module assesses the variations of confidentiality δC, integrity δI, and availability δA levels due to the activation of a response policy.

f) Policy Instantiation Engine: This module instantiates abstract response rules (specified with roles, views and activities) into concrete rules (with subjects, objects and actions).

g) Threat Context Handler: This module activates and deactivates the threat contexts (i.e. Start(Threat i ) and End(Threat i )), and calculates the cumulative impact of the threat (See Section V-A).

h) Response Context Handler: This module activates and deactivates the response contexts Start(Response i ) and End(Response i ), and calculates the cumulative impact of the response (See Section V-B).

i) Policy Decision Point: This module selects the optimal set of PEPs in order to deploy the activated response rules. Then, the module generates the appropriate scripts to reconfigure these PEPs, in order to enforce the activation (or deactivation) of response rules in the monitored system [START_REF] Preda | Reliable process for security policy deployment[END_REF]. j) Policy Enforcement Point: These modules are reconfigured, using the scripts generated by the previous module, in order to enforce OrBAC rules, and thus to activate or to deactivate response polices in the monitored system [START_REF] Cuppens | Expression and deployment of reaction policies[END_REF], [START_REF] Cuppens | Web-Based Information Technologies and Distributed Systems[END_REF].

VII. CASE STUDY: VOIP SERVICE

We consider the VoIP service of a mid-size company with 1000 clients as a case study. SIP is used as the Signaling protocol, and the media is transported using RTP or SRTP protocols. We suppose that each client is subscribed with one of the two available account types: premium accounts (20% of clients) for business use, and normal account (80% of clients) for personal use. In normal circumstances (i.e. nominal context), premium and normal accounts are allowed to make standard or secured calls. Thus, the Operational Policy2 OP will be:

• permission(premium, call 3 , all, nominal) • permission(premium, secure call, all, nominal) • permission(normal, call, all, nominal) • permission(normal, secure call, all, nominal) First, Section VII-A shows threats identification, and the specification of one of these threats. Second, Section VII-B presents the associated response policy specification. Finally, Section VII-C presents how the latter response policy is activated and deactivated, in three different scenarios.

A. Threat Specification

First, the expert identifies the following potential attack objectives: The first attack consists of sending Spam over IP Telephony (SPIT), which definitely annoys the clients. Regular SPIT attacks with no proper response may cause the clients to change the operator. The second attack violates the confidentiality of the calls; while the third attack consist of injecting audio to an established call between two parties (and thus violates the integrity of the calls). It is obvious that the second and third attacks are not tolerable especially for the premium clients. The objective of the forth attack is to cause a partial (or total) DoS on SIP servers, and thus violates the availability of the VoIP service for all the clients. The fifth and sixth attack objectives aim a victim user whose account had been already compromised.

We decide to retain the first four attack objectives to be handled as strategic threats, and therefore we proceed to define the associated contexts. The remaining two attack objectives will be handled by the administrator with local countermeasure(s). Therefore, there is no need to specify the associated strategic responses. Due to space limitation, we will proceed with the specification of the last retained threat (i.e. Server partial Denial of Service): Threat4) and (SL Threat 4 < 4)] then End(Threat4)

• if (SL Threat 4 > 5) then Start(Threat4) • if [Start(

B. Response Specification

The expert must specify the Response Policy RP using Or-BAC, to enforce a set of response rules for each of the previous four threats. The expert may specify the same response for several threats at the same time. In this case study, we decide that the second and third threats should be associated with the same response. Due to space limitation, we will proceed with the specification of the last response policy associated to the retained threat in Section VII-A (i.e. Server partial Denial of Service).

1) Resp C : This strategic response is used when the system is under considerable (or even near total) DoS. According to this response, the system must allow only the premium clients to perform and receive calls. However, they are prohibited to perform secure calls, due to their greater resources consumption. Moreover, during these harsh conditions, normal clients are prohibited to perform or receive calls. Therefore, the response rules that must be enforced are Resp C : On the other hand, when the administrator has to end the activated response, the following rules have to be enforced in the monitored system. We notice that we do not need to explicitly specify the counterpart of permissions and prohibitions, because they are automatically deactivated when End(Resp C ) is triggered. (See Section IV-B):

• Obligation(admin, endC notify, premium, ¬RespC , RespC ) • Obligation(admin, endC notify, normal, ¬RespC , RespC )

The second and fifth rules in Resp C are defeasible obligations, and thus the counterpart rules in ¬Resp C are also defeasible obligations. Finally, the triggering conditions of these response contexts are: Figure 3 depicts the mapping between the attack objectives, the threat contexts and the response contexts. The generated attack graph is used to calculate the success likelihood of ongoing threats. Interested readers may refer to [START_REF] Kanoun | Success likelihood of ongoing attacks for intrusion detection and response systems[END_REF]. The attack graph contains elementary attack steps that lead to the pre-identified attack objectives.

• if [(Start(

C. Activating and Deactivating the Response Policy

Once the threat and response contexts are specified, they can be used by the activation/deactivation framework and architecture, as presented in Section V-B and Section VI. Let us suppose that the attacker begins to flood the SIP server using several infected machines. This attack incurs a heavy DoS for the VoIP service (85%). Therefore, the success likelihood of the attack objective Server DoS rises dramatically. The associated threat Threat 4 becomes active, and thus the associated context Start(Threat 4 ) is triggered. The impact of this threat is a decrease in the availability of the VoIP service for all clients (δA = 0; δC = δI = 0). We consider that the incurred cost for each premium user is δA = -1.5/min, while the cost for a normal user is δA = -1/min with a delay of thirty minutes. Consequently, normal users tolerate a thirty minutes service downtime, which is not acceptable for premium users.

To counter this ongoing attack, the associated response context Response 3 is activated at time T activ = 0 min (by activating Start(Response 3 )). In consequence, the remaining resources are exclusively dedicated to the premium users, while the normal users are denied of making or receiving calls. The deactivation process of Response 3 would be performed in one of the following cases:

a) The Threat Vanishes: The deactivation of Threat 4 is due to a decrease of its success likelihood. For instance, if the flooding bots are disinfected (See the attack graph in Figure 3), the success likelihood of the ongoing threat will decrease significantly (below 4), and therefore End(Threat 4 ) is activated: The evanishment of the ongoing threat leads to the deactivation of the response. b) The Threat Impact Decreases: In the second scenario the threat remains present; in other words its success likelihood does not decrease. However, its impact on the monitored system decreases: for example the DoS magnitude falls from 85% to only 20% at t = 40 min. The threat impact may decrease for several reasons, for instance:

1) The DoS level may decrease due to other tactic or strategic response(s) that has been activated by the monitored system (e.g. blocking traffic from attacker domain, activation of backup servers) 2) The DoS level may decrease due to third party actions.

For instance, another operator blocked the attacking machines after detecting the high level of outbound traffic, or upon request from the monitored system (i.e. the victim system, operator) 3) The attacker might have decided, for unknown or hidden reasons, to reduce the DoS magnitude. For instance, the attempt was undertaken in order to blackmail the monitored system. Figure 4 shows the evolution of the cumulative impact of Threat 4 and Response C over time. We can notice also a rise of the slopes of the two curves at t = 30 min, which is due to the addition of normal users' cost after their tolerance delay had expired. The cost incurred by the activated Response C becomes larger than the cost of the threat Threat 4 . Therefore, the response policy must be deactivated immediately: the associated event-based context End(Response C ) is launched at T deactiv ≈ 40min. Despite the response deactivation, the threat context Threat 4 remains active, because the threat is always present. Moreover, this ensures that Start(Resp C ) could be re-activated if the impact of Threat 4 rises again.

c) The Response Impact exceeds the Threat Impact: In the third scenario the threat remains present, and its success likelihood does not decrease. Moreover, its impact remains steady over time: the DoS level of the threat remains at 85%. Figure 5 shows that at t = 68 min, the cumulative impact of Resp C becomes higher than the one of Threat 4 . Thus, Resp C is no more effective, and End(Resp C ) is launched at T deactiv ≈ 68 min. Even though the response was deactivated, the threat context Threat 4 remains active to signal that the threat is always present.

VIII. CONCLUSION

In this paper, we presented first how to specify response requirements as response policy with associated threat and response contexts. We distinguished threat contexts from response contexts, which was not done in previous work.

The specification considers the security and response requirements at both the beginning and the end of the response. In other words, the response policy indicates how responses should be deployed when activated and deactivated, using Start(Response i ) and End(Response i ). Moreover, a temporal reaction and countermeasure taxonomy was proposed to help the expert specify the aforementioned response contexts. Second, a dynamic risk-aware framework to activate/deactivate the responses was described. The framework considers the two fundamental components of a risk: the success likelihood and the impact of the threat. Moreover, the impact of the response is also considered. Additionally, we introduced the cumulative impact metric for threats and responses, in order to assess the cumulative impact over time due to variation in confidentiality, integrity and availability levels of monitored systems and services. Third, an online architecture was proposed to activate/deactivate and deploy response policies in real-time. Finally, our work was validated using a VoIP service case study.

However, we did not consider a dynamic enforcement of response rules in the monitored system. Each response rule was statically mapped into a generic script: if a response rule is activated, the associated script is launched. [START_REF] Preda | Reliable process for security policy deployment[END_REF] shows how to enforce security rules while minimizing configuration changes and reducing resource consumption. Such model can optimize the enforcement of activated/deactivated response rules.

On the other hand, potential conflicts were handled by assigning priorities to threat and response contexts. When a conflict occurs, the rule with the highest priority is enforced. As a first approach to resolve the issue, the prioritization derived from the preliminary risk analysis (See Section IV-A) was used: the response associated with the threat with a higher risk, possesses a higher priority. Future work will focus on a risk-aware transactional management of multiple responses which may be activated/deactivated simultaneously.

Fig. 1 .

 1 Fig. 1. Temporal Response Taxonomy.

1 )

 1 SPIT (Spam over IP Telephony) Storm 2) Conversation Tapping (Internal Attack) 3) Audio Injecting -Mixing (Internal Attack) 4) Server partial Denial of Service 5) Client Toll Fraud 6) Client Account highjack

Fig. 3 .

 3 Fig. 3. The mapping between attack objectives, threat contexts and response contexts of the VoIP case study.

Fig. 4 .

 4 Fig. 4. The cumulative impact of T hreat 4 drops below the cumulative impact of Response 3 .

Fig. 5 .

 5 Fig. 5. The cumulative impact of Resp C exceeds the cumulative impact of Threat 4 .

•

  Prohibition(premium, secure call, all, RespC ) • Obligation(admin, startC notify, premium, RespC , ¬RespC ) • Prohibition(normal, call, all, RespC ) • Prohibition(normal, secure call, all, RespC ) • Obligation(admin, startC notify, normal, RespC , ¬RespC )

  Threat)4 is true) and (CI T hreat 4 > 500)] then Start(RespC ) is true • if (Start(RespC ) is true) and [(End(Threat4) is true) or (CIResp C (t) > CI T hreat 4 (t))] then End(RespC ) is true

SIP, NoE and H.323 are signaling protocols used in VoIP systems

The organization has been omitted since the case study treats a single organization

For simplicity, we consider the activities call and secure call includes making a call, and receiving a call.


S Preda

N Cuppens-Boulahia

F Cuppens

J Garcia-Alfaro

L Toutain

Model-driven Security Policy Deployment: Property Oriented Approach

We address the issue of formally validating the deployment of access control security policies. We show how the use of a formal expression of the security requirements, related to a given system, ensures the deployment of an anomaly free abstract security policy. We also describe how to develop appropriate algorithms by using a theorem proving approach with a modeling language allowing the specification of the system, of the link between the system and the policy, and of certain target security properties. The result is a set of proved algorithms that constitute the certified technique for a reliable security policy deployment.

Introduction

Security is concerned with assets protection. Securing the access to a file server, guaranteeing a certain level of protection of a network channel, executing particular counter measures when attacks are detected, are appropriate examples of security requirements for an information system. Such security requirements belong to a guide usually called the access control security policy. Deploying the policy means enforcing (i.e., configuring) those security components or mechanisms so that the system behavior is the one specified by the policy. Successfully deploying the policy depends not only on the complexity of the security requirements but also on the complexity of the system in terms of architecture and security functionalities.

Specifying, deploying and managing the access control rules of an information system are some of the major concerns of security administrators. Their task can be simplified if automatic mechanisms are provided to distribute or update, in short to deploy the policy in complex systems. A common approach is the formalization of the security policy, based on an access control model and the application of a downward process (i.e., the translation and refinement of the formal policy requirements into concrete security device configurations). Though PBNM (Policy Based Network Management) architectures (cf. [rfc 3198]) are such examples, a challenging problem persists: proving the deployment process to be correct with respect to some initial target security properties and ensuring that no ambiguities (e.g., inconsistencies [START_REF] Garcia-Alfaro | Complete Analysis of Configuration Rules to Guarantee Reliable Network Security Policies[END_REF]) are added within this process.

In this paper we aim at establishing a formal frame for the deployment of security policies in information systems. We formally prove the process of deploying a security policy related to an information system. To do so, we require [START_REF] Abou El Kalam | Organization Based Access Control[END_REF] an expressive security access control model that covers a large diversity of security requirements, (2) a modeling language for system specification and (3) a formal expression of security properties modeling the relationships between the security policy and the system it was designed for. We propose a formal technique that combines the use of access control policies expressed in the OrBAC (Organization-Based Access Control) language [START_REF] Abou El Kalam | Organization Based Access Control[END_REF] together with specifications based on the B-Method [START_REF] Abrial | The B-Book -Assigning Programs to Meanings[END_REF]. Our proposal avoids, moreover, the existence of inconsistencies derived from the deployment [START_REF] Garcia-Alfaro | Complete Analysis of Configuration Rules to Guarantee Reliable Network Security Policies[END_REF].

Paper Organization -Section 2 gives the motivation of our work and some related works. Section 3 presents the model on which we base our approach and establishes some prerequisites necessary for our proposal. Section 4 formally defines the link between a policy and a system, including the expression of some security properties. Section 5 provides a discussion upon our approach.

Motivation and Related Work

The policy-based configuration of security devices is a cumbersome task. Manual configuration is sometimes unacceptable: the security administrator's task becomes not only more difficult but also error-prone given the anomalies he/she may introduce. Guaranteeing the deployment of anomaly-free configurations in complex systems is achievable if the policy is first formalized based on an access control model and then automatically translated into packages of rules for each security device. This is the current approach in PBNM architectures where the PDP, Policy Decision Point, is the intelligent entity in the system and the PEPs, Policy Enforcement Points, enforce its decisions along with specific network protocols (e.g., Netconf [rfc 4741]). Obtaining these packages of rules (i.e., the configurations of PEPs) is the result of the downward translation process: the abstract policy, given the system architecture, is compiled through a set of algorithms at the PDP level into, for example, firewall scripts and IPsec tunnel configurations -all the way through bearing the system architecture details (interconnections and capabilities) [START_REF] Preda | A Semantic Context Aware Security Policy Deployment[END_REF].

The correctness of these algorithms is a crucial aspect since the system configuration must reflect the abstract policy. One can simply design such algorithms using imperative languages and then validate them via specific tools [START_REF] Ponsini | Rewriting of imperative programs into logical equations[END_REF]. Imperative program verification is performed in three steps: (1) the specification of a program is first formalized by some properties based on a first order logic; (2) an automatic process for analyzing the program extracts its semantics, i.e., a set of equations that define the program theory in the first order logic; (3) a proof system is finally used to prove that the program has the properties of step [START_REF] Abou El Kalam | Organization Based Access Control[END_REF] given the extracted data in step [START_REF] Abrial | The B-Book -Assigning Programs to Meanings[END_REF]. The main concerns with such approaches are: (a) the verification of these properties is realized at the end and not during the algorithm implementation; (b) it is difficult to express the interesting properties: not only those concerning the design of operations which may be seen as generic (e.g., termination of loops or lack of side effects), but also those reflecting, in our case, some network security aspects (e.g., no security anomalies are introduced during the deployment of the policies [START_REF] Garcia-Alfaro | Complete Analysis of Configuration Rules to Guarantee Reliable Network Security Policies[END_REF]). To cope with these issues, we claim that the algorithms intended for enforcing deployment of policies have to be designed with proof-based development methods, like the B-Method, to allow the expression and verification of important properties (e.g., security properties).

Formal validation or security policy deployment has already been addressed in the literature. The approaches in [START_REF] Jürjens | Model-based security analysis for mobile communications[END_REF] and [START_REF] Laborde | Implementation of a Formal Security Policy Refinement Process in WBEM Architecture[END_REF] seem to be the closest to ours. Jürjens et al. propose in [START_REF] Jürjens | Model-based security analysis for mobile communications[END_REF] to apply UMLsec [START_REF] Jürjens | Secure Systems Development with UML[END_REF] to analyze some security mechanisms enforced with respect to a security policy. UMLsec is an extension of UML which allows the expression of some security-related information in UML diagrams. Stereotypes and tags are used to formulate the security requirements. Analyzing the mechanisms means verifying whether the requirements are met by the system design. For this purpose two models are proposed: (1) a Security Requirements Model which includes architectural or behavioral system details in a prescriptive manner and (2) a Concretized Model summarizing a concrete architecture which should satisfy the security requirements. Both models appear as UMLsec diagrams. The verification is realized using the UMLsec tools which includes several plugins that uses (1) SPIN (Simple Promela Interpreter) for model-checking and (2) SPAAS (an automated theorem prover for first-order logic with equality) or Prolog as theorem provers given that some UMLsec sequence diagrams are automatically translated to first-order formulas. Applying the right plugin depends on the scenario, i.e., the architecture and the security requirements. However, the approach in [START_REF] Jürjens | Model-based security analysis for mobile communications[END_REF] presents some drawbacks. First, no abstract model is employed for modeling the policy. Second, the Concretized Model must already exist in order to automatically derive the first-order formulas to be automatically proved by SPAAS. And finally, the expressions of security properties are application-dependent: there are no generic properties dealing with the anomalies that could exist within single-or multi-component network security policies. [START_REF] Laborde | Implementation of a Formal Security Policy Refinement Process in WBEM Architecture[END_REF] a different solution to the problem of deploying security policies: the use of (1) Petri Nets as the language to specify the system and (2) CTL (Computational Tree Logic) as the language to express the security properties. Four generic system functionalities are identified and modeled as different Petri Nets which are then interconnected in order to specify the system (i.e., each security device is modeled by a Petri Net): channel (e.g., network links), transformation (IPsec and NAT), filtering (to include the firewalls) and the end-flow functionality for the hosts (the active and passive entities in the network). The Petri Nets transitions for each PEPs (here, firewalls and IPsec tunnels) are guards which actually represent the security rules to be enforced by the PEP. The policy model is RBAC-based. However, no clear downward (i.e., refinement) approach is defined and no algorithms for selecting the right PEP are described either. The model-checking verification is realized after manually deploying the policy and consequently this approach can be applied to relatively simple architectures. Besides, it is not clear whether other functionalities (e.g., intrusion detection performed by IDSs) can be taken into account with one of the four functionalities.

Laborde et al. present in

The research presented in [START_REF]D Éveloppement de Systèmes Informatiques par Raffinement des contraintes Sécuritaires[END_REF] proposes the use of Event B specifications to provide a link between the two levels of abstractions provided by the OrBAC model. As further research perspectives, the authors mentioned that their models can be reused for further developments of real infrastructures with respect to their security policy. We consider our work as a natural continuation of such a research line. As we did, the authors in [START_REF]D Éveloppement de Systèmes Informatiques par Raffinement des contraintes Sécuritaires[END_REF] chose not to address the proof of an OrBAC policy in terms of conflicts. The use of automatic tools (e.g., MotOrBAC [START_REF] Autrel | MotOrBAC 2: A security policy tool[END_REF]), allows us to assume that the policy is consistent and free of anomalies. Similarly, Coq was proposed in [START_REF] Capretta | Formal correctness of conflict detection for firewalls[END_REF] to derive OCaml algorithms for conflict detection in firewall policies. The use of Coq as a theorem prover to derive refinement algorithms can also be found in [START_REF] Unal | Theorem proving for modeling and conflict checking of authorization policies[END_REF]. The authors provide a solution to detect and remove conflicts in policies defined as tuples <permission/prohibition, subject, read/write/execute, object>. Finally, and regarding the security policy deployment domain, there exist in the literature several proposals. Some are more or less RBAC-based (e.g., proposal presented in [START_REF] Bartal | Firmato: A novel firewall management toolkit[END_REF]), others propose different languages for the high level policy definition. Although the efforts are significant [START_REF] Damianou | The ponder policy specification language[END_REF], often such languages are not generic enough [START_REF] Ioannidis | Virtual Private Services: Coordinated Policy Enforcement for Distributed Applications[END_REF], covering only some specific security applications (e.g., host firewalls, system calls management); or they do not address some key policy matters like the conflict management or the dynamic and contextual security requirements [START_REF] Casassa Mont | POWER prototype: towards integrated policy-based management[END_REF].

Model and Notation

We propose a refinement process that guarantees anomaly-free configurations ( [START_REF] Garcia-Alfaro | Complete Analysis of Configuration Rules to Guarantee Reliable Network Security Policies[END_REF]). The process derives a global policy into specific configurations for each security component in the system. Our proposal provides the set of algorithms for such a refinement process, and proves the correctness of the outgoing algorithms. We briefly justify in the sequel the choice of our formalisms. We also describe the necessary concepts to establish the link between policies and architectures.

Choice of OrBAC and B-Method

The OrBAC [START_REF] Abou El Kalam | Organization Based Access Control[END_REF] (Organization-Based Access Control) model is an extended RBAC [START_REF] Sandhu | Role-Based Access Control Models[END_REF] access control model which provides means to specify contextual security requirements. It allows the expression of a wide range of different requirements both static and contextual. OrBAC is well-known for being a robust language for defining complex administration tasks at the organizational level. Existing automatic tools (e.g., MotOrBAC [START_REF] Autrel | MotOrBAC 2: A security policy tool[END_REF]) ease, moreover, the administration of tasks using this model.

In contrast to model checking, we choose the B-Method -a theorem proving approach -for various reasons. First, the performances of theorem-proving tools are not influenced by system complexity. For example, we do not make any assumption concerning the number of nodes in the architecture. Second, the B Method eases the use of refinement paradigms. Even if B refinement does not necessarily mean an enhancement of system specifications (i.e., here it denotes the weakening of the preconditions and of the operation indeterminism towards the implementation level), there is always the possibility of keeping a B specification up to date. The B refinement allows the decomposition of system specification in layers and particular B clauses (e.g., use of SEES and IMPORTS clauses). This allows a modular system proof. New modules can be added to a B specification and existent ones may be assumed as being already proved; there is no need to totally reprove (i.e., recompute) the new specification. We therefore reuse an already proved specification. This aspect is very important as the security functionalities may be changed in a given system. Moreover, since specifying the system is an important step in our proposal, the link with the security policy must be established in a specific way. In this sense, the OrBAC philosophy considers that the security policy must be detached by functionality and by technology details at network level; and that changing the system architecture (hereinafter system or network with the same meaning) has no impact in policy definition. The same OrBAC policy may be specified for two different systems. Finally, the specification language must ensure the previous constraint: changing the security policy or the architecture should not trigger a new call for a total system proof.

We consider that the B-Method is suitable to achieve these purposes: in our approach the policy SEES the system it was designed for. The SEES clause in the B-Method makes the assumption that the seen system is already proved (i.e., the INVARIANTS of the SEEING module are being proved with the assumption that the INVARIANTS of the SEEN module are already proved). Let us notice that in our approach, we use the terminology security property as a synonym of correct deployment of a security policy in a system, meaning that it is achievable whenever certain specific security properties are verified. For instance, all network traffic between two network zones is protected if all traffic passes through an IPsec tunnel with certain parameters. If an IPsec tunnel is established and there is no IPsec tunnel anomaly [START_REF] Fu | IPSec/VPN Security Policy: Correctness, Conflict Detection and Resolution[END_REF] related to the current tunnel, the integrity security property is consequently verified. Hence, in a B specification there is the possibility of capturing such details at the INVARIANT clause level. Some security requirements are dynamic or contextual. It is sometimes necessary to add new security functionalities to the given system. For example, some firewalls are upgraded with new functionalities (e.g., temporal functionality). Taking into account all security functionalities is out of our scope. We, therefore, address only some basic functionalities such as packet filtering, IPsec tunneling and signature-based Intrusion Detection. If further functionalities are added to the specification, their semantics must be reflected in particular SETS, CONSTANTS and consequently PROPERTIES clauses; but the main deployment algorithms should remain unaffected.

Policy and System Modeling

The starting point in deploying a security policy is a set of OrBAC abstract rules. A first assumption is that the abstract policy is consistent: no OrBAC conflicting rules. This is ensured by some pertaining tools like MotOrBAC which implements the conflict resolution described in [START_REF] Cuppens | High level conflict management strategies in advanced access control models[END_REF].

The context definition may be related to a specific subject, action and object. Consequently, it is necessary to instantiate the corresponding subjects, actions and objects for each such contexts before deploying the OrBAC rules over each PEP. The abstract OrBAC rules, Permission(org, r, a, ν, c), must be brought to a concrete OrBAC expression [START_REF] Abou El Kalam | Organization Based Access Control[END_REF], Is permitted(org, s, α, o, c). Even if a large set of concrete security rules will have to be deployed, this may be the only option if the security requirements imply only such context definitions. At this point, we refer to the works in [START_REF]D Éveloppement de Systèmes Informatiques par Raffinement des contraintes Sécuritaires[END_REF] that addressed the refinement problem: the OrBAC abstract expression towards a concrete one and using the B-Method (cf. Section 2). The works in [START_REF]D Éveloppement de Systèmes Informatiques par Raffinement des contraintes Sécuritaires[END_REF] stopped at our stage, i.e., the link with the system. Therefore we will make a second assumption: the OrBAC concrete rules (i.e., Is permitted(org, s, α, o, c)) are already available and they represent the input to our deployment process. The main entities to implement our approach are described as follows. The "security policy" is defined as the set of rules over the domain (Subjects × Actions × Objects × Contexts). "Subjects" and "objects" represent active and respectively passive entities in the network. A host in a subnetwork may be modeled as a subject in contrast to a web-server which may be seen as an object; not only the hosts/network components but also the clients and servers applications may be seen as subject-object entities. The "actions" are defined as network services (e.g., http and https are actions of the same abstract activity, web). We should also include the "contexts" in which some rules are activated. These may be bound in hard with some functionalities. For example, the protected context relies on IPsec functionalities and the warning context on IDS functionality. Is permitted(s, α, o, default) is activated in the default context only if a path from s to o exists, so the firewalls on this path have to open some ports corresponding to the action α. Finally, the approach also includes all those interesting "nodes" in the network (subjects and objects) will appear as nodes in a connected graph. Those having security functionalities are the PEPs. A PEP may also be a subject or an object.

Figure 1 depicts a sample network in which an access control policy must be deployed. The system is modeled as a graph (cf. Figure 2). In real networks, each link may have a real cost or weight (e.g., an overhead required to send IP packets over the link and inversely proportional to the bandwidth of the link). A routing protocol like the OSPF, Open Shortest Path First [rfc 2328], establishes routes in choosing, for example, the shortest paths (i.e., the less expensive). We choose positive integers for the link costs and we assume that IP datagrams always follow the shortest path between two points. In such a system, the PEPs must be enforced with the right decisions corresponding to each security rule. For didactical reasons we take into account only permissions. One may choose to enforce the same rule in all PEPs having the same functionalities: this is what we call a redundancy anomaly and this is what we try to avoid. Our configuration approach is the following: for each permission, only the interesting PEPs must be identified and enforced. This leads us to consider an algorithm for selecting the interesting PEPs: the well placed PEPs for each security rule. For example, a rule in a default context takes into account only the firewalls on a certain path. In a protected context, two PEPs must configure an IPsec tunnel and all firewalls on the tunnel path must permit the establishment of the tunnel.

Regarding the warning context, the most down-stream IDS (i.e., the closest IDS to the destination) is enough and more efficient to spoofing attacks than the most up-stream IDS (i.e., the closest to the source).

We aim to formally implement this approach in B and go as far as possible towards the IMPLEMENTATION level. In this manner we will capture all interesting details for the security property enouncement. In the following sections we consider the policy at concrete OrBAC level as described above. We deal with a system where some distributed nodes have security functionalities (PEPs) and some are either active entities (subjects) or resources (objects) or both.

Policy Deployment Process: Formal Specification

Not all B machines will be carried out to an IMPLEMENTATION level: the Policy and Network (cf. Figure 4) machines should be instantiated for each scenario. The data these machines manipulate does not require highly specialized mathematical objects: only lists/sequences must be provided. But the other machines we present will have an IMPLEMENTATION structure. We describe in detail the Policy and Network (system) machines; they will be incorporated to our model development as a result of an IMPORTING machine: Deployment machine which also imports other machines necessary to our process. The Path machine will implement a tracing path algorithm necessary to select the well placed PEPs for each security rule which are then updated by the UpdatePep machine (cf. Figure 3).

Policy and Network Machines

The SUBJECTS, ACTIONS and OBJECTS will represent deferred sets but we prefer for the moment a concrete/enumerated set of CONTEXTS: default, protected, user-defined and other. The set of permissions to be deployed as well as the matching nodes-subjects, nodes-objects may be considered as CONSTANTS. They will be defined via some relations, more precisely functions. As already mentioned we prefer to bind in hard a context to a security functionality; we model this by the matching relation. Moreover, the user will be given the possibility of defining other types of context activation. For instance, a certain userdefined context may impose a hub-and-spoke tunnel configuration so the user must be able to manually indicate the hub and the spokes (nodes in the network). We model this by the context constant relation. Besides, the permissions are progressively read in the deployment process. An abstract variable is consequently necessary, the Read Permissions. All these semantics will be summed up at PROPERTIES level.

Regarding the dynamic part of the Policy machine: the Read Permissions is initialized with the empty set and some simple operations are necessary (1) to read and return a permission (read permission) and ( 2) to read the attributes (subject, object, action and context) of a permission (read data in permission). The INVARIANT is a simple one, it checks the variable type. Other inquiry operations (no read permission, no more permissions) simply return true or false.

Concerning the Network machine, we can envision the following two options. We can use an abstract machine encapsulating a node, say the Node machine. It should contain at least the node functionalities as a deferred SET. Node could be imported in our project by renaming: the project will therefore contain as many renamed Node machines as the existent ones in the real network. In the same project, a different SEEN machine will define, via a constant, the network The Project Organization A Dependency Graph is automatically obtained from a B project in Atelier B if no machine sharing rules (i.e., via SEES, IMPORTS clauses) are violated.

We deliberately do not charge the graph with the other machines necessary to the final implementation of Weighted Forest and Priority Queue. Their implementation is similar to the one in [START_REF] Fu | IPSec/VPN Security Policy: Correctness, Conflict Detection and Resolution[END_REF] and they do not reveal any important security details. topology (e.g., the nodes connections). The second option is to define a machine Network containing the topology description from the beginning. This way, we do not require other machines to carry out the network topology. Network will simply be imported only once in the project.

We choose the second solution. The Network machine models a graph: a non-empty set of Nodes, a set of Links ∈ Nodes × Nodes and a weight function binding a link to a natural number. We choose to identify each node by a natural number in the sequence 1..nn, where nn = card(Nodes). These are constants that require a refinement (i.e., valuation) at the IMPLEMENTATION level with concrete data for each different topology. The graph is undirected, so Links ∩ Links -1 = ∅. The connectedness assumption is caught by All Links * = (Nodes) × (Nodes) (where * stands for the transitive closure of relations). Each node may have security functionalities: functionality ∈ Nodes ↔ FUNCTIONALITIES (a constant relation). Some definitions are also necessary when a path is traced in the network: all links having a common node and the cost/weight of a set of links. These are the λ-functions cost and neigh nodes.

When choosing the variables of the Network machine we take into account not only the network parsing aspect but also the nodes involved in the construction of paths (shortest paths) given a source node and a destination one. We, therefore, introduce some processed nodes (PPnodes) and links variables necessary in our shortest path algorithm. The INVARIANT of the Network machine acts on the variables type. We follow a generous style in specifying the operations: almost each operation has some preconditions. The generous style, in contrast to the defensive style which considers some internal operation tests (e.g., IF, SELECT substitutions), is more in the spirit of a B specification ( [START_REF] Abrial | The B-Book -Assigning Programs to Meanings[END_REF]) as it demands prior design and specification. Such operations may be called from somewhere else (i.e., operations of other machines) and their preconditions must be verified; otherwise, they may not terminate.

Policy SEES Network (cf. Figure 4). Although the constants of Network may appear in the operations of a SEEING machine (e.g., Policy) its variables may be read-only. No operation of a SEEN machine can be called from within a SEEING machine. Therefore, Network is not aware of the fact that it is seen. Even if there are specific proof-obligations generated as a result of a SEES clause ( [START_REF] Abrial | The B-Book -Assigning Programs to Meanings[END_REF]), the invariants of the SEEN machine are considered already proved. If we change the Policy for the same Network, the latter is once and independently proved. A SEEN machine, and consequently Network, may be imported only once somewhere in the project. We pay attention and we import Network only in a machine that really necessitates more than read-only variable references. This is illustrated in Figure 3.

A Tracing Path Algorithm

The role of a tracing path algorithm in our development is to find the security devices that must enforce each policy rule. These security devices must have the right functionalities and must be well placed in the network. If the right functionalities are indirectly designated by the OrBAC contexts (i.e., default -Preda, Cuppens-Boulahia, Cuppens, Garcia-Alfaro, Toutain firewall, protected -IPsec and firewalls, warning -IDS), finding the well placed device in the network is not obvious. Nevertheless things are getting simpler if we consider that IP packets follow the shortest path in the network. One could say this is a severe assumption, but conciliating a given routing policy with our deployment process is a simpler matter: it suffices to take into account the few hops a route may involve. Therefore, we use Dijkstra's shortest path algorithm. Implementing such an algorithm in imperative languages is not too difficult but it is not obvious using the B-Method. There are already B algorithms for deriving spanning trees, [START_REF] Fraer | Minimum Spanning Tree[END_REF], [START_REF] Abrial | Formal Derivation of Spanning Trees Algorithms[END_REF], but none for shortest-path trees. We base our path derivation algorithm on the works in [START_REF] Fraer | Minimum Spanning Tree[END_REF]; we could not totally reuse their method: the shortest path may not go along the minimum spanning tree. Moreover, shortest-path tree changes as a result of choosing different source and destination nodes. Some implementation details in [START_REF] Fraer | Minimum Spanning Tree[END_REF] concerning the priority-queues turned out to be extremely useful: we reused them although the lists would have been much easier to manipulate. However, we mention that the project in [START_REF] Fraer | Minimum Spanning Tree[END_REF] violates a sharing rule: a SEEN machine must be imported once but IMPORTS must not introduce loops in the project. We believe their error is due to their prover which did not check on machine sharing rules.

Path Machine, Weighted Forest, Min Weight Link: Path machine SEES Network whose constants (Nodes, Links and weight) are used. We need a definition of a path in the network. But as a pre-requisite we have to formalize the notion of a tree, more precisely of a spanning-tree: a forest with (n -1) links, where n = card(Nodes) and a forest is a cycle-free set of links. We also need a definition of the set of paths from a source node to a destination node: all (i.e., the union of) adjacent links with the source and destination as extremity nodes. We are therefore interested in selecting the less-expensive path in this set of paths. This will represent the shortest path which will be simply selected once the shortest-path tree is generated (shortest path tree). In what follows we introduce only some specific B details we faced when designing Path machine and its implementation (the termination of the shortest path tree operation is ensured by our assumption of a connected graph).

Implementing the Path machine with the previous specifications would be difficult. The IMPLEMENTATION will therefore import two machines: Min Weight-Link machine, to find the minimum link weight in a set of links adjacent to some processed nodes (Dijsktra's algorithm) and Weighted Forest machine, to build the tree as a union of links. The tree is noted LL which is an abstract variable of Weighted Forest. LL finally represents the shortest-path-tree. Due to space limitations we do not go further with our algorithm. The complete implementation of Weighted Forest and Min Weight Link has several hundreds of B code lines. We mention only that we used the Abstract Constants clause in order to avoid the error in [START_REF] Fraer | Minimum Spanning Tree[END_REF] regarding the SEES and IMPORTS clauses: if an abstraction SEES a machine, all the further refinements must also SEES this machine and the final IMPLEMENTATION cannot IMPORTS the seen machine.

Deployment Implementation and Security Properties

The root machine of our model is the Deployment machine (cf. Figure 5). Its abstract specification is quite simple: there is only a Boolean concrete variable, deployment ok modified by an operation, deploy. The refinement of this operation is based on other operations of the IMPORTED machines Policy, Path and Up-datePep. Network is imported in our model indirectly, via the Path machine. By using the IMPORTS clause, allowed only from within an IMPLEMENTATION there are specific obligation-proofs generated for the IMPORTING machine. We deliberately leave the IF substitution unfinished: there are tests concerning the existence of a path in the network according to the type of context. Therefore, exists path, a boolean variable of the Path machine, is valued in function of several other variables: the security functionalities of the source and destination nodes (e.g., the IPv6 protocol incorporates the IPsec suite but this functionality may not be considered in the IPsec tunnel extremities), the security functionalities in their neighborhood (e.g., for IDS rules) or the security functionalities of the whole path (path set) between the source and the destination. These tests are simple and rely on the definition and implementation of the Path machine. Finally, the UpdatePep machine stores, for each PEP, the security configuration as a set of rules {sub → act → obj → ctx} modified via the update pep operation. The concrete deployment ok variable respects the data types required in an IMPLEMENTATION. It needed no further refinement and we defined it as a CONCRETE VARIABLE in the abstraction.

Security Properties

A security property is generally expressed at a more abstract level than the security requirements. A security property may rely on the correct enforcement of several security requirements. Moreover, a property may still not be verified after the deployment of all security rules. Often, a property violation is the result of anomalies in deploying the policy. Our refinement approach is a property-aware one: the target properties determine the enforcement of the security devices. In the implementation of the Deployment machine (cf. Figure 5), we denote by P 1 -P 8 some of the most interesting application-independent properties the policy deployment process should verify. We do not claim to achieve a thorough analysis of security properties: some may be enounced at higher levels ( [START_REF] Benaissa | Integration of Security Policy into System Modeling[END_REF]) and some may be identified from specific security requirements ( [START_REF] Jürjens | Model-based security analysis for mobile communications[END_REF]).

-Completeness: Captured by INVARIANT P 1 , this property states that if the network path from a subject to an object is correctly computed (i.e., it exists and the security devices belonging to this path have the right functionalities with respect to the context) the security rule may and will be deployed.

-Accessibility (and Inaccessibility): Property P 6 states that for each permission rule, a subject is able to access an object with respect to the policy. Thus, there must be a path between the subject and the object network entities and if this path involves some firewalls, they must all permit the action the subject is supposed to realize on the object. In this manner, the default context is activated (this may be seen as a minimal context). However, P 6 must be seen as a partial accessibility property: it is verified at each WHILE loop iteration, i.e., it does not take into account all deployed rules. In order to guarantee the global accessibility, P 3 relies on the correct deployment of all permissions. We simplified the notation: given that the operation shortest path(src, dest) returns a set of links called path set, we should have written: node ∈ path set. In P 3 we use config which is defined in the UpdatePep machine: config ∈ Nodes↔PERMISSIONS and config [{ni}], the image of the {ni} set under config, is the set of rules already deployed over the node ni.

Following the same reasoning we can also enounce the global inaccessibility property, P 4 : there should be no open path from the subject to the object. The path variable is given in the Path machine and regroups a set of links from a source node to a destination one.

-All traffics are regulated by firewalls: Property P 7 is also interesting when there is a new context called logging: this context is managed by those devices with a logging functionality as today's most popular firewalls.

-Integrity and confidentiality property: This property is related to the establishment of IPsec tunnels. It ensures the extremities of the IPsec tunnel. Moreover, particular IPsec configurations may include recursive encapsulation of traffic on a path. Verifying this property begins at higher levels: if no OrBAC security rule is enounced with a protected (prot) context, no further verification is necessary. To ensure the protected context activation, a configuration of an IPsec tunnel is necessary. If no specific information concerning the IPsec tunnel establishment is provided, we may suppose the following two cases: (1) the subject/source and the object/destination are IPsec enabled (e.g., IPv6 nodes and end-to-end tunnel) or (2) at least one node in their neighborhood (e.g., site-to-site tunnel) has IPsec functionalities. For the first case, it suffices to check on the IPsec functionalities on both the subject and the object nodes and this is captured by the P 8 property of the WHILE loop. The second case is handled as follows: in one of the IMPORTED machines on the Weighted Forest development branch, we provide an operation predec(node) which returns the precedent node in the current shortest-path from the source (src) node to the destination (dest) node. Via PROMOTE clauses, the operation may be called by higher IM-PORTING machines, including the Deployment machine. We consequently check on the predec(dest) and predec -1 (src) nodes as in the P 8 formula.

There is a further case that cannot be addressed at the WHILE loop IN-VARIANT level (i.e., after each iteration) because it relies on the correct enforcement of all IPsec tunnels in the network. Figure 6 shows an example of successive encapsulations on a site-to-site topology. It may result in violating the confidentiality property. It also shows an example where the source-destination traffic is twice encapsulated: by n1 (IPsec tunnel mode between n1 and n2) and by n3 (between n3 and n4). The configurations of n2 and n3 neighbor nodes include a security rule in a default context (i.e., {sub →act →obj →default}) allowing the IP traffic to pass the section n2-n3 with no encapsulation: the confidentiality is not preserved in this topology (i.e., between n1 and n4). Such an anomaly is the result of deploying separately the IPsec tunnels and consequently it cannot be controlled by the WHILE INVARIANT after each iteration. Nevertheless, the main INVARI-ANT of the Deployment machine is not reproved during these iterations but after the loop termination and consequently the IPsec anomaly can be dealt with only at this level. The P 2 formula, in logical conjunction with the completeness property, accomplishes the integrity and confidentiality property. -Authentication: P 5 is interesting if we deal with an authentication context: an action that cannot be applied in a certain context unless an authentication process is achieved. We can verify these cases by providing a variable that records the actions realized by the subject concerned with the authentication. We, therefore, impose a workflow constraint (history[{sub}] is the set of actions that sub realized, with history ∈ SUBJECTS ↔ ACTIONS ).

Discussion

The B project depicted in this paper was realized using Atelier B v4.0. Validating a B project consists in proving the Proof Obligations (POs) automatically generated after analyzing and type-checking the entire project. The functional correctness of each machine is validated separately with respect to the specific B inter-machine clauses (SEES, IMPORTS, etc.). The current project was validated with the assumption of a conflict-free OrBAC policy and of a correct system architecture: no lack of security functionalities in the security components placed on the shortest-paths. This leads us to conclude that the outgoing algorithms are correct with respect to the security properties we considered. The number of POs automatically generated for each machine varied based on the operational complexity: from 2 for the Policy machine which involved very simple operations to 272 for the Min Weight Link implementation; for the latter one, 110 POs were automatically discharged, the rest being interactively proved. The choice of the OrBAC model and of the B-Method was motivated by the type of applications that we address in this paper: the deployment of access control security policies. However, our work shows some limitations. On the one hand, our approach focuses on the deployment of policies in systems with an already existing set of security devices. The appropriate deployment of the access control policy is closely related to the interconnections and the capabilities of these security devices. As we avoid the intra-and inter-component anomalies ( [START_REF] Garcia-Alfaro | Complete Analysis of Configuration Rules to Guarantee Reliable Network Security Policies[END_REF]), there may be unaccomplished security requirements because of a deficient security device capability. Thus, an improvement to our approach would be to find, for a given system and a given security policy, the best security architecture so that all security requirements be met. On the other hand, the type of security requirements may also induce a limitation to our approach. As long as we consider only access control requirements, the B-Method is very efficient. However, temporal logic specifications cannot be addressed with the B Method. Therefore, except for the specific case of authentication, the security requirements involving a trace-like modeling (an ordered set of actions to be realized by a subject on an object) cannot be addressed with the B Method. The authentication can be dealt with since the subject needs to accomplish a single (previous) action (modeled by a provisional -history -OrBAC context) before gaining the access.

Conclusions

The configuration of security devices is a complex task. A wrong configuration leads to weak security policies, easy to bypass by unauthorized entities. The existence of reliable automatic tools can assist security officers to manage such a cumbersome task. In this paper, we established a formal frame for developing such tools. Our proposal allows the administrator to formally specify security requirements by using an expressive access control model based on OrBAC [START_REF] Abou El Kalam | Organization Based Access Control[END_REF]. A tool which is proved using the B-Method may therefore implement the so-called downward process: the set of algorithms realizing the translation of an OrBAC set of rules into specific devices configurations. Not only the job of administrators is simplified, but they know for certain what security properties are verified at the end.

Fig. 1 .

 1 Fig. 1. The Real Architecture. Fig. 2. The Corresponding Graph.

Fig. 3 .

 3 Fig. 3. Dependency Graph.

Fig. 4 .

 4 Fig. 4. Policy and Network Machines.

Fig. 5 .

 5 Fig. 5. Deployment Implementation.

Fig. 6 .

 6 Fig. 6. Chained IPsec Tunnels.

Preda, Cuppens-Boulahia, Cuppens, Garcia-Alfaro, Toutain

Acknowledgments -This work has been supported by a grant from the Brittany region of France and by the following projects: POLUX ANR-06-SETIN-012, SEC6 Project, TSI2007-65406-C03-03 E-AEGIS, and CONSOLIDER CSD2007-00004 "ARES".