An End-to-End Security Model for Adaptive Service-Oriented Applications

SOA applications are generally built from existing services and based on standard tools for service composition like Web Services (WS) [1]. These applications are deployed in various domains like e-health systems, e-commerce and social networks. They exchange critical information between mistrusted parties and networks and have to preserve people’s privacy and business data confidentiality. Several standards and tools [2,3,4] are currently used to secure WS communications. They are generally based on access control policies that focus on point-to-point communications. Nevertheless, end-to-end security is required and implies tracking information flow through all the system services and analyzing data dependencies. Typically, forwarding confidential data to unauthorized services has to be detected. Consequently, data dependence has to be tracked and explicitly exposed; otherwise, security composition can induce security leaks called interference [5].

An application free of this problem is said to satisfy the non-interference property [8]. To check that a WS satisfies non-interference, a classical technique consists in classifying WS data with respect to its security level and verifying that data with low-level security constraint (like public data) is not influenced or calculated from any data with high-level security constraint (like confidential data). Furthermore, the security classification model has to consider authorization rules and trust between services and consider the network not unique as potential attacker. Indeed, current SOA applications are generally composed of loosely coupled services that come from different providers. Tracking data flow to non-authorized services is not an easy task in a distributed system [6].

Standard orchestration languages like BPEL (Business Process Execution Language) [7] are practical to build complex composed WS and to track their execution for reliability reasons mainly. Nevertheless, these languages, as well as WS security standards, provide no way to define data security classification and to check non-interference property. There is a clear need for a new security model and a practical tool that helps administrators setting intuitive security configuration parameters and synthesizes automatically the whole security configuration. The tool has to be robust proving formally that the security configuration satisfies security policies. It has to be scalable, that is, when the number of services’ activities is huge or when the number of composed services is important, security configuration is calculated within an acceptable reasonable time. Furthermore, security configuration has to be adaptable to special cases like emergency where security constraints have to be relaxed. For example, in a home gateway application, if a fire is detected, the information has to reach a remote monitor service in a short time even though such information is not protected with cryptography encryption. More generally, a compromise between security constraints and functionality needs has to be found and relaxing some information secrecy is sometimes needed to reach this compromise. This feature is called declassification and is still a hard problem in security research field and is rarely implemented in real applications like SOA [9, 10]. Another aspect of adaptation is when the system architecture is modified. Typically, removing or adding new services or modifying some security configuration settings may require the security configuration synthesis that has to be executed rapidly not to slow down the adaptation time.

In this paper, we propose E2SM (End-to-End Security Model), a security model for composed and adaptive SOA applications constructed as a composition of BPEL processes. The main idea of E2SM is to abstract BPEL processes to a set of graphs to show data dependencies and starting from a few initial configuration settings, the whole system configuration is generated while checking its non-interference property. Non-interference checking is modular: to check that a hierarchical BPEL process is secure, it is sufficient to check that each involved BPEL process is secure. Furthermore, E2SM assists users (service designers, developers or administrators) to set-up business oriented security constraints at a high level, checks constraints coherence and synthesizes a complete secure configuration. If the user’s security constraints induce non-secure configuration, the user is guided to correct his initial configuration by relaxing some constraints or modifying his initial configuration. Dynamically, E2SM checks any security re-configuration. It tracks the affected service parts and regenerates the new security configuration in acceptable time. Our solution is practical since users do not need to be security experts, robust since the security model and algorithms are based on a formal modeling, scalable thanks to the compositional checking and adaptable to SOA dynamic reconfiguration.

The rest of the paper is structured as follows. Section 2 describes program dependence graphs as abstractions for BPEL workflows. Section 3 presents the security model and E2SM configuration synthesis algorithms. Section 4 evaluates E2SM mainly the algorithm performance. Section 5 presents related work and Sect. 6 concludes the paper and presents its perspectives.

In this section, we describe program dependence graphs (PDG) as abstraction for BPEL processes for data tracking and the system dependence graphs (SDG), our extension to PDG to abstract composed BPEL processes.

