Najah Ben Said

Takoua Abdellatif

Saddek Bensalem

Marius Bozga

A Robust Framework for Securing Composed Web Services

Keywords: component-based systems, information flow security, non-interference, dependency flow graph, automated verification

This paper proposes a framework that automatically checks and configures data security in Web Services starting from high level business requirements. We consider BPEL-based composed Web Services. BPEL processes and initial security parameters are represented as component-based models labeled with security annotations. These models are formal and enable automated analysis and synthesis of security configurations, under the guidance of the service designer. The security property considered is the non-interference. The overall approach is practical since security is defined separately from functional processes and automatically verified. We illustrate its utility to solve intricate security problems using a smart grid application.

Introduction

With the expansion of Web Services (WS) [START_REF] Walsh | UDDI, SOAP, and WSDL: The Web Services Specification Reference Book[END_REF] deployed on the enterprise servers, cloud infrastructures and mobile devices, Web Service composition is currently a widely used technique to build complex Internet and enterprise applications. Orchestration languages like BPEL [START_REF] Juric | Business Process Execution Language for Web Services BPEL and BPEL4WS 2nd Edition[END_REF] allow rapidly developing composed WS by defining a set of activities binding sophisticated services. Nevertheless, advanced security skills and tools are required to ensure critical information security. Indeed, it is important to track data flow and prevent illicit data access by unauthorized services and networks; this task can be challenging when the service is complex or when the composition is hierarchical (the service is composition of composed services and atomic services). For example, a classical travel organization WS has to keep a client's destination secret as messages are exchanged between different services like travel agency services and the payment service. Each piece of information depending on the destination, like ticket price, can lead to the secret disclosure if it is not protected. WS security standards [START_REF] Damiani | Securing SOAP e-services[END_REF][START_REF] Della-Libera | Web services security policy language (WS-SECURITYPOLICY)[END_REF] provide information flow security solutions for point-to-point inter-service communication but fall short in ensuring end-to-end information flow security in composed services. Furthermore, the BPEL language does not state any rules on how to properly apply security mechanisms to services. Generally, developers manually set up their system security configuration parameters which can be tedious and error-prone. Information flow control, particularly the non-interference [START_REF] Goguen | Security policies and security models[END_REF] property check, is an alternative, more robust, approach than applying access control for point to point communication. Indeed, it allows tracking information propagation in the entire system and prevents secret or confidential information from being publicly released. Information flow control relies on annotating system data with specific levels of security and uses specific methods for checking non-interference, that is, absence of leakage between different levels. Nonetheless, providing annotations and establishing their correctness are equally difficult, especially for distributed implementations, where only code is available and no higher-level abstractions exist to give a better view and easier way of correction.

In this paper, we propose a robust tool assisting a designer ensuring endto-end information flow security in WS composition. Figure 1 shows a workflow overview of this tool. The service designer describes in BPEL his process and defines partial security constraints in a configuration file. The constraints are expressed as authorization rights, that is, a list of services owners and authorized readers for a subset of critical data. The BPEL process and the configuration information are then automatically transformed into a component-based framework. This framework was first adapted to abstract distributed WS orchestration to a component-based model where all Web services are transformed into atomic components communicating through interactions by sending and receiving variables and second, to synthesize security configuration for total system variables with respect to security constraints by considering all implicit and explicit data dependencies in the system. The calculated configuration is optimal that is only data that need to be protected is configured as critical and its security level is minimal. It is indeed, very important to reduce the security processing overhead like cryptography encryption and decryption, signature calculation, certificate verification, etc. In case a total configuration file is generated by the tool, the system information flow is then considered non-interferent with respect to initially defined configuration. Otherwise, the system is interferent and system designer has to re-define the input initial configuration. As a security advisor, automated configuration synthesis allows designers, developers and administrators to focus on functional constraints and be confident that their secret data is protected and people privacy respected. The proposed framework is based on a formal compositional security model. It is implemented and tested on a smart grid application. This application shows the practical usage of our tool since only basic security skills are required and WS standards are respected.

The paper is structured as follows. Section 2 presents the functional and security aspects of the adopted component-based framework. In Section 3, we present a practical compositional approach to synthesize security configurations in component-based system models. In Section 4, we apply this approach to Web Service orchestration. We consider a transformation from BPEL orchestration language to the component-based framework and we present the adopted security annotation model and the tool implementation. In Section 5, we provide a usecase as illustrative example. Finally, Section 6 discusses the related work and Section 7 concludes and presents some lines for future work.

Component-Based Model

In the scope of this work, we consider systems composed of atomic components interacting through point-to-point communications. Atomic components are in form of finite automata extended with data. Communication is synchronous and directed between one sender and one receiving component. Regarding security, we consider transitive information flow policies expressed on system variables and we focus on non-interference properties.

