Web services are software systems that support distributed applications composed of independent processes which communicate by message passing. To realize the full potential of web services, we need to compose existent web services in order to get more functionalities. However the composition of web services should be secure. In this paper we propose an automatic formal approach to monitor the execution of a choreography of web services and we prove its correctness. We introduce the syntax and semantic rules of a new operator which takes as input a choreography and a security policy and produces as output a secure version of this choreography which behaves like the original one and does not violate the security policy.
With the explosive growth of the Internet, intranet and electronic commerce,
the concept of web services has emerged in the world to be exploited by most
cross-organizational boundaries. In fact, web services provide a suitable
technical foundation for making business processes accessible within and across
enterprises. Moreover web services are software systems that support distributed
applications composed of independent processes which communicate by message
passing. But for an appropriate exploitation of web services, we need to
compose them. Indeed, individual web services often o↵er limited capabilities. In
some situations, a client's request cannot be satised by a single web service.
However, when composed with other web services, they can satisfy the client
demand. To realize the full potential of web services, we need to compose
existent web services in order to get more functionalities. Web service composition
rules deal with how di↵erent services are composed into a coherent global
service. In particular, they specify the order in which services are invoked, and the
conditions under which a certain service may or may not be invoked. Among
the approaches investigated in service composition, we distinguish
orchestration and choreography. The orchestration composes available services and adds
a central coordinator (the orchestrater) which is responsible for invoking and
composing the single sub-activities. However the second one, referred to as web
service choreography, does not assume the exploitation of a central coordinator
but it denes complex tasks via the denition of the conversation that should be
undertaken by each participant. While several proposals exist for orchestration
languages (e.g. Business Process Execution Language (BPEL)[
The need of secure web service composition has led to a great interest from
researchers of the last decade. However most of the works focus on how to
guarantee desired properties such as correctness, deadlock avoidance, etc. In our
work, in addition to these properties, we introduce an automatic approach to
monitor a choreography by specifying and enforcing security policies on web
services and we prove its correctness using formal methods. Some works such as
[
is proposed. In [
[
In this paper, we propose an enforcement of security policies over web services using formal methods. We present an automated approach for monitoring the behavior of a service in a choreography. More precisely, we dene an operator ⌦ that takes as input a process P and a security policy P and generates a new process P 0 = P ⌦ P which respects the following conditions : ✏ P 0 j s P ;i.e. P 0 satises the security policy P : ✏ P 0 v P;i.e. behaviors of P 0 are also behaviors of P: ✏ 8 Q : ((Q j s P ) and (Q v P )) =) Q v P 0 , i.e. all good behaviors of P are also behaviors of P 0 :
P 0 = P ⌦ P
the global calculus. Section 3 presents the formalism used to specify security policies. Section 4 illustrates the formalism used to specify choreographed services.
2
2.1
Syntax of the Global Calculus
I ::=
A ! B : ch (⌫ s~):I (Init) j A ! B : sh op; e;i y:I (Comm) j x@A := e:I (Assign) j if e@A then I 1 else I2 (If T henElse ) j I1 + I2 (Sum) j I1j I2 (P ar) j (⌫s)I (N ew) j XA (recV ar) j rec XA:I (Rec) j 0 (Inaction) The rst rule ( Init) says that the participant A invokes a service ch located at B and initiates new freshly generated session channels s~:The second rule (Comm) expresses the sending action by A whose message consists of a selected operator op and an expression e to the participant B which will store the value of e at the variable y:(Assign) is a local construct which updates the variable x located at A with e:(P ar) and (Sum) are respectively the parallel composition and the non-deterministic choice of interactions. (If T henElse ) is the standard conditional operation, while (recV ar) and (Rec) are used to express recursive behavior of interactions. 0 is the inactive interaction. 2.2
Semantics of the Global Calculus
The formal semantics of the global calculus is dened in terms of congurations
( ; I):The notation ( ; I) ! ( 0 ; I0) says that the global description I at a state
(which is the collection of all local states of the participants) will reduce to I0
at a new state 0 :Samples of reduction rules are presented here while the overall
operational semantic is detailed in [
(Init)
( ; A! B : ch (⌫ s~):I) ! ( ;(⌫ s~)I) (Comm)
` e@A + v ( ; A! B : sh op; e;i x:I) ! ( [x@B 7! v]; I) (Assign) (P ar)
( ; I1) ! ( 0 ; I10) ( ; I1j I2) ! ( 0 ; I10j I2) (Sum)
( ; I1) ! ( 0 ; I10) ( ; I1 + I2) ! ( 0 ; I10) (Rec) ( ; I[rec XA:I=XA]) ! ( 0 ; I0) ( ; rec XA:I) ! ( 0 ; I0) The rst rule is for initiation : A invokes a service located at B and initiates session channels s~ which will be shared locally by A and B:The second rule is for communication. The notation ` e + v is an evaluation judgment : evaluates the expression e to the value v: [x@B 7! v] is the resulting state of updating the local variable x at B by v:The evaluation judgment is also used in the assignment rule. The fourth rule is for parallelism. The (Sum) rule describes the behavior of a non-deterministic choice. The (Rec) rule says that if the unfolding of rec XA:Iunder reduces to I0 then rec XA:Iunder will reach ( 0 ; I0):
the buyer selects one of the two options o↵ered by the seller, QuoteAccept and
which will be stored in x by Seller and continues with the interaction I1:In the other case, the seller sends the abort number stored in the variable xAbortNo which will be stored in y by the Seller and terminates.
f Buyer ! Seller : B2Sch h quoteAccept;100; xi:1I g else
f Buyer ! Seller : B2Sch h quoteReject; xabortNo; xi:0 g 3
augmented with the notion of participants and their local states. In [
3.1
Syntax of EP C We show the syntax of EP C ;where s denote session channels, e an expression which can be an atomic value (such as a natural number or a boolean value) or a function (such as arithmetic functions and boolean operators) or a variable. op1; op2; :r:a:nge over operations. x is a variable. The rst construct is a receiving action, it is the invocation of one of the operators opi and reception of an expression which will be evaluated and stored in xi:The second construct is a sending action, it is the invocation of operator op with expression e:Furthermore, the operator " " represents the alternative composition. Finally, recursion is used for representing unbounded repetition. For representing recursive behaviors, we use term variables X; Y; : :Th:e operator used for recursion is rec X:P:Each occurrence of X in P denotes a recurring point. rec X:Pbehaves as P until an occurrence of X is found in the execution of P;then it will return to rec X:P: s B ⌃opi(xi):Pi; s C oph ei :P; i
P 1
P2;
X; rec X:P; 0 3.2
Semantics of EP C
which synchronize with another one to evolve. A participant A with its behavior
j j j N ::= A[P ] (Participant)
(⌫s)N (Res-NW) ✏ (Inaction-NW) where A[P ] is a participant with its behavior as shown in the rst construct.
parallel composition. When two participants initiate a session channel for communication, this session channel must be restricted to these two participants, this is given by (Res-NW): ✏denote the lack of networks. Reduction rules of networks are given by :
M ⌘
M 0
M 0 ! N 0 M ! N
N 0 ⌘
N
M ! M 0 M j N ! M 0 j N
M ! M 0 (⌫s)M ! (⌫s)M 0
2 ` e + v A[s C opjh ei :P] 1 j B[s B ⌃opi(xi):Qi] 2 ! A[P ] 1 j B[Qj] 2[xj7! v] i
A[P1] ! A[P 10] 0 A[P1
P2] ! A[P 10] 0
A[P [rec X:P=X]] ! A[P 0 ] 0
A[rec X:P] ! A[P 0 ] 0
employ mainly three operators to compose properties : and, or and not:The or operator is given here by :The not operator is dened here as follows : assume we have two participants A and B communicating and we want to apply the property "A should not send op1 to participant B", then we write it using
P = rec X:(sB C i6=1 opih eii :X sB B ⌃opi(xi):X) i
a bank. The bank should not send him back his account details if he is not yet authenticated. A client is said to be authenticated if he has received from the bank an acceptance for his authentication's attempt using the operation accept:The bank answers the client for his account request through the operation resAccount:The security property will then be written as follows : P = rec X:(s B ⌃opi(xi):X
i s C opi2f= accept;resAccountg i The block P 1 expresses the fact that the property allows all receiving actions. The block P 2 inhibits sending accept or resAccount to the client. The block P 3 intercepts the accept sending action and then no more restrictions are imposed since the authentication of the client is accepted.
4.1
Secured End-Point Calculus
The secured end-point calculus EP CS is a variant of EP C (End-Point Calculus)[
Syntax of EP CS Since EP C is a subset of EP C and EP CS is an extension of EP C;a part of the syntax of EP CS is presented in the last section. So in this section we will present the overall syntax of EP CS but we will describe only constructs that have not been described before.
j j j j j j j j j j P ::= !ch (s~):P j ch (⌫ s~):Q j s B ⌃i opi(xi):Pi s C oph ei :Q x := e:P if e then P else Q P Q P j Q (⌫s)P X rec X:P 0 The two rst constructs represent session initiation. ! ch (s~):Pis used for input and ch (⌫ s~):Qfor output. !ch (s~) says that the service channel ch; which is available to public, is ready to receive an unbounded number of invocations, o↵ering a communication via its freshly generated session channels s 2 s~:ch (⌫ s~) is an invocation of a service located at the service channel ch and an initiation of a communication session which will occur through session channels s~:After a session has been initiated between two participants and freshly generated session channels have been shared between them, they can communicate using the communication constructs. The assignment operator is x := e:P. if e then P else Q is a choice based on the evaluation of the expression e:The parallel composition is given by P j Q:The restriction construct (⌫s)P indicates that the session channel s is local to P:0 denotes the lack of actions. Finally, @P (P ) is the enforcement operator which controls the execution of P by allowing it to evolve if
Semantics of EP CS Initiation/Communication simulation Let P be a process stipulating the local behavior of a participant A in a web service. We observe in the end-point calculus reduction rules that processes always evolve without an external factor unless in initiation and communication. In fact, a participant initiating a communication or communicating with an another participant needs to synchronize with him to realize the interaction . Therefore, for enforcing security policies on a participant's behavior, we need to have a totally local description of its interactions. So we need to dene a simulation relation for the initiation and the communication of processes so that we can simulate the evolution of a process locally, i.e. without synchronizing with an another participant . We will dene the normal form of a process then introduce the simulation relation. Denition 1 (Normal form of a process). Every process representing the local behavior of a participant in a web service can be written as an internal sum of processes, which we call the normal form of a process :
8 P 2 P; P= i aiPi where P denotes the set of processes, ai range over atomic actions and Pi range over processes in P: Denition 2 (Simulation Relation). We dene a simulation relation over networks, denoted by A[P ] a A[P 0 ] 0 ;which says that process P in A at the state is able to execute the action a and reduce to P 0 with a new local state 0 : The simulation relation is dened following this rule
P = i aiPi 9 i 2 f 1; : : :g ;:an = ai
A[P ]
a A[Pi]
This rule says that when P is written in its normal form and one of the constituting processes is able to do an action a then A[P ] is also able to do it. Semantics of EPCS :
A[!ch (s~):Pj P0 ] A j B[ch (⌫s~):Qj Q0 ] B ! (⌫s~)(A[!ch (s~): PjPj P0 ] A j B[Qj Q0 ] B)
A ` e + v A[x := e: PjP0 ] A ! A[Pj P0 ] A[x7! v]
A ` e + tt A[if e then P1 else P2j P0 ] A ! A[P1j P0 ] A IfTrue
A ` e + ff
A[if e then P1 else P2j P0 ] A ! A[P2j P0 ] A IfFalse
A[P1j R] A ! A[P10j R] A0 A[P] A ! A[P0 ] A0 A[P1j P2j R] A ! A[P10j P2j R] A0 Par A[(⌫s)P] A ! A[(⌫s)P0 ] A0 Res
A[@P (!ch (s~):P)] Aj B[ch (⌫s~): QjR] B ! (⌫s~)(A[@P (P)j @P (!ch (s~):P)] Aj B[Qj R]) A[@P (ch (⌫s~):P)] Aj B[!ch (s~): QjR] B ! (⌫s~)(A[@P (P)] Aj B[!ch (s~): QjQj R] B)
A[P] A sB op(x) A[P0 ] A A[P ] A sB op(x) A[P0 ] A A ` e + v A[@P (P)] Aj B[s C oph ei : QjR] B ! A[@P0 (P0 )] A[x7! v]j B[Qj R] B Comm-In-Sec
A[P] A sC opjh ei A[P0 ] A A[P ] A sC opjh ei A[P0 ] A B ` e + v A[@P (P)] Aj B[s B ⌃i opi(xi):Qij R] B ! A[@P0 (P0 )] Aj B[Qjj R] B[xj7! v]
A ` e + v A[@P (x := e:P)] A ! A[@P (P)] A[x7! v]
A[@P (P1)] ! A[@P0 (P10)] 0 A[@P (P1j P2)] ! A[@P0 (P10j P2)] 0 Par-Sec
` e + tt A[@P (Pj if e then P 1 else P2)] ! A[@P (Pj P1)] IfTrue-Sec ` e + ff A[@P (Pj if e then P 1 else P2)] ! A[@P (Pj P2)] IfFalse-Sec A[(⌫ s~)(@P (P ))] ! A[(⌫ s~)(@P 0 (P 0 )] 0 )
freshly generated session channels s~:These session channels are restricted to participants A and B by the binding operator (⌫):Assignment is a local construct. Assign-rule evaluates an expression e and assigns the result of this evaluation to the variable x in A;then A behaves as P:The Res-rule restricts the use of session channels s~ to the process P in A:Init-In-Sec and Init-Out-Sec are the rules for communication initiation. We do not control session initiations but we control communication messages between the participants. Communication rules say if P and P are able to send or receive through the same session channel the same operation and become respectively P 0 and P 0 then @P (P ) do this action and becomes @P 0 (P 0 ):Secured assignment rule says that assignment is not considered by enforcement. The secured parallel composition rule says that the security operator applied to P1j P2 can evolve into (@P 0 (P 10j P2)) if P1 can evolve simultaneously with the policy security P into respectively P 10 and P 0 :For the restriction rule, binding session channels does not a↵ect the enforcement. Finally, the conditional rules say that enforcement is not a↵ected by conditionals. 5
Some of the important features of the enforcement operator is that it allows us to enforce only concerned participants by the security policies. In this in-lined monitoring framework, we do not modify the original behaviors of participants in a choreography. But if the security policy is not veried the evolution of the choreography will stop. In this section, we prove the correctness of our theory by dening rst some notions such as the partial order over processes and satisfaction notions.
Denition 3 (Partial Order over Processes). Let A[P1] ; A[P2] be two networks. We say A[P1] v A[P2] if the following condition hold : A[P1] a A[P 10] =)
A[P2] a A[P 20] and A[P 10] v
A[P 20] : Denition 4 (Satisfaction Notions). Let P trace. Symbols ✏ and j s are dened as follows : { {
We say that ⇠ satises P ;denoted by ⇠ ✏ P ;if ⇠ 2 JP K where JP K denotes the set of traces of P : We say that ⇠ could satisfy P ; denoted by ⇠ j s P ; if it exists a trace ⇠0 such that ⇠:⇠0 ✏ P : Theorem 1. Let P be a process and P a policy security. The following properties hold : be a security policy and ⇠ a 1. @P (P ) j s P ; 2. A[@P (P )] v A[P ] ; 3. 8 P 0 : ((P 0 j s P ) and (A[P 0 ] v A[P ] )) =) A[P 0 ] v A[@P (P )] : Proof. 1. The process @P (P ) is dened so that it can evolve into another process only if the security policy P is satised.
rules of the security operator and the denition of the partial order.
A[P 0 ] a A[P 10] 0 :Since A[P 0 ] v A[P ] 0 ; we conclude directly from the denition of v that A[P ] a A[P1] 0 :Since P 0 j s P ;we can also conclude from the denition of j s ;that a j s P :Finally, as A[P ] a A[P1] 0 and a j s P so A[@P (P )] a A[@P 0 (P1)] 0 and then A[P 0 ] v A[@P (P )] : Example 3 (Buyer-Seller Protocol). The buyer initiates a communication with the seller and requests for a quote. The seller sends back the quote. If the buyer rejects it then the protocol terminates. Otherwise, the seller sends to the buyer an order conrmation and the buyer conrms his command. In this case, the seller contacts the shipper and asks for delivery details which he transfer to the buyer and the protocol terminates. The security property that we want to apply in this protocol is : "the seller should communicate with the shipper only if the buyer conrms his command". As a consequence, the seller won't send to buyer the delivery details if he has not conrmed his command. The protocol is depicted in Fig.1. Critical actions that we have to supervise are in dark grey in Fig.1.
Seller ! Buyer : sh respQuote; vquote; xquotei : if resonable(xquote)@Buyer then
Buyer ! Seller : sh quoteAccepti : Seller ! Buyer : sh orderConf irmi :
Shipper ! Seller : s0 h delivDet; vdelivDet; xdelivDeti : Seller ! Buyer : sh delivDet; xdelivDet; xdelivDeti :0 else
Buyer[B2SCh (⌫s): sB ackSession:s C reqQuote: sB respQuote(xquote)
Seller
Fig. 1. Buyer Seller Protocol :if reasonable(vquote) then s C quoteAcc: sB orderConf irm:s C ackConf irm : sB delivDet(xdelivDet):0 else s C quoteRej:0]
Seller[B2SCh (s):s C ackSession: sB reqQuote:s C respQuoteh equotei : (s B quoteAcc:s C orderConf irm: sB ackConf irm: B2SHCh (⌫s0 ):s0B ackSession:s0 C reqDelivDeth ebuyeri :s0B delivDet(xdelivDet) :s C delivDet(xdelivDet):0 ) + (s B quoteRej:0)]
Shipper [B2SHCh (s0 ):s0 C ackSession:s0B reqDelivDet(xbuyer) :s0 C delivDeth edelivDeti :0]
P = rec X:( s C
op6=delivDet s B ⌃
op6=ackConfirm s B ackConf irm:rec Y:(s0 C
opi(xi):X The security property P is written using the recursion operator. In the recursion block, there are 3 processes combined with the internal choice. The rst process is : sC opih ei :Xwhich says that, through the session channel s (shared op6=delivDet between the buyer and the seller), the buyer can execute any sending action unless delivery details which should be done after the seller has received a conrmation from the buyer. The second process is : sB ⌃ opi(xi):Xwhich op6=ackConfirm says that the seller can receive any operation other than ackConf irm. This action is intercepted in the third process s B ackConf irm:rec Y:(s0 C opih ei :Y s0 B ⌃opi(xi):Y s C
i i conrmation from the buyer, he can communicate with the shipper through the session channel s0 without any restriction and he has also no restriction on his sending actions to the buyer, so he can send him the delivery details. i opih ei :Y):In this process, after the seller has received a 6
forts. Some of the relevant contributions in this domain are cited in this section.
gram when a violation is detected. Moreover, these contributions implement a monitor as a web service in addition to other web services. The originality of our work is the introduction of the monitor within concerned participants processes. In [11], a run-time event-based approach to deal with the problem of monitoring conformance of interaction sequences is presented. When a violation is detected, the program shows errors in dashboards. In [12], authors introduce an approach to verify the conformance of a web service implementation against a behavioral specication, through the application of testing. The Stream X-machines are used as an intuitive modeling formalism for constructing the behavioral specication of a stateful web service and a method for deriving test cases from that specication in an automated way. The test generation method produces complete sets of test cases that, under certain assumptions, are guaranteed to reveal all non-conformance faults in a service implementation under test. However, this approach only returns non-conformance faults and does not react dynamically against these errors. While, in [13], authors propose a monitoring framework of a choreographed service which supports the early detection of faults and decide whether it is still possible to continue the service. Authors in [?] have proposed service automata as a framework for enforcing security policies in distributed systems. They encapsulate the program in a service automaton composed of the monitored program, an interceptor, an enforcer, a coordinator and a local policy. The interceptor intercepts critical actions and passes them to the coordinator that determines whether the action complies the security policy or not and decides upon possible countermeasures then the enforcer implements these decisions. However the authors do not precise how to detect critical actions. 7
In this paper, we have introduced a formal approach allowing to automatically enforce a security policy on choreographed services. Indeed, we introduced a new calculus with an enforcement operator @P :The semantics of the proposed calculus insure that choreographed services can evolve only if it does not violate the enforced security policy. The originality of our work consists on the fact that we do not add a new web service as a monitor but rather we wrap the security policy inside the choreographed services.
11. Baouab, A., Perrin, O., Godart, C.: An optimized derivation of event queries to monitor choreography violations. In: ICSOC. (2012) 222{236 12. Dranidis, D., Ramollari, E., Kourtesis, D.: Run-time verication of behavioural conformance for conversational web services. In: ECOWS. (2009) 139{147 13. Ardissono, L., Furnari, R., Goy, A., Petrone, G., Segnan, M.: Monitoring choreographed services. In: Innovations and Advanced Techniques in Computer and Information Sciences and Engineering. (2007) 283{288 14. Fu, X., Bultan, T., Su, J.: Analysis of interacting bpel web services. In: WWW. (2004) 621{630