2.1 Program Dependence Graphs

Program dependence graphs (PDG) are a standard tool to model information flow through a program [11]. Graph nodes represent program statements or expressions. A data dependence edge, represented with an arrow, \( {\text{x}} \to {\text{y}} \) means that statement x assigns a variable which is used in statement y (without being reassigned underway). A control dependence edge \( {\text{x}} \to {\text{y}} \) means that the mere execution of y depends on the value of the expression x (which is typically a condition in an if- or while-statement). A path \( {\text{x}} \to {}^{*}{\text{y}} \) means that information can flow from node x to node y. Contrarily, if no path exists from node x to y, it is guaranteed there is no information flow from x to y. To identify all statements influencing a node y, the backward slice is defined as \( {\text{BS}}\left( {\text{y}} \right) = \left\{ {{\text{x}}|{\text{x}} \to {}^{*}{\text{y}}} \right\} \). PDG is classically used in imperative languages like Java [8, 11]. We implemented in a previous work [18] a PDG generator for BPEL processes. A BPEL process is composed mainly of two types of activities, that are (1) basic activities, such as receive, reply, invoke, assign, throw, exit, and (2) structured activities, such as sequence, if, while, repeat − until, pick, f low. First, a BPEL control dependence sub-graph is constructed where nodes represent BPEL activities and edges represent possible execution sequences of the activities. This is applicable mainly for condition activities like < if…. > or < switch… >. For example, a control flow edge x → y means that the activity represented by y may execute immediately after the execution of the activity represented by x. Second, a data dependence analysis is performed attributing the system variables to their activities and based on a Definition-Use relation. For each ordered pair (n_d, n_u), where a statement called n_d contains a definition of a variable v and used in a statement n_u, a data dependence is identified [12]. For example, Fig. 1. illustrates the graphical representation of the BPEL process of a laboratory service deployed on a cloud. It receives a patient medical record and following the record type, it forwards the record to the radio laboratory service or the blood laboratory service. The activities are indexed with their node number.

Graphical representation of the Laboratories BPEL and the correspondent PDG

Full size image

For example, node (01) corresponds to the receive BPEL activity and node (02) corresponds to the copy instruction of the assign activity. In (01), variable input_from_reception is used and in (02) this variable is copied to the newly defined record variable. Since there is a Definition-Use relation between the two activities w.r.t input from reception variable, a graph edge is created between node (01) and (02). Similarly, there is an edge between nodes (01) and (03). Node (04) corresponds to a structured if activity where variable record type is used. The Definition-Use relation with respect to variable record_type allows creating the edge between (02) and (04). On the other hand, a control dependence creates the edge between (04) and (05) and between (04) and (05) due to the condition activity at node (04).

2.2 System Dependence Graphs

For composed BPEL processes, SDG describes the information flow for the entire system. To build it, we consider the PDG of all services and connect them with binding edges. Each binding edge corresponds to an inter-service connection: the source is the sender output endpoint and the sink is the destination service endpoint. Furthermore, for each primitive service, we construct a restricted PDG with nodes corresponding to input and output variables and edges joining the input nodes to the output nodes they depend on. Variable dependence in atomic services can be identified either using classical program dependence graphs [13] or using a description of the service behavior. In the worst case, we consider that all service outputs depend on all service inputs. Hereafter, we give a formal definition of SDG.

Definition 1

(System Dependence Graph). Let WSS be a WS system composed of n services \( \left( {{\text{S}}_{\text{i}} } \right)_{{{\text{i}} = 1,{\text{n}}}} \). For each service S_i, let \( {\text{G}}_{\text{i}} = ({\text{N}}_{\text{i}} ,{\text{E}}_{\text{i}} ) \) be its associated PDG. The system dependence graph \( {\text{G}} = \left( {{\text{N, E}}} \right) \) is constructed as follows: \( {\text{N}} = \cup_{{{\text{i}} = 1,{\text{n}}}} \) Ni and \( {\text{E}} = {\text{E}}_{\text{inter}} \cup ( \cup_{{{\text{i}} = 1,{\text{n}}}} {\text{E}}_{\text{i}} ) \) where \( {\text{E}}_{\text{inter}} \) is the set of edges corresponding to inter-service bindings.