The proposed model is general enough to deal with information flow security from a practical point of view for commonly used programming languages and/or modeling frameworks such as BPEL. Nevertheless, it should be mentioned that this model is actually a strict subset of the secureBIP component model previously introduced in [START_REF] Ben Said | Model-driven Information Flow Security for Component-Based Systems[END_REF][START_REF] Ben Said | Model-driven information flow security for component-based systems[END_REF]. The latter considers additional coordination mechanisms through multiparty interactions as well as different definitions of non-interference. For the sake of readability we recall hereafter the key concepts and we re-formulate the key results which are useful in our precise context, on the restricted subset considered.

Preliminaries

Let D = {D j } j∈J be a universal set of data domains (or data types) including the Boolean domain D Bool = {true, false}. Let Expr be an universal set of operators, that is, functions of the form op : × m i=1 D ji → D j0 , where m ≥ 0, D ji ∈ D for all i = 0, m. We consider typed variables x : D where x denotes the name of the variable and D d om(x) ∈ D its domain of values. We define expressions e as either (i) constant values u ∈ ∪ j D j , (ii) variables x : D or (iii) composed expressions op(e 1 , ..., e m ) constructed by applying operators op on sub-expressions e 1 , ..., e m such that, their number and their domains match exactly the domain of op. We denote by use(e) the set of variables occurring in expression e and by Expr[X] the set of expressions constructed from a set of variables X and operators in Expr. We denote by Asgn[X] the set of assignments to variables in X, that is, any subset {(x i , e i )} i∈I ⊆ X × Expr[X] where (x i ) i∈I are all distinct. An assignment (x, e) is denoted by x := e.

Given a set of variables X, we define valuations V of X as functions V : X → ∪ j∈J D j which assign values to variables, such that moreover, V (x) ∈ d om(x), for all x ∈ X. We denote by V [u/x] the valuation where variable x has assigned value u and any other variable has assigned the same values as in V . For a subset Y ⊆ X, we denote by V |Y the restriction of V to variables in Y .

Given an expression e ∈ Expr[X] and a valuation V on X we denote by e(V ) the value obtained by evaluating the expression according to values of X on the valuation V . Moreover, given an assignment a ∈ Asgn[X] and a valuation V of X we denote by a(V ) the new valuation V obtained by executing a on V , formally V (x) = e(V ) iff x := e ∈ a and V (x) = V (x) otherwise.

Operational Model

An atomic component B is a tuple (Q, P, X, T ) where Q is a set of states, X is a set of local variables, P is a set of ports (or action names) and T is a set of transitions. We distinguish respectively input ports P in ⊆ P and output ports P out ⊆ P and we assume they are disjoint, P in ∩ P out = ∅. Every input or output port p ∈ P in ∪ P out is associated to a unique variable v ar(p) ∈ X. Every transition t ∈ T is a tuple (q, p, g, a, q ) where q src(t), q d st(t) ∈ Q are respectively the source and the target states, p port(t) ∈ P is a port, g guard(t) ∈ Expr[X] is the enabling condition and a asgn(t) ∈ Asgn[X] is the assignment of t.

In our model, atomic components have exclusive access on their variables. Interactions between components take place only through explicit input/output binary connectors. A connector defines a static communication channel from one output port p out of a sender component B to an input port p in in a receiver component B = B. The connector is denoted by the tuple (p out , p in ). Intuitively, when communication takes place, the value of v ar(p out ) is assigned to v ar(p in ).

Figure 2 provides examples of atomic components. The Producer component contains two states l 1 and l 2 and one output port out. The transition labelled with port produce takes place only if the guard [w ≤ 3] is true. Then, the variable x is updated by executing the assignment x := 3x + 1.

We denote by Γ (B 1 , ..., B n ) the composition of a set of atomic components B i = (Q i , X i , P i , T i ) i=1,n through a set of connectors Γ . For the sake of simplicity, we tacitly assume that every input and output port of every B i is used in exactly one connector in Γ . The operational semantics of a composition is defined as a labelled transition system (Q, A, -→) where states correspond to system configurations and transitions to internal steps or communication through connectors. A system configuration q, V in Q where q = (q 1 , ..., q n ),

V = (V 1 , ..., V n ) is obtained from component configurations (q i , V i ) where q i ∈ Q i and V i is a prod_buffer_cons.pstex l2 l1 l4 l5 x:=0 [w ≤ 3] z:=0 produce u:=0 t:=1 w:=0 consume in y:=0 l 3 in out out out in in u:=z-t out x:=3x+1 x y y z
Fig. 2. A Producer-Buffer-Consumer example valuation of X i , for all i = 1, n. The set of labels A is defined as Γ ∪ {τ }, that is, either communication on connectors or internal action (τ ). The set of transitions -→⊆ Q × A × Q between configurations are defined by the following two rules:

Inter (q i , p i , g i , a i , q i ) ∈ T i p i ∈ P in i ∪ P out i g i (V i ) = true V i = a i (V i ) ∀k = i. (q k , V k ) = (q k , V k ) (q 1 , ..., q n ), (V 1 , ..., V n ) τ -→ (q 1 , ..., q n ), (V 1 , ..., V n ) Comm (p out i , p in j ) ∈ Γ (q i , p out i , g i , a i , q i ) ∈ T i (q j , p in j , g j , a j , q j ) ∈ T j g i (V i ) = g j (V j ) = true u = V i (v ar(p out i )) V i = a i (V i ) V j = a j (V j [u/v ar(p in j )]) ∀k = i, j. (q k , V k ) = (q k , V k ) (q 1 , ..., q n ), (V 1 , ..., V n ) p out i p in j -----→ (q 1 , ..., q n ), (V 1 , ..., V n )
The system evolves either by performing asynchronously an internal step of some component B i (Inter rule) or by performing a synchronous communication between two components B i , B j involving respectively ports p out i , p in j related by a connector in Γ (Comm rule). Transitions are executed only if guards are evaluated to true in the current configuration. As usual, next configurations are obtained by taking into account variable assignments and communication.

A run ρ of the system

Γ (B 1 , ..., B n ) is a finite sequence q 0 , V 0 α 1 q 1 , V 1 α 2 ... α q , V where q k-1 , V k-1 α k --→ q k , V k for all k = 1, .
The set of all runs starting from a configuration q 0 , V 0 are denoted by Runs q 0 , V 0 .

Finally, for a run ρ and a subset of variables Y ⊆ ∪ n i=1 X i we denote by tr(ρ, Y ) the trace of ρ with respect to Y . Traces represent what is actually observable from a trace by having access to variables in Y . They are inductively defined for runs as follows:

tr( q, V , Y ) = q, V |Y tr( q, V ) α ρ , Y ) =        tr(ρ , Y ) if α = τ and tr(ρ , Y ) starts with q, V |Y q, V |Y α tr(ρ , Y ) otherwise where V |Y denotes (V 1|Y1 , ..., V n|Yn ) for Y i = Y ∩ X i , for all i = 1, n.
Finally, for a trace tr(ρ, Y ) we define the set E nable(tr(ρ, Y )) of configurations which are enabling the same trace on alternative runs, formally:

E nable(tr(ρ, Y )) = { q 0 , V 0 | ∃ρ ∈ Runs q 0 , V 0 , tr(ρ, Y ) = tr(ρ , Y ) } 2.

Security Model

We consider transitive information flow policies expressed on system variables and we focus on the non-interference properties. We restrict ourselves to confidentiality and we ensure that no illegal flow of information exists between variables having incompatible security levels. Formally, we represent security domains as finite lattices (S, ≤) where S denotes the security levels and ≤ the flows to relation. For a level s, we denote by [-, s] (resp. by [s, -]) the set of levels allowed to flow into (resp. from) s. Moreover, for any subset S ⊆ S, we denote by S (resp. S) the unique least upper (resp. greatest lower) bound of S according to ≤.

Let Γ (B 1 , ..., B n ) be a system and let X = ∪ n i=1 X i (resp. P = ∪ n i=1 P i ) be the set of all components variables (resp. ports). A security annotation on variables is a function σ : X → S which associates security levels to variables. We denote by

σ -1 : 2 S → 2 X the pre-image of σ, defined as σ -1 (S) = {x ∈ X | σ(x) ∈ S}, for all S ⊆ S. For any s, define Y s = σ -1 ([-, s]
), the set of variables having security levels at most s. For a security level s, we denote by ≈ s the indistinguishability relation on configurations at level s defined by q 1 , V 1 ≈ s q 2 , V 2 iff q 1 = q 2 and V 1|Ys = V 2|Ys . That is, configurations are identical on control states and up to variables with security levels at most s. For a set of configurations C ⊆ Q, we denote by

[[C]] s = {c ∈ Q | ∃c ∈ C. c ≈ s c}.
We are now ready to define the security criterion for an annotated system. Definition 1. A security annotation σ is secure for a system Γ (B 1 , ..., B n ) and initial configurations Init iff ∀s ∈ S. ∀ q 0 , V 0 ∈ Init. ∀ρ ∈ Runs q 0 , V 0

E nable(tr(ρ, Y s )) = [[E nable(tr(ρ, Y s ))]] s
Intuitively, the definition states that for any security level s, no additional information is obtained by observing traces with respect to variables Y s behind the equivalence ≈ s . Or, any two indistinguishable initial states enable precisely the same set of traces with respect to Y s . If this would not be the case for let say, (q 0 , V 0 ) ≈ s (q 0 , V 0 ), then one could find a run ρ 0 ∈ Runs q 0 , V 0 such that no run ρ ∈ Runs q 0 , V 0 had the same trace with respect to Y s . But then, this means (q

0 , V 0 ) ∈ E nable(tr(ρ 0 , Y s )) whereas (q 0 , V 0 ) ∈ E nable(tr(ρ 0 , Y s )). and consequently E nable(tr(ρ, Y s )) [[E nable(tr(ρ, Y s ))]] s .
The following proposition defines static conditions ensuring that a security annotation on variables is secure for a system.

Configuration Synthesis

The configuration synthesis problem is defined as follows. Given a partial security annotation of a system, extend it towards a complete annotation which is provable secure according to Proposition 1, or show that no such annotation actually exists. We assume that system components are port deterministic. We rely on flow dependency graphs as an intermediate artifact for solving this problem. For every component B i = (Q i , X i , P i , T i ), we define the flow dependency graph G i = (N i , → i ) where the set of vertices N i = X i ∪ P i contains the ports and variables of B i and edges → i ⊆ N i × N i correspond to flow dependencies required by Proposition 1 and are defined below, for every x, y ∈ X i , p, r ∈ P i :

y → i x iff ∃t ∈ T i . x := e ∈ asgn(t), y ∈ use(e) ∪ use(guard(t)) p → i x iff ∃t ∈ T i . x := e ∈ asgn(t), p = port(t) p ∈ P in i , x = v ar(p) y → i p iff ∃t ∈ T i . y ∈ use(guard(t)), p = port(t) p ∈ P out i , y = var(p) p → i r iff ∃t, t ∈ T i . p = port(t), r = port(t ), (d st(t) = src(t ) ∨ src(t) = src(t ))
Using flow dependency graphs, the configuration synthesis problem is formally rephrased as follows:

-Given system Γ (B 1 , ..., B n ), partial annotation σ 0 : X → S ∪ {⊥} -Find complete annotation ζ : X ∪ P → S such that (C1) (initial annotation) ∀x ∈ X. σ 0 (x) = ⊥ =⇒ ζ(x) = σ 0 (x) (C2) (flow preservation) ∀i = 1, n. ∀x, y ∈ P i ∪ X i . x → i y =⇒ ζ(x)≤ζ(y) (C3) (connector consistency) ∀γ = (p out p in ) ∈ Γ. ζ(p out ) = ζ(p in )
If a complete annotation ζ exists and satisfies the conditions (C1-C3) above, then the system Γ (B 1 , ..., B n ) is provable secure for σ = ζ |X and ς = ζ |P , which are respectively the projections of ζ to variables X and ports P . That is, all conditions required by Proposition 1 on annotation of ports and variables within components are captured by dependency graphs (G i ) i=1,n and satisfied according to (C2). Connectors are consistently annotated according to (C3). Moreover, the initial annotation is preserved by (C1).