Many security annotation models are proposed in the literature [5]. Nevertheless, DLM, the decentralized label model [14] initially proposed for Java programs, is more appropriate for distributed services with mutual distrust. We extend DLM for SOA and we define non-interference for BPEL-based workflows. Afterwards, we propose two algorithms for non-interference checking and configuration synthesis.

3.1 Decentralized Label Model

The essentials of DLM are objects containing information to protect, principals and labels. Objects can be variables, storage locations or input/output communication channels receiving/sending data. Principals are persons or programs that own or access pieces of system information. To express confidentiality policy, labels are associated to objects and a principal can be owner initiating the information or reader authorized to access that information. A label general structure is \( {\text{L}} = \left\{ {{\text{o}}_{1} :{\text{r}}_{11} ,{\text{r}}_{12} , \cdots ;{\text{o}}_{2} :{\text{r}}_{21} ,{\text{r}}_{22} , \cdots ; \cdots ;\,{\text{on}}\,:{\text{r}}_{{{\text{n}}1}} ,{\text{r}}_{{{\text{n}}2}} , \cdots } \right\} \) where o_i are owners and r_ij are readers. For example, in a clinical SOA, the medical record can be labeled L = {patient : clinic, doctor} which indicates that the patient principal allows the clinic and the doctor to access his information. Labels are ordered using the no more restrictive than relation, represented by ⊆ symbol. Given two labels L1 and L2, we have \( {\text{L}}1 \subseteq {\text{L}}2 \) if and only if owners of L1 are included in L1 and, for a given owner, the readers of L2 are included in those of L1. For example, if L1 = {clinic : doctor1} and L2 = {patient : doctor1, doctor2}, we have \( {\text{L}}2 \subseteq {\text{L}}1 \). During program computation, when information is labeled with L1 and L2, respectively, the result should have the least restrictive label that maintains all the flow restrictions specified by L1 and L2. This least restrictive label, the join of L1 and L2 (written as L1∪L2), is constructed so that owners is the union of L1 and L2 owners and the reader set for each owner in L1 and L2 is the intersection of their corresponding reader sets. For example, let us suppose that a medical record is composed of two parts so that the first part is labeled L1 = {patient : doctor1} and the second one is labeled L2 = {patient : doctor1, doctor2}. The medical record has to respect both constraints and then only doctor1 is allowed to read the medical record content with label L1 ∪ L2 = {patient : doctor1}. Note that security labels represent a lattice (L, ⊆) [14] where L denotes the finite set of labels that is partially ordered by ⊆. We denote by * the weakest principal used to annotate public information. For example, label {p : *} indicates that information is owned by principal p which allows all principals access its information.

Principals can delegate their information ownership to other principals with regard to a trust relation. According to trust hierarchy, information can be relabeled in a safe way following two forms. In the first form, label ownership is changed. A label’s owner O can be replaced by owner O’ so that O trusts O’. The second form of relabeling is declassification, which allows relaxing security constraints in a safe way. The information is copied in a fresh variable and relabeled to a less restrictive security label. This is allowed only by data owner or by another principal trusted by the owner. The new label is usually calculated from the information label by adding readers (more principals are allowed to access information) or removing some policies (owners with their respective readers), which imposes less reading constraints on that information. For example, in the Fig. 1. use-case, the patient record labeled L = {patient: laboratory} does not allow initially neither the blood-Lab or the radio-Lab to read data. Nevertheless, since these labs are trusted by the patient, they can be added as readers and L is declassified to L2 = {patient:laboratory, blood-Lab, radio-Lab}.

Since we have two kinds of services in SOA, managed and external services, we extend DLM with required and provided labels. Required labels are immutable labels that represent external constraints, typically third-party service requirements that cannot be changed by the administrator. Provided labels are labels set on managed resources and can be modified by the administrator when needed.

3.2 PDG-Based Non-interference Checking

Let N be the set of PDG nodes, X the set of program variables and L the set of security labels. Let \( {\text{S}}:{\text{N}} \cup {\text{X}} \to {\text{L}} \) be a function assigning security labels L to nodes in \( {\text{N}} \cup {\text{X}} \) defined as follows. For a program statement represented by a node n, if a variable v is defined (that is, assigned) in that statement, then \( {\text{S}}\left( {\text{n}} \right) = {\text{S}}\left( {\text{v}} \right) \). For example, in Fig. 1., we have \( {\text{S}}\left( {\left( {01} \right)} \right) = {\text{S}}\left( {input\_from\_reception} \right) \). If no variable is assigned in the statement represented by the node n, then \( {\text{S}}\left( {\text{n}} \right) = \cup_{\text{i}}\,{\text{L}}_{\text{i}} \) where L_i represents the security label of i^th variable used in that statement [11]. Non-interference property is satisfied in annotated PDG with S if and only if for every edge \( {\text{x}} \to {\text{y}} \) it holds \( {\text{S}}\left( {\text{x}} \right) \subseteq {\text{S}}\left( {\text{y}} \right) \). Classically, non-interference is iteratively checked starting from specific nodes called slicing criteria that we define hereafter. For a statement of interest represented by a node x, the backward slice BS(x) extracts those statements that potentially have an influence onto that statement. This later is called the slicing criterion. In our work, we define slicing criteria are the nodes that have required labels. Typically, a slicing criterion is a node representing an endpoint to an external service and imposing its security constraint. Consequently, required security label specifies a limit so that only information having a smaller security label may reach that statement. Inversely, provided labels can be assigned to any node in PDG. Formally, provided labels are defined by a partial function \( {\text{P}}:{\text{N}} \cup {\text{X}} \to {\text{L}} \cup \{ \bot \} \). Similarly, required security is defined as a partial function \( {\text{R}}:{\text{N}} \cup {\text{X}} \to {\text{L}} \cup \{ \bot \} \). In this model, the security label S(n) of every node n must moreover satisfy: \( {\text{P}}\left( {\text{n}} \right) \subseteq {\text{S}}\left( {\text{n}} \right) \subseteq {\text{R}}\left( {\text{n}} \right) \) whenever P(n) and/or R(n) are defined. In this extended model, the non-interference property in an annotated PDG can be verified as follows.

Proposition 1

(Non-interference checking - version 1). In a PDG with P and R the functions assigning respectively the provided and required security labels, the non-interference property holds if the following condition is satisfied: \( \forall {\text{n}} \in {\text{dom}}\left( {\text{R}} \right) \), \( \forall {\text{x}} \in {\text{dom}}\left( {\text{P}} \right) \cap {\text{BS}}\left( {\text{n}} \right) \), \( {\text{P}}\left( {\text{x}} \right) \subseteq {\text{R}}\left( {\text{n}} \right) \). Considering actual security labels S, the next proposition provides an alternative way for checking non-interference [11].

Proposition 2

(Non-interference checking - version 2). In a PDG with P and R the functions assigning respectively provided and required security labels, non-interference property is satisfied if the following condition holds: \( \forall {\text{n}} \in {\text{dom}}\left( {\text{R}} \right) \), \( {\text{S}}\left( {\text{n}} \right) \subseteq {\text{R}}\left( {\text{n}} \right) \).

Starting from an initial annotation for provided and required security levels R and P, Algorithm 1 calculates the actual security configuration S using an iterative method. Algorithm 1 can be considered as a flavor of the classical Bellman-Ford algorithm. The number of iterations depends on relabeling occurrence which depends itself on the number of vertices, the graph connectivity and the initial label distribution.

Regarding declassification, specific nodes are selected to be declassification nodes [15]. A declassification node d has a security label S(d) and a required security label R(d) so that the relation \( {\text{S}}\left( {\text{d}} \right) \subseteq {\text{R}}\left( {\text{d}} \right) \) is not satisfied. Declassification implies that the user authorizes lowering S(d) to R(d). Non-interference with declassification holds if for each path from node x to y where the relation \( {\text{S}}\left( {\text{x}} \right) \subseteq {\text{S}}\left( {\text{y}} \right) \) is not true, there is a declassification node d on the path with \( {\text{S}}\left( {\text{x}} \right) \subseteq {\text{R}}\left( {\text{d}} \right) \) and \( {\text{S}}\left( {\text{d}} \right) \subseteq {\text{S}}\left( {\text{y}} \right) \) (assuming that there is no other declassification node on that path) [11]. Therefore, information flow control with declassification is no longer transitive. For confidentiality checking with declassification, a simple solution is to represent declassification nodes as barriers where slicing stops [16]. Barrier slices are defined as follows.

Definition 2

(Barrier slice). Let \( {\text{G}} = \left( {{\text{N}},{\text{E}}} \right) \) be a PDG, C a slicing criterion and B the set of barrier nodes. The barrier slice BS(C, B) for the slicing criterion C is the set of nodes on which a node \( {\text{n}} \in {\text{C}} \) (transitively) depends via a path that does not contain any node of B [16].

Checking confidentiality with declassification implies checking non-interference considering barrier slices instead of backward slices where the barrier nodes are composed of the declassified nodes and the entry node (corresponding to the entry point in the program). The slicing criterion is composed of the join of nodes with required labels and declassified nodes. Consequently, Proposition 1 can be adapted considering slices with barriers as follows.

Proposition 3

(Non-interference with declassification checking). In a PDG with P and R the partial functions assigning respectively the provided and required security labels, D a set of declassified nodes, e the root of the PDG (corresponding to the entry point of the program) and B a barrier node set where \( {\text{B}} = {\text{D}} \cup \left\{ {\text{e}} \right\} \). Non-interference with declassification is satisfied if the following condition holds:

Based on this definition, we propose Algorithm 2 that helps users checking and building secure configurations with declassification. Algorithm 2 calls the checkTrust(S, L1, L2) function that, for each service S and labels L1 and L2, verifies the declassification condition based on trustfulness between principals.

Proposition 4.

The algorithm Secure configuration checking accepts secure configurations and rejects non-secure ones.

Proof.

Let S be the computed configuration. For each node x with required security, we have one of the following conditions: either S(x) ⊆ R(x) or x is a declassified node. Otherwise, the algorithm stops. By definition, we have a secure PDG and then S is a secure configuration.

3.3 SDG-Based Non-interference Checking

To deal with system security, we extend the definition of security configuration defined for single WS (see Definition 1) to WS composition. A security system configuration is an assignment of security labels to variables and nodes within all the PDG of services composing the WS system.

Definition 3

(Security system configuration S). Let WSS be a WS system composed of a set of n services \( \left( {\text{Si}} \right){\text{i}} = 1,{\text{n}} \). For each service Si, let \( {\text{Gi}} = \left( {{\text{Ni}},{\text{Ei}}} \right) \) be the associated PDG and let Xi the set of its variables. Let \( {\text{E}}_{\text{inter}} \) be the set of edges corresponding to inter-service bindings. Let L be the set of labels, X the set of all service variables and N the set of all PDG nodes associated to WSS. We define a security configuration for a WS system as a mapping \( {\text{S}}:{\text{X}} \cup {\text{N}} \to {\text{L}} \) that associates security labels to variables and nodes. Moreover, we require the following three matching conditions amongst the different categories, for all i, j: (1) \( \forall {\text{v}} \in {\text{Xi}},\forall {\text{n}}_{\text{v}} \in {\text{Gi}} \), v defined at \( {\text{n}}_{\text{v}} \Rightarrow {\text{S}}\left( {\text{v}} \right) = {\text{S}}\left( {{\text{n}}_{\text{v}} } \right) \), (2) \( \forall {\text{v}} \in {\text{X}}_{\text{i}} ,\forall \text{n}_{\text{v}} \in {\text{G}}_{\text{i}} \), v used in \( {\text{n}}_{\text{v}} \Rightarrow {\text{S}}\left( {\text{v}} \right) \subseteq {\text{S}}\left( {{\text{n}}_{\text{v}} } \right) \) and (3) \( \forall {\text{n}} \in {\text{G}}_{\text{i}} ,\forall {\text{m}} \in {\text{G}}_{\text{j}} \), \( \left( {{\text{n}},{\text{m}}} \right) \in {\text{E}}_{\text{inter}} \Rightarrow {\text{S}}\left( {\text{n}} \right) = {\text{S}}\left( {\text{m}} \right) . \)

The two first conditions correspond to security configuration definition for a single service. The third condition states that the nodes corresponding to binding edges have the same security label since they hold the same information. By analogy to secure PDG, we define now a secure SDG as a composition of secure PDG. For SDG, we have two kinds of barrier slices: internal barrier slices inside PDG joining input variable nodes to output variable nodes and external barrier slices that correspond to inter-service bindings. For internal slices, since PDG are assumed to be secure, we have the guarantee that information does not flow from high level labels to low level labels except for declassification nodes. For external slices, the security enforcement ensures a matching between labels of inter-service nodes connecting PDG. Furthermore, in SDG, there is no room to declassification since it was treated locally to each PDG and for each declassified node ni, its actual security label was assigned to its required one, that is \( {\text{S}}\left( {{\text{n}}_{\text{i}} } \right) = {\text{R}}\left( {{\text{n}}_{\text{i}} } \right) \).

Definition 4

(Secure SDG). Let \( {\text{G}} = \left( {{\text{N}},{\text{E}}} \right) \) be an SDG of a WS system and \( {\text{G}}_{\text{i}} = \left( {{\text{N}}_{\text{i}} ,{\text{E}}_{\text{i}} } \right) \) the set of PDG of services composing the system for \( 1 \le {\text{i}} \le {\text{n}} \). We say that G is secure iff \( \forall 1 \le {\text{i}} \le {\text{n}} \), G_i is a secure PDG.

We define an end-to-end secure system as a system where information do not flow from high-level sources to lower level destinations except for special destinations where the user authorizes information declassification. Information dependence is detected thanks to PDG for BPEL activities and for atomic service programs.

Definition 5

(End-to-end secure WS System). Let WSS be a WS system comprising a set of composed WS services and let S the security configuration of the system. We say that WSS is end-to-end secure if for all y, x two variables, y depends on x implies \( {\text{S}}\left( {\text{x}} \right) \subseteq {\text{S}}\left( {\text{y}} \right) \).

Proposition 5.

Let WSS be a WS system and G its associated SDG. If G is secure then WSS is end-to-end secure.

Proof.

We prove the proposition by induction on the number n of composed services the information flows through. Consider the basic case where n = 1. This means that information flows inside a single composed service. Let us consider any two variables y and x so that y depends on x. That means, there exist a path in the PDG from a node n_x to a node n_y where respectively x and y are defined. Since the PDG is secure, we have \( {\text{S}}({\text{n}}_{\text{x}} ) \subseteq {\text{S}}({\text{n}}_{\text{y}} ) \). By matching variable and node labels, we have \( {\text{S}}\left( {\text{x}} \right) \subseteq {\text{S}}\left( {\text{y}} \right) \). Consider now that the proposition is true for any WS system composed of n−1 services for some n > 1. We prove that it is true for n composed services. Let S₁,.., S_n be the system services, \( {\text{G}}_{1} ,..,{\text{G}}_{\text{n}} \) their PDGs supposed secure and consider that information flows from variables x to y, which moreover belong to separate services S₁ and S_n. Let z be the output variable calculated from x inside S₁. Since, G₁ is secure, we have

Suppose that z is further received by S₂. By the induction hypothesis, the system composed of n−1 services \( {\text{S}}_{2} ,..,{\text{S}}_{\text{n}} \) is end-to-end secure. Then

(1) and (2) implies \( {\text{S}}\left( {\text{x}} \right) \subseteq {\text{S}}\left( {\text{y}} \right) \). As a conclusion, the proposition is true for a WS system with any number n of composed services. As illustrated in Algorithm 1, inside each process, the binding between the process and the service endpoints it communicates with, is checked before checking security inside the process. Applying the previous proposition, this ensures that the system is end-to-end secure.

3.4 Non-interference Runtime Checking

At run time, non-interference re-checking occurs when a label value changes corresponding to a security constraint modification. The non-interference checking and configuration synthesis is executed for the concerned process. If the label of a binding edge changes, the other edge’s label is updated and then the affected service has its security configuration re-checked and synthesized. The same logic is applied when a structural re-configuration occurs in the SOA. Indeed, adding or removing a service to the application implies adding or removing a binding and this may induce modifications to edge labels.

Scalability is ensured thanks to the composed checking and security configuration synthesis that can be performed in a parallel way. For the algorithm’s performance evaluation, we generate a single source graph so that the number of vertices ranges from 5 to 4000 vertices and generates edges in a probabilistic way. We use Erdos-Renyi model to generate edges. So edges are generated with a probability p where p is set to three values: 0.1 for weakly connected graph, 0.5 for moderated connected graph and 1 for full connected graph. Without loss of generality, we consider two security levels : secret and public. We distribute randomly public and private labels on graph edges and do not consider required labels not to stop the program iteration before visiting all edges.

Figure 2. shows the average time obtained after repeating the program execution 10 times. The bench is executed on a Mac OS version 10.8.5 with processor 1.3 GHz Intel Core i5 and 4 GB of Memory. The execution time increases with the number of vertices in the PDG and with the number of connectivity. We clearly see that the execution time is very acceptable and does not exceed 1 s for 4000 vertices and a fully connected PDG.

Performance evaluation of configuration’s synthesis program

Full size image

Adaptability to special cases is ensured thanks to the declassification feature, which allows a controlled relaxation of security constraints. E2SEM declassification can be extended to other kinds of declassification like temporal declassification [9]. Regarding system’s reconfiguration by adding or removing a service, thanks to the compositional verification, there is no need to recheck the whole newly obtained application, only affected processes have their security configuration re-checked and synthesized.

Our work is related to information flow security solutions for SOA. SEWSEC [17] is an end-to-end security tool for WS security. Compared to SEWSEC, our work allows not only non-interference checking but also security configuration synthesis, provides a formal security model and deals with adaptation. In [18], a security configuration synthesis is provided but the adopted model does not deal with declassification and adaptation. Similarly, in [19], information flow security is applied to component-based systems. Nevertheless, component code is required for label propagation, no formal model is provided and adaptation is not considered. Information flow control is also treated for event-based communications like those described in BPEL [20, 21]. For data dependence tracking, systems are modeled as Petri-nets [22, 23] or propagation graphs from workflow’s log data [24]. A language based information flow is proposed in [25] to check non-interference but declassification and adaptation are not supported. In [26, 27], authors deal with chained services with no centralized orchestration service composing them. A recent work extends BPEL-orchestration engine [28] and requires BPEL processes’ annotation whereas we propose a more practical approach with minimal configuration effort and configuration synthesis.

In this paper, we propose a robust security model to protect confidential data in complex business applications. Even though, we concentrate on BPEL, the work is applicable to other types of SOA composition languages. They only need to be mapped to program dependency graphs. We are currently implementing E2SM associated tool and experimenting it to secure e-health real SOA application.