An iterative algorithm to compute the complete annotation ζ is depicted as Algorithm 1 below. If the algorithm terminates without detecting inconsistencies, then ζ is the less restrictive annotation satisfying conditions (C1-C3). If an inconsistency is detected, then no solution exists. In this case, the initial annotation is inconsistent with respect to the information flow within the system. Initially, all system variables are either annotated by security levels given from system designer σ 0 if it exist or a default level that correspond to the lowest security level ( S) in the lattice (line 1). The algorithm visits iteratively all components (lines 2-18). For every component B i , it propagates forward the current annotation ζ within the flow graph G i (lines 3-13). The security level ζ(n i ) of every node n i is eventually increased to become more restrictive than the levels of its predecessors (lines 8-13). An inconsistency is reported if the security level increases for an initially annotated variable (lines 10-11). Any change triggers recomputation of successors nodes of n i (lines 12-13). Finally, once the annotation within G i is computed, any change on security levels on input/output ports is propagated to connected ports (lines [START_REF] Corporation | Using BPEL processes in WebSphere Business Integration Server Foundation[END_REF][15][START_REF] Tatsubori | Best-practice patterns and tool support for configuring secure web services messaging[END_REF][START_REF] Busi | A survey on non-interference with petri nets[END_REF][START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF]. After this propagation step, any pair of connected ports has again the same security level. As for variables, notice that annotations for connected ports can only increase: any increase due to propagation within a component is immediately propagated to the connected port. The involved components need to be revisited again (line 18). Notice that both while loops are guaranteed to terminate as the number of annotation changes is bounded for every node. That is, the security level can only be increased finitely many times in a bounded lattice (S, ≤). Proposition 2. Algorithm 1 solves the configuration synthesis problem.

Algorithm 1: Annotation Synthesis 1 ζ(n) ← σ0(n) if n ∈ X, σ0(n) = ⊥ S otherwise initialization 2 BList ← {Bi}i=1,n inter-component outer loop 3 while BList = ∅ do
Proof. Initially, the annotation ζ is defined to satisfy initial annotation condition (C1). It equally satisfies connector consistency (C3) but not necessarily flow preservation (C2). The algorithm propagates this annotation along the flow graphs, without changing the initially annotated variables. Intra-component propagation makes flow preservation (C2) hold for the component but may actually destroy (C3). On the contrary, the propagation across connectors re-establish (C3) but may destroy (C2) for connected components. At termination, no annotation changes are possible/needed, hence, the final annotation ζ satisfies both flow preservation condition (C2) but and connector consistency (C3).

As an example, we apply Algorithm 1 to the Producer-Buffer-Consumer presented in Figure 2 with initial annotation {x → M, z → H}, for security levels L(ow), M (edium) and H(igh), such that L≤M ≤H. The three flow dependency graphs and their dependencies through connectors are depicted in Figure 3. For this initial labelling, the algorithm succeeds to generate a complete annotation for variables {x → M, w → L, y → M, z → H, t → L, u → H} and all ports are mapped to M . If however we add to the initial configuration a label to the guard variable w, {w → H}, Algorithm 1 detects an inconsistency at the Producer component and an illicit flow from the w variable to y variable through port produce is reported to the user. In this section, we apply the synthesis approach to generate secure configurations of WS applications. We consider a composition of BPEL and elementary services annotated using the decentralized label security model (DLM) [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF]. We briefly present how such WS compositions are represented in the componentbased model and we show how the DLM annotations are used in the BPEL context.

The BPEL Composition

BPEL provides structuring mechanisms to compose several WS into a new one. We particularly focus on BPEL4WS [START_REF] Andrews | BPEL4WS, Business Process Execution Language for Web Services Version 1[END_REF] processes which compose services from activities, that are either (1) basic such as receive, reply, invoke, assign, throw, exist, or (2) structured such as sequence, if, while, repeatuntil, pick, flow. The representation of BPEL processes in our component model is structural, that is, the structure of the source BPEL model is preserved in the target model. More precisely, a process is represented as an atomic component where the behavior encompasses all its basic and structured activities. All process variables are added to the atomic component. Basic activities such as receive.../ , reply.../ , invoke.../ are translated into specific transitions triggered by respectively Receive * and Reply * ports. Their corresponding variables are implicitly attached to the above ports. The assign.../ activity is translated as an internal transition that executes the corresponding assignment. Structured activities define the overall control flow of transitions in the atomic component, in the usual way. In particular, transition guards are extracted from if..., while..., repeatuntil.../ and pick.../ activities. As a restriction, the parallel execution of activities within a flow.../ is not supported. In this case, their execution is made sequential in an arbitrary order.

Finally, we define the connectors and the composition of the atomic components by using the PartnerLinks defined for BPEL processes. Every invoke.../ , receive.../ and reply.../ , receive.../ interaction defined over partner links is translated to a connector relating the corresponding components and their respective ports. Let us notice that processes may interact through partner links with external WS, that is, developed in other languages than BPEL (such as Java, C, etc). In this case, these WS are represented as atomic components with an implicit behaviour, for arbitrarily sending and receiving data through their connected ports.

Similar translations have been already defined in the literature [START_REF] Stachtiari | Rigorous analysis of service composability by embedding WS-BPEL into the BIP component framework[END_REF]. As the above translation is structural the resulting model remains comprehensive for the WS designer. The representation relies basically on adapting reusable and composable model components that directly maps processes with limited numbers of execution steps. Despite that, some features in BPEL language are not considered such as fault/event handling and scopes. Security errors that can be generated by these aspects are not in the scope of this paper.

Decentralized Label Model

The decentralized label model (DLM) [START_REF] Myers | Protecting privacy using the decentralized label model[END_REF] provides a universal labeling scheme where security labels (or levels) are expressed using set of policies. A confidentiality label L contains (1) an owner set, denoted O(L), that are principals representing the originating sources of the information, and (2) contains for each owner o ∈ O(L) a set of readers, denoted R(L,o), representing principals to whom the owner o is willing to release the information. The association of an owner o and a set of readers R(o) defines a policy. Principals are ordered using an acts for partial order relation (denoted ≺) which is a delegation mechanism that enables a principal to pass his rights to another principal (e.g., o 1 ≺ o 2 states that o 2 can act for o 1 ). A security domain is defined over the set of confidentiality labels by using a flows to relation defined as follows:

L 1 ≤L 2 ≡ ∀o 1 ∈ O(L 1 ). ∀o 2 ∈ O(L 2 ). o 1 ≺ o 2 ∧ ∀r 1 ∈ R(L 1 , o 1 ). ∃r 2 ∈ R(L 2 , o 2 ). r 1 ≺ r 2
The intuition behind the flows to relation ≤ above is that (1) the information can only flow from one owner o 1 to either the same or a more powerful owner o 2 where o 2 can act for o 1 and (2) the readers allowed by R(L 2 , o) must be a subset of the readers allowed by R(L 1 , o) where we consider that the readers allowed by a policy include not only the principals explicitly mentioned but also the principals able to act for them.

In our setting for BPEL WS composition, the principals used to define the acts for relation and the security domain are obtained from BPEL partner links that correspond to WS URI. That is, principals can be either BPEL processes or atomic WS in some primitive language.

The designer expresses his security policy by tagging BPEL variables using DLM labels. The security domain and these annotations are then transposed as such on the component-based model. For example, a confidentiality label L: {Prosumer:SMG} assigned to the variable outplan in the Prosumer process presented in Figure 4 (right side) is used directly, as it is, for the outplan variable in Prosumer atomic component obtained by translation (left side).

Implementation

The configuration synthesis algorithm described in Section 3 is implemented and available for download at http://www-verimag.imag.fr/∼bensaid/secureBIP/. The user provides the WS composition in BPEL and a configuration file (.xml) that contains an acts for relation defining authorities for different processes and the DLM annotations for some process variables. An example of a configuration file is provided in the Appendix. In a first step, the BPEL composition is structurally transformed into a component-based model representation in BIP [START_REF] Basu | Rigorous component-based design using the BIP framework[END_REF]. The transformation extends an already existing translation of BPEL to BIP developed in [START_REF] Stachtiari | Rigorous analysis of service composability by embedding WS-BPEL into the BIP component framework[END_REF] to study functional aspects. In a second step, the synthesis tool takes as input the system model (.bip) and the configuration file (.xml), builds the dependency graphs of components and runs the synthesis algorithm to produce the complete configuration.

Use-case: Smart Grid Application

To illustrate the use of our framework we consider a simplified model of a smart grid system [START_REF] Koss | Establishing a Smart Grid Node Architecture and Demonstrator in an Office Environment Using the SOA Approach[END_REF] managed through Internet network using WS. Smart grid systems usually interconect a number of cooperating prosumers, (that is, pro-ducers and con-sumers) of electricity on the same shared infrastructure. In principle, every prosumer is able to produce, store and consume energy within the grid. However, its use of the grid has to be negotiated in advance (e.g., on a daily basis) in order to adapt to external conditions (e.g., weather conditions, day-to-day demands,...) as well as to maintain the behaviour of the grid in some optimal parameters (e.g., no peak consumption). Smart grids are subject to requirements related to safety and security e.g., the power consumption / production of a prosumer must remain secret as it actually may reveal sensitive information.

In our WS model of the smart grid, the system consists of a finite number of prosumer processes, P r i , communicating with a smart grid process, SMG. Initially, each P r i sends its consumption and production plan, (P i , C i , B i ), for the next day to the grid. Production P i , consumption C i and (storage) battery B i are expressed using energy units (integer) where 0 P i 2, -3 C i 0 and -1 B i 1. The SMG validates the plans received by checking that the overall energy flow through the grid implied by these plans does not exceed the power line capacity. This check measures the consumption exceed acknowledgment, ack, compared to a bound, that is, ack=0 if the -1 n i=1 (P i + C i + B i ) 4, otherwise, it returns the difference between the sum of the plans and the consumption bounds. The SMG sends back to each P r i an ack i to negotiate updating its own plan, where ack = n i=1 ack i . The negotiation terminates when ack=0 meaning that the energy flow on the grid does not exceed the line capacity. Figure 5 shows the system overview with two prosumers that exchange queries with the smart grid. The information flow security requirements that we emphasize here consist first, on ensuring the confidentiality of energy consumption plan for each P r i , (which can reveal sensitive competitive information such as its production capacity) and second, ensuring that no prosumer is able to deduce the consumption plan of any other prosumer by observing the received ack information. For instance, consider two prosumers such that one of them, P r 1 , sends an extreme consumption plan (0, -3, -1) to the SMG while the second, P r 2 , sends (0, -3, 0) as a consumption plan. The SMG first calculates the acknowledgment message that is ack=3 then sends ack 1 =1, ack 2 =2 messages to respectively P r 1 and P r 2 . Assume now that P r 2 sends back a new consumption plan (1, -2, 1) and gets back ack 2 =0. By only observing other ack1 message sent to P r 1 , the P r 2 can deduce that the consumption plan of P r 1 is equal to (0,-3,-1). The translation of P r 1 process is given in Figure 4 while the translation of the SMG process is given in the appendix.

For applying our approach to check system security, the designer introduces initially his partial security policy by tagging intuitively some variables that he considers sensitive in system model with security annotations. He also provides an acts for diagram for all model components where he gives authorities to some of them to act for others. In this system the SMG component can only acts for both P r 1 and P r 2 . To ensure confidentiality of prosumers plan, the system administrator annotates out plan1 with L 1 = {P r 1 : SMG} label and out plan2 with L 2 = {P r 2 : SMG} label. Obviously, L 1 ≤ L 2 and L 2 ≤ L 1 are indicating that both prosumers represent separate security domains that can only communicate with the SMG component. Then, the tool automatically generates the dependency graph of the transformed smart grid system. Presented in Figure 6, the dependency graph is build over ports (rectangles) and data variables (circles) locally at each atomic component(big circles), where arrows intra-circles represent dependencies between ports and data in the same atomic component while arrow inter-circles represent inter-components dependencies.

The application of Algorithm 1 to the system dependency graph detects an illegal information flow in the system and generates an error in the out plan node for both prosumers. Indeed, the label propagation in the system creates at ack node of the SMG component a new label L 3 = L 1 L 2 . Obviously, label L 3 = {P r 1 : SMG; P r 2 : SMG} is more restrictive than both labels L 1 and L 2 .

Since the ack node depends on out ack1 in P r 1 and out ack2 in P r 2 , then it is labelled with L 3 in both prosumers which causes security level inconsistency at out plan nodes. Algorithm 1 generates an inconsistent security level error between both out plan and ack nodes. Here, the system designer has to redefine the initial configuration, for instance, by given more privilege to prosumers to act for SMG component and enforce variable ack to higher security level L 3 = {SMG : SMG}. In this case, and with the authority that each prosumer gain, flow can go from L 3 to L 1 and L As an evaluation of the compositional approach performance, table 1 presents some experiments over configuration time t for different variation of the number of prosumer components, n, in the smart grid system for a given number of variables X, ports P and with initial labels number, σ 0 . Here we can notice that our configuration synthesis does not introduce an overhead even by increasing the number of system components.

Related Work

There are many commercial tools like IBMs XML Security Gateway XS40, application servers [START_REF] Corporation | Using BPEL processes in WebSphere Business Integration Server Foundation[END_REF] and Web Service Enhancements for Microsoft .NET (WSE) [15] that provide GUI to help users configure and verify WS security but the user has to learn about standard WS-Security syntax and options.

In [START_REF] Tatsubori | Best-practice patterns and tool support for configuring secure web services messaging[END_REF], authors propose a high-level GUI for configuring WS security with a business-policy-oriented view. It models the messaging with customers and business partners, lists various threats, and presents best-practice security patterns against these threats. A user can select among proposed generated basic patterns according to the business policies, and then apply them to the messaging model. The result of the pattern application is, afterwards, described in the Web Services Security Policy Language (WS-Security Policy). None of these tools handle the non-interference property like we do. Regarding formal models for non-interference in WS, in [START_REF] Busi | A survey on non-interference with petri nets[END_REF], authors present WS data flows as extensions of the Petri-net model and in [START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF], non-interference has been formalized for Petri-nets. Nevertheless, these solutions have some drawbacks which are mainly that data and resource description is manual and can be therefore error prone. Later on, the same authors propose the IFAudit tool that represents data flow as propagation graphs generated from workflow's log data. The propagation graphs are analyzed against the security policies.

Distinct security models are proposed in [START_REF] Movahednejad | Security-aware web service composition approaches: State-of-the-art[END_REF] where authors propose a classification of security-aware WS. They list a set of works classified in information flow category. Nevertheless, these works are restricted to verification rather than security configuration synthesis. Here we propose a practical automated verification method for transformed model of composed BPEL WS, based on formally proved security conditions. In [START_REF] She | Enhancing security modeling for web services using delegation and pass-on[END_REF], the authors deal with chained services and security is checked with a notion of back check procedure and pass-on certificate. It is not clear how to apply this solution to WS orchestration workflows and how to handle implicit interference. A recent work extends BPEL-orchestra engine [START_REF] Demongeot | Preventing data leakage in service orchestration[END_REF] to handle IFC security. This work is inspired from SEWSEC framework [START_REF] Zorgati | Sewsec:a secure web service composer using information flow control[END_REF] by adopting the distributed security label to annotate information. Nevertheless, instead of using abstractions like PDG, this annotation is set inside the BPEL code. Code annotation requires security skills, does not separate functional and security concerns and induces development overhead.

Finally, our work is related to information flow security in component-based systems. In contrast to [START_REF] Abdellatif | Automating information flow control in component-based distributed systems[END_REF] where authors verify security in a component-based model by annotating the system ADL (Architecture Description Language) and tracking information flow at intra-and inter-components separately, this work provides a sound model with formal proofs guaranteeing system non-interference. Besides, and compared to our previous work [START_REF] Ben Said | Model-driven Information Flow Security for Component-Based Systems[END_REF] where we adopted a more general component-based model to build secure distributed systems, here we propose a simpler message-based send-receive model suitable to model applications with web-style primitives and communications like BPEL-based composed WS and we propose not only a security verification but also a practical solution for security configuration synthesis.

In this paper, we propose a component-based approach to assist system designers to analyze and enforce information flow security in WS compositions. We implemented a compositional synthesis algorithm that propagates labels and generates secure system configurations starting from partial configurations.

As future work, we plan to extend this work in several directions. First, we are seeking for less restrictive syntactic conditions for establishing non-interference. In particular, we believe that a finer control flow analysis using for instance dominance analysis [START_REF]Domain Engineering, Product Lines, Languages, and Conceptual Models[END_REF] can provide finer dependencies amongst variables and ports. Second, we are working on relaxing the non-interference property and introducing declassification mechanisms to our model. Declassification has been studied for sequential interactive programs with inputs and outputs [START_REF] Askarov | Tight enforcement of information-release policies for dynamic languages[END_REF], nevertheless, its extension to distributed concurrent component-based models such as Web Services is less understood.

Fig. 1 .

 1 Fig. 1. Information flow analysis overview with component-based model

4 6 while nList = ∅ do 7 choosestop inconsistency detected 12 ζ

 6712 choose-and-remove(BList, Bi) 5 nList ← Xi ∪ Pi intra component inner loop for Gi -and-remove(nList, ni) 8 si ← {ζ(n) | n →ini} recompute security level of ni 9 if ζ(ni)≤si and si = ζ(ni) then 10 if ni ∈ Xi and σ0(ni) = ⊥ and σ0(ni)≤si then 11 (ni) ← si update and propagate change within Gi 13 nList ← nList ∪ {n | ni →in} 14 foreach pi ∈ P out i ∪ P in i do 15 find pj ∈ P out j ∪ P in j with (pipj) ∈ Γ or (pjpi) ∈ Γ 16 if ζ(pi) = ζ(pj) then 17 ζ(pj) ← ζ(pi) update and propagate change across connectors 18 BList ← BList ∪ {Bj}

Fig. 3 .

 3 Fig. 3. Dependency graphs of Producer-Buffer-Consumer from Figure 2

9 Fig. 4 .

 94 Fig. 4. Atomic component representation of a BPEL process

Fig. 5 .

 5 Fig. 5. Smart grid application overview

Fig. 6 .

 6 Fig.6. Generated dependency graphs (fragments).

  Proposition 1. A security annotation σ is secure for a system Γ (B 1 , ..., B n ) with an arbitrary non-empty set of initial configurations Init whenever all local transitions t in components B i are sequentially consistent ∀(x := e) ∈ asgn(t). ∀y ∈ use(e) ∪ use(guard(t)). σ(y)≤σ(x) all components B i are port deterministic i.e., for all transitions t 1 , t 2 src(t 1 ) = src(t 2 ) ∧ port(t 1 ) = port(t 2 ) ⇒ guard(t 1 ) ∧ guard(t 2 ) ≡ f alse and moreover, there exists a security annotation on ports ς : P → S such that: ports of all causal local transitions t 1 , t 2 have increasing levels of security d st(t 1 ) = src(t 2 ) ⇒ ς(port(t 1 ))≤ς(port(t 2 )) ports of all conflicting local transitions t 1 , t 2 have the same level of security src(t 1 ) = src(t 2 ) ⇒ ς(port(t 1 )) = ς(port(t 2 )) variables and ports are consistently annotated on all local transitions t ∀(x := e) ∈ asgn(t). ∀y ∈ use(guard(t)). σ(y)≤ς(port(t))≤σ(x) variables and ports are consistently annotated on connectors ∀(p out p

in ) ∈ Γ. σ(v ar(p out ))≤ς(p out ) = ς(p in )≤σ(v ar(p in ))

Proof. (Sketch) It can be shown that the conditions above imply the unwinding conditions of

[START_REF] Rushby | Noninterference, transitivity, and channel-control security policies[END_REF]

for indistinguishability ≈ s at security level s. In turn, unwinding conditions are guaranteeing non-interference and therefore security as defined in Definition 1. A detailed proof is available in

[START_REF] Ben Said | Model-driven Information Flow Security for Component-Based Systems[END_REF][START_REF] Ben Said | Model-driven information flow security for component-based systems[END_REF]

for a slightly more general component-based model allowing multiparty interactions between components.

Table 1 .

 1 Model size and configuration time (in s) for smart grid application with one initial security label by each prosumer.

	n	P	X	σ0	t
	4	26	24	3	1.82
	13	98	87	12	1.94
	25	194	171	24	2.01
	101	802	703	100	2.82

2 .

The research leading to these results has received funding from the European Community's Seventh Framework Programme [FP7/2007-2013] under grant agreement ICT-318772 (D-MILS).

Appendix

Figure 7 shows a transformation of the SMG process of the smart grid system given as BPEL workflow, into an atomic component. The behavior of the atomic component represents the activities given in the BPEL process. The designer input configuration file includes an acts for relation as well as some annotated variables. Here we presented an example of a configuration file of the smart grid system. In this xml file we define authority/ to different system components representing the acts for relation. Moreover, we specify by var config/ the annotations of variables from different atomic components (processes).

<? xml version = " 1.0 " ? > < config > < acts_for > < authority > SMG: Prosumer1 , Prosumer2 , Prosumer3 </ authority > </ acts_for > < var_config > < variable var = " outplan " process = " Prosumer1 " label = " Prosumer1:SMG " > </ variable > < variable var = " outplan " process = " Prosumer2 " label = " Prosumer2:SMG " > </ variable > < variable var = " outplan " process = " Prosumer3 " label = " Prosumer3:SMG " > </ variable > </ var_config > </ config >