A,B , Ilaria Gabriele Costa
email: gabriele.costa@iit.cnr.it

Enforcing Private Policy via Security-by-Contract 1

Keywords: Private Policy Enforcement, Security-by-Contract, Distributed Connecting System

This work aims to investigate how the Security-by-Contract (SxC) paradigm, developed for providing security assurances to mobile applications, can be used for guaranteeing the security of communicating systems composed by several, heterogeneous components. These components need to communicate with each other by establishing direct, point to point connections. Direct connections can involve components sharing no common communication protocols and need a suitable interface. Enablers are in charge of providing these communication interfaces. Each component has a local security policy composed by a public and a private part. When a communication between two components has to be established, each component asks the enabler for providing a communication interface that respects its public policy. We exploit the Security-by-Contract approach for assuring that the application implementing the communication interface is always safe, i.e., it satisfies the security policies setted by components. Moreover, we present an extension of the Security-by-Contract for dealing with trust. Trust management is useful when one of the involved actors is considered to be potentially untrusted and the others want to measure its trust level.

INTRODUCTION

The growing diffusion of computational entities and their composition in networks has made security a critical issue in every phase of the software life-cycle. The modern scenarios present a complexity degree that only few years ago was unpredictable. Let us consider a communicating system composed by two classes of actors: components and enablers. Components are the end-users in our network. They can be both software agents (e.g., programs) or physical devices (e.g., mobile phones). Whenever two components want to communicate with each other they need to agree on a common protocol. If this is not possible, they ask to an enabler to provide them with a way to communicate. Enablers store information for creating/choosing an appropriate application for allowing the communication between different components. Moreover, each component has requires a local security policy to be always respected by applications running on it. Such security policy is the combination of two local security policies: a private policy and a public one. A private policy is a security policy hidden to the external world, e.g., because it speaks about some sensitive data. On the contrary, a public policy is made publicly accessible, e.g., because it does not involve information that the component considers to be private. Our goal is to guarantee that the communication between components is always secure, i.e., a provided application satisfies local security policies. We firstly provide a description of the threat models for that system. Secondly, we show that the Security-by-Contract paradigm [START_REF] Dragoni | Security-by-Contract (SxC) for software and services of mobile systems[END_REF] can be suitably applied for dealing with them. In doing this, we reduces our analysis to systems in which components trust to each other but they do not trust to enabler. The Security-by-Contract (SxC) framework was developed for providing security of mobile application. It is based on the idea of contract of an application. Roughly, a contract is a description of the behaviour of an application that comes together with the application itself. The typical scenario in which the SxC is applied consists in a device user defining his own security policy. When the user receives an application verifies whether its code and its contract actually match. If the check fails the user can decide to delete the application or to enforce the security policy on it by exploiting a proper enforcement infrastructure. Otherwise, the system can proceed and verifies whether the contract satisfies the user's policy. Once again, if this step fails the solution consists in enforcing the active policy on the execution. Finally, if the previous checks were positively passed, the application can be executed with no active runtime enforcement. In the simplest case, we assume to have a single enabler. Two components send to the enabler a communication request and their public security policies. The enabler provides an application, e.g., by synthesizing it on-the-fly or selecting it from an existing pull, with a contract describing its behaviour. Components expect to receive a contract that satisfies their public security policies. Remarkably, being not aware about the private security policies of the components, the enabler does not guarantee the application to comply with them. Each component involved in the communication checks whether the contract is compliant with both its own public and private policy. Going ahead, we also consider trust aspects by extending the Security-by-Contract paradigm with trust (SxCxT) [START_REF] Costa | Extending security-by-contract with quantitative trust on mobile devices[END_REF]. Indeed, we extend our scenario by assuming to have many enablers forming a cloud. Two components that want to communicate with each other send the request to the cloud of enablers. Similarly to the previous case, each enabler provides an application. However, in this scenario different enablers concur to provide their applications and the components decide which application will be adopted. Clearly, components can discriminate according to their levels of trust w.r.t. the enablers. Hereafter, assuming that components associate each enabler with a certain level of trust, we propose an integration of the SxC paradigm with a monitoring/enforcement infrastructure dealing with contracts. Contract monitoring allows for trust level management of enablers depending on their applications behaviour. Indeed let us assume that enablers are initially considered to be trusted. When components obtain some application provided by an enabler, they start monitoring it. Monitoring follows the execution an updates the trust value associated with the enabler depending on the actions fired by the application.

The paper is structured as follows: Section 2 recalls some background notions about the Securityby-Contract paradigm. Section 3 describes threat models for the considered system and Section 4 and 5 present the application of the SxC and SxCxT paradigms to threat models, respectively. Section 6 compares our work with what already exists in literature. Section 7 concludes the paper and describes some future work.

BACKGROUND

Security-by-contract (SxC) is a paradigm for providing security assurances to mobile applications [START_REF] Dragoni | Security-by-Contract (SxC) for software and services of mobile systems[END_REF]. According to [START_REF] Dragoni | Security-by-contract (SxC) for mobile systems or how to download software on your mobile without regretting it[END_REF], the basic idea of Security-by-Contract is to certify the code by binding it together with a contract. Loosely speaking, a contract contains a description of the relevant features of the application and the relevant interactions with the hosting platform. Relevant features include, among others, sensitive memory usage, secure and insecure web connections, user privacy protection, data confidentiality. By signing the code, developers certify its compliance with the stated claims on its security-relevant behaviour.

Definition 2.1:

A contract is a formal complete and correct specification of the behavior of the application for what concerns relevant security actions (e.g., Virtual Machine API call, Operating System Calls). It defines a subset of the traces of all possible security actions.

The second cornerstone of the SxC approach is the concept of policy. A mobile platform can specify its own contractual requirements through a customised policy. Moreover, policies can be user-defined. In both cases, if a contract matching the policy means that the corresponding application (provider) declares an acceptable behaviour.

Definition 2.2:

A policy is a formal complete specification of the acceptable behavior of applications to be executed on the platform for what concerns relevant security actions (e.g., Virtual Machine API calls, Operating System Calls). It defines a subset of the traces of all possible security actions.

The Security-by-Contract paradigm works as follows: when a client receives an application, it verifies whether the code and the contract actually match by using an evidence checking procedure. If the check fails, the user can decide to refuse (delete) the MIDlet or to enforce the security policy on it by exploiting a monitoring/enforcement infrastructure. The enforcement approach has been shown to be feasible on mobile devices exploiting several different techniques [START_REF] Castrucci | Enhancing java me security support with resource usage monitoring[END_REF][START_REF] Costa | Runtime monitoring for next generation java me platform[END_REF]. Otherwise, the system can proceed to verify whether the contract (correctly representing the application) satisfies the user's policy. Once again, if this step fails the solution consists in enforcing the active policy on the execution. Finally, if the previous checks were positively passed, the MIDlet can be executed with no active runtime monitor. The Contract-Policy matching function ensures that any security relevant behavior declared by the contract is also allowed by the policy. This matching step can be done w.r.t. different behavioural relation, e.g., language inclusion [START_REF] Desmet | Security-by-contract on the .net platform[END_REF] or simulation relation [START_REF] Greci | A framework for contract-policy matching based on symbolic simulations for securing mobile device application[END_REF]. Hence, the matching procedure formally guarantees that applications having a contract that is compliant with the active policy never violate it. Figure 1 shows the SxC pre-execution strategy.

THREAT MODELS

We introduce and detail several threat models. Let us consider a basic scenario in which two components want to establish a communication. For sake of simplicity, we assume that there is only one enabler in the network. To communicate, the two components send their requirements to the enabler. Then, the enabler produces a suitable application by taking it from a pre-compiled repository or synthesizing a new one on-the-fly. In this process we distinguish two security levels:

• Local security of each component of the network. Each component sets a local policy that has to be locally satisfied. Such security policy is the combination of a private policy and a public one. A private policy is a security policy that a component does not declare to the external world, e.g., a policy that speaks about sensitive data. On the contrary, a public policy is a policy that the component consider freely deliverable, e.g., a policy that does not involve private information. Clearly, two limit cases exist: i) a component has only a private policy or ii) it sets only a public policy. • Global security of the distributed system. Interactions among components and enablers must satisfy some security policy describing the correct behaviour of the distributed system as a whole.

Focusing on trust aspects, the following sub-cases arise:

• The two components involved in the communication trust each other but they do not trust the enabler. • Each component involved in the communication trusts the enabler but does not trust the other component. • All actors (components and enabler) trust on each other.

• No trust relationships exist between two components or between a component and the enabler.

SECURITY-BY-CONTRACT FOR CONNECTING COMPONENTS

We show how to apply the SxC paradigm for providing network components with local security. As we said in Section 3, here we consider to have two components, trusting each other, that interact with an untrusted enabler.

Private and Public Security Policy

First of all, we investigate on the possible relationship existing between public and private policies defined on each single component. Three cases arise: 1. The public policy is a generalization of the private policy. This means that the public policies allows more execution than the private one. A particular instance of this case occurs when only the private policy has been defined. 2. The private policy is a generalization of the public one. Referring to the notion of compliance used in the SxC paradigm, this case means that whenever the public policy is satisfied also the private one will be. An instance of this case occurs when no private policy has been setted on the component. 3. Private and public policy partially overlap. There exists at least one execution that satisfies both the private and the public policy.

Some examples can clarify the above classification.

Example 4.1: Imagine a component requiring a connector and declaring the following, informally defined, policies:

• Ppub: "Always connect to the same host"

• Ppriv: "Encrypt every message with key k" As it refers to some sensitive data, i.e., k, the component can be interested in keeping Ppriv secret. Clearly, these two policies do not imply each other (unencrypted messages can be delivered to a single host or correctly encrypted messages can be sent to multiple hosts). However, there are executions satisfying both of them, e.g., a single, encrypted message is sent. This example belongs to the third case introduced above.

Example 4.2: Imagine now a component similar to the previous one, but defining a different private policy.

• P pub : "Always connect to the same host".

• P priv : "Connect only with host h".

Here, the set of behaviours accepted by P priv also satisfies P pub . Hence, we are in the second case.

In addition to the relation existing between private and public security policy, we must also investigate the relation among security policies and applications contract. All possible relations are summarized in Figure 2. In the following, we assume that the public policy generalizes the private policy (case (b) in Fig. 2).

The relationship between the policy and the contract drives the Security-by-Contract run-time strategy. Figure 3 shows schematically the system behaviour.

If the contract complies with the private policy (M in figure), the system monitors the application run-time compliance w.r.t. its contract. Instead, if the contract does not comply with the private policy (E in figure), the private policy is enforced on the executing application. Note that we are intentionally ignoring the case in which private policy and contract have no intersection. Indeed, whenever this happens, the enforcement process forces the execution to generate only empty traces.

Enforcing Private Security Policy through SxC

Let us consider the scenario in Figure 4. Two components want to start a conversation and ask an enabler for a suitable application, i.e., a connector. Each component has its own security policy composed by a private and a public part. Both components declare a public policy that generalizes the private one.

Let P 1 and P 2 be the public policies of the two components. To communicate, both components send a connection request and their local public policies to the enabler. If possible, the enabler answer by providing the components with an application. This application will be a mobile code that the enabler annotated with a contract C denoting its behaviour. By design, when the enabler returns a contract C then it also declare, under its own responsibility, that C satisfies both P 1 and P 2 .

After retrieving the application, the components must verify how its contract fits with their private policies (P priv 1 and P priv 2 respectively). Since P pub (1/2) generalise P priv (1/2) components only need to check contract against private policies. If the application is accepted from both the components, it is used to establish the communication. An instance of this scenario arises when both components declare no public security policy. Since there is no assumption about the application contract that the enabler returns, this case reduces to the original SxC scenario for mobile devices [START_REF] Dragoni | Security-by-Contract (SxC) for software and services of mobile systems[END_REF]. However, when a component receives an application it decides which monitoring/enforcement configuration must be activated. Firstly, the component verifies whether the code comes from a trusted source. If the check fails then the component can decide to refuse the application or to enforce the security policy on it (Enforce Policy). Otherwise, the component verifies whether the contract (considered to correctly denote the application) satisfies the private security policy (Contract-Policy Matching [START_REF] Greci | A framework for contract-policy matching based on symbolic simulations for securing mobile device application[END_REF] at deployment-time). If this step fails the solution consists in enforcing the active policy on the execution and, possibly, also monitoring the application contract. In this scenario, the contract monitoring configuration can be activated on a statistical base in order to record possible application misbehaviours leading to a trust weight adjustment. Finally, if the previous checks were positively passed, the communication is established and only the contract monitoring is turned on.

ENABLERS TRUST MANAGEMENT

We detail our trust management-oriented extension of the SxC paradigm, hereafter denoted by SxCxT [START_REF] Costa | Extending security-by-contract with quantitative trust on mobile devices[END_REF]. The main novelty of our technique consists in adding a new component to the standard architecture. This module is responsible for contract monitoring and reacts to contract violations by updating the trust level of the involved enabler. This could be useful, for instance, if we consider more than one enabler in the system. Figure 6 shows the application life-cycle. In model, the Check Evidence step has been replaced by a check on the enabler trust measure (Trusted Provider). This check discriminate between applications running guarded by a mere policy enforcement and applications being contractmonitored. Whenever the contract satisfies the local public policy, two possible relations with the private policy arise:

1. The contract satisfies the local private security policy. In this case our monitoring/enforcement infrastructure is required to monitor only the application contract. Indeed, under these conditions, contract adherence also implies private policy compliance. If no violation is detected during the execution then the application worked as expected.

Otherwise, we discovered that a trusted party provided us with a fake contract. Our framework reacts to this event by reducing the level of trust of the indicted provider and switching to the policy enforcement modality. 2. The contract does not satisfy the local private security policy. Since the contract declares some potentially undesired behaviour, policy enforcement is turned on. Similarly to a pure enforcement framework, our system guarantees that executions are policy-compliant. However, monitoring contract during these executions can provide a useful feedback for better tuning the trust vector. Hence, our framework also allows for a mixed monitoring and enforcement configuration. This configuration is statistically activated with a certain probability. Several strategies are possible for deciding the probability to activate the monitoring procedure, e.g., using a fixed value or a function of the current trust level.

Note that, in the second scenario, the monitoring component plays a central role. Indeed, a contract violation denotes that a trusted provider released a fake contract. The reaction of our system to this event is a instant correction of the trust measures. We outline how trust measures assigned to security assertions can be adjusted by our contract monitoring strategy. Trust measures associated with an enabler mainly concern on the contract goodness. Hence, updated trust measures will influence future interactions with an enabler and its applications. In other words, our system penalizes enablers when their contracts do not specify the correct applications behaviour.

Here we present a possible extension of the monitoring/enforcement infrastructure model proposed in [START_REF] Costa | Runtime monitoring for next generation java me platform[END_REF]. The monitoring/enforcement infrastructure mainly consists of two components: a Policy Decision Point (PDP) and Policy Enforcement Points (PEPs). Roughly, the PDP holds the actual security state and is responsible for accepting or refusing new actions. Actions are delivered to the PDP by PEPs that in charge of intercepting security-relevant operations done by the application. When the application tries to run a monitored command, it stimulates a corresponding PEP that suspends the execution and fires the action to the PDP. The PDP evaluate the action against the its current security state and answer allowing or denying the permission to proceed. Finally the PEP enforce the PDP decision by running or aborting the operation under analysis.

In our system the PDP is also responsible for the contract monitoring operations and for the trust vector updating.

According to [START_REF] Castrucci | Enhancing java me security support with resource usage monitoring[END_REF][START_REF] Costa | Runtime monitoring for next generation java me platform[END_REF], we assume that both contracts and policies are specified through the same formalism. Hence, the policy enforcement configuration of the PDP keeps unchanged. The PDP must load connector contracts as well as local private security policies dynamically. Moreover, it must be able to run under three different execution scenarios (Fig. 6): policy enforcement enabled, contract monitoring enabled or both. The base enforcement scenario (execution scenario 1) is actually unchanged w.r.t. the standard usage of the classical PDP. Hence, no contract monitoring nor trust management operations are involved.

Main interest resides in the other two scenarios. The contract monitoring scenario applies to application carrying a contract released by a trusted enabler (Section 5.1).

Similarly to the policy enforcement strategy, PEPs send action signals to the PDP. An important difference is that the PDP keeps in memory the program events trace. When a signal arrives, the PDP checks whether it is consistent with the monitored contract. If the contract is respected then the internal monitoring state is updated and the operation is allowed. Otherwise, if a violation attempt is detected, the PDP reacts by changing its state. The first consequence of a contract violation is a decreasing of the trust weight of the involved enabler.

Secondly, the PDP switches its state from contract monitoring to policy enforcement configuration. Since an instance of the policy is always present, this operation does not imply a serious computational overhead. Afterwards, the policy state is updated using the execution trace recorded during the monitoring phase. This step, that can be time consuming, is necessary for verifying whether, breaking the contract, the application has also violated the policy. However, this computational cost, being the consequence of an extraordinary event, must be paid at most once. Indeed, when the PDP is both monitoring a contract and enforcing a policy, the current policy state is known. Finally, the execution continues with the PDP enforcing the policy starting from the last action, that is the event breaking the contract. Figure 7 and Figure 8 show the behaviour of the monitor/enforcement infrastructure performing the contract monitoring task in the two previously discussed scenarios. Summing up, both execution scenario 2 and 3 check contract violations through the contract monitoring strategy described above and update enablers trust level. Such updates will influence future interactions with applications and enablers.

In this way our system gains experience and refines its interactions with enablers by ignoring applications coming from malicious enablers. Moreover, the executions are always kept safe by the security enforcement infrastructure.

RELATED WORK

In literature there not exist a lot of work on possible extension of the Security-by-Contract paradigm for dealing with trust and, in particular, that integrate policy enforcement and trust management, especially for mobile code. An attempt of integration of trust management and fine grained access control in Grid Architecture can be found in [START_REF] Koshutanski | A fine grained and x.509 based access control system for globus[END_REF] where it is proposed an access control system the enhances the Globus toolkit with a number of features. This copes with the fact that access control policies and access rights management becomes one of the main bottleneck using Globus for sharing resource in a Grid architecture. Along this line of research [START_REF] Colombo | Fine grained access control with trust and reputation management for globus[END_REF] presents an integrated architecture, extending the previous one, with an inference engine managing reputation and trust credentials. This framework is extended again in [START_REF] Koshutanski | Enhancing grid security by fine-grained behavioral control and negotiation-based authorization[END_REF] where it is introduced a mechanism for trust negotiating credential to overcome scalability problem. In this way the framework provided preserves privacy credentials and security policy of both users and providers. Even if the application scenario and the implementation is different, the basic idea of considering the trust as a metrics for deciding the reliability of an application provider. Also [START_REF] Liu | An incentive compatible reputation mechanism for ubiquitous computing environments[END_REF] presents a reputation mechanism to facilitate the trustworthiness evaluation of entities in ubiquitous computing environments. It is based on probability theory and supports reputation evolution and propagation. The proposed reputation mechanism is also implemented as part of a QoS-aware Web service discovery middleware and evaluated regarding its overhead on service discovery latency. On the contrary, our approach is not a probabilistic. We provide a method according to we update the level of trust of an application provider.

CONCLUSION AND FUTURE WORK

Here we have investigate on how using the Security-by-Contract paradigm for enforcing private policy in a communicating system composed by several components that ask to communicate with each other. Firstly, we have investigated the possible threat models if the system and then we showed an application of SxC for establishing a secure communication among components of a network by guaranteeing that the application for communication is secure, i.e., it works according the security policies required by components. Secondly, we afterwards extended the SxC approach for managing trust measures by exploiting a contract monitoring procedure. Furthermore, we presented how this extension is useful for the considered system in which several actors are involved and measuring trust could be needed. Many future directions are viable. Indeed we aim to adapt both the SxC and the SxCxT paradigms to all possible threat models we have pointed out in the introduction. Furthermore, mainly our trust management strategy is still a work in progress. Currently, trust weights can only decrease monotonically as a consequence of contract violations with the only exception of a direct intervention of the user, see e.g., [START_REF] Naqvi | Fine-Grained Continuous Usage Control of Service Based Grids -The GridTrust Approach[END_REF]. Moreover, quantitative representation of this adjustment we consider to present in the future work.

Figure 1 :

 1 Figure 1: The Security-by-Contract Application life-cycle [7].

Figure 2 :

 2 Figure 2: A graphical representation of possible relations among Private policy, Public policy and Contract.

Figure 3 :

 3 Figure 3: A graphical representation of scenario (b). M denotes contract monitoring and E policy enforcement.

Figure 4 :

 4 Figure 4: Secure application.

Figure 5 :

 5 Figure 5: Secure and Trusted application

Figure 6 :

 6 Figure 6: The Extended Security-by-Contract Application life-cycle.

Figure 7 :

 7 Figure 7: Mixed Enforcement/Monitoring strategy.Figure 8: Pure Monitoring strategy.

Figure 8 :

 8 Figure 7: Mixed Enforcement/Monitoring strategy.Figure 8: Pure Monitoring strategy.

Work partially supported by EU project FP7-231167 CONNECT (Emergent Connector for Eternal Software Intensive Networked Systems) and by the EU project FP7-214859 Consequence (Context-aware data-centric infor-mation sharing).


Gabriele Costa
email: gabriele.costa@iit.cnr.it

Pierpaolo Degano
email: degano@di.unipi.it

Fabio Martinelli
email: fabio.martinelli@iit.cnr.it

Secure Service Composition with Symbolic Effects

Local policies represent security properties that are applied to (parts of) programs or services. They are amenable for developers since they provide for a full compositionality (through scope nesting), for a simple, automaton-like structure and for a direct enforcing through a corresponding execution monitor. Compliance w.r.t. local policies is statically verified against a safe over-approximation of all the possible execution traces, namely a history expression. Given a service, a safe type and effect system extracts a history expression, from which a viable composition plan can be automatically produced. Viable plans drive executions that never rise policy exceptions. Our main contribution consists in defining a type and effect system that also deals with open systems. We extend the syntax of a service-oriented version of the λcalculus, namely λ req , with resources and external branching operators. Then, we safely over-approximate the possible runtime behaviour of services collecting partial information on the relationship between the program flow and the actual resources. Indeed, the history expressions obtained in this way are compact, rather accurate and able to derive viable plans in most cases.

I. INTRODUCTION

The main purpose of the history-based approach to security is to discriminate between legal and illegal execution traces [START_REF] Abadi | Access control based on execution history[END_REF]. We can classify most history-based techniques in two different groups: static verification and run-time enforcement. In the first case, the compliance with the security policy is checked on a model describing (a suitable approximation of) all the possible behaviours of a system. The other approach mainly consists in deploying a monitor that is responsible for preventing the actual execution trace from violating the security policy. Both of them have been widely studied (e.g. see [START_REF] Skalka | History effects and verification[END_REF], [START_REF] Besson | Model checking security properties of control flow graphs[END_REF], [START_REF] Schneider | Enforceable security policies[END_REF], [START_REF] Ligatti | Edit automata: enforcement mechanisms for run-time security policies[END_REF]) and many results on their features are present in the literature. An approach based on local policies [START_REF] Bartoletti | History-based access control with local policies[END_REF] candidates to be a mixed one to the problem of security. These policies are defined through usage automata, namely a variant of nondeterministic finite-state automata (NFAs) parameterized over system's resources. Usage automata are intuitive, can be defined via visual editing and do not require specific technical skills. Policies compose each other through scope nesting and apply also to higher-order terms (e.g. mobile applications an service composition). The compliance with policies is statically verified through model checking. If a system passes this static check, then it can run with no security enforcement. Otherwise, the necessary policies give automatically rise to a reference monitor associated with the guarded code (e.g. via instrumentation). In [START_REF] Bartoletti | Securing Java with local policies[END_REF] Java has been extended with local policies showing the feasibility of this approach on a real-world system.

The benefits of verifying history expressions extend to the orchestration of services in a closed world [START_REF] Bartoletti | Planning and verifying service composition[END_REF], [START_REF] Bartoletti | Secure service orchestration[END_REF]. The orchestrator produces a plan, with an associated allinclusive history expression. If this approximation of the whole service network is statically proved to comply with the required policies, then the composed service is secure.

In many cases we would like to also analyse open networks, i.e. networks having unspecified participants. We give an intuition through an example.

Example 1. Consider the four-services network in Figure I.

A service is represented by a rounded box, and is hosted at location ℓ i . During its execution, the service at ℓ 0 calls another service, with parameter y. The call is subject to a policy ϕ. Suppose that the three services ℓ 1 , ℓ 2 and ℓ 3 are compatible with the request ρ. Imagine now that the policy ϕ says: "callee must never do action β on the (globally known) resource r and can do α only on r". Completing the network with clients binding y to some actual resource we can check which services can be safely associated with ρ for each possible composition plan. In this example it is easy to verify that ℓ 3 always complies with ϕ. Exploiting this observation we can define a viable plan without any knowledge about the structure of clients (that could be statically unpredictable). Note that this plan is partial because it only concerns the four services considered, regardless of the environment in which they will operate.

Here, we extend the results of [START_REF] Bartoletti | Planning and verifying service composition[END_REF], [START_REF] Bartoletti | Secure service orchestration[END_REF] on networks that are open in the sense mentioned above. In particular, we will single out partial plans that involve parts of the known network and that can be safely adopted within any operating context. We say that a plan is partial if it is partially defined over the set of existing requests. For simplicity, here we restrict our analysis to stateless security policies, i.e. they do not depend on the previous execution history, but only speak about the intended behaviour of called services.

The paper is structured as follows. In Section II we give the syntax and semantics of λ req . In Section III we introduce history expressions and our type and effect system. Finally, Section IV concludes the paper.

II. SERVICE STRUCTURE

The programming model for service composition based on λ req was first introduced in [START_REF] Bartoletti | Planning and verifying service composition[END_REF]. Its syntax resembles the classical call-by-value λ-calculus with two main differences: security framing and service request.

Service networks are set of services. Each service e is hosted in a location ℓ. As expected, we assume that there exists a public service repository Srv. An element of Srv has the form e ℓ : τ H -→ τ ′ , where e ℓ is the code of the service, ℓ is a unique service location (sometimes used to denote the service itself), τ -→ τ ′ is the type of e ℓ , and H is the effect of e ℓ (see Section III-A).

A. Syntax

The syntax of λ req is in Table I. The expression * represents a fixed, closed, event-free value. Resources, ranged over by r, r ′ , belong to finite, statically defined classes R, R ′ . Access events α, β are side effects, parametrized over resources.

Function abstraction and application follow the classical syntax (we use z in λ z x.e as a binding to the function in e). Security framing applies the scope of a policy ϕ to a program e. Service request requires more attention. We state that services can not be directly accessed (for instance using a public name or address). Clients invoke services through security framing req ρ τ → τ ′ service request their public interface, i.e. their type. The label ρ is a unique identifier associated with the request. Since both τ and τ ′ can be higher-order types, we can model simple value-passing interaction, as well as mobile code scenarios. We use v to denote values, i.e. resources, variables, abstractions and requests. Moreover, we introduce the usual abbreviations: λx.e = λ z x.e with z ∈ f v(e), λ.e = λx.e with x ∈ f v(e) and e; e ′ for (λ.e ′ )e.

Here we make explicit the conditions of branching, similarly to [START_REF] Boreale | A symbolic semantics for the pi-calculus[END_REF]. Briefly, we check equality between resources, and we have negation and conjunction.

Definition 1. (Syntax of guards) g, g ′ ::= true | [x * = y * ] | ¬g | g ∧ g ′
where x * ,y * range over variable and resource names.

We use f alse as an abbreviation for ¬true, [x = y] for ¬ [x = y] and g ∨ g ′ for ¬(¬g ∧ ¬g ′ ). We also define as expected an evaluation function B mapping guards into boolean values, namely {tt, ff }.

E.g. B([x = x]) = tt and B([x = y]) = ff if x = y.
In our model we assume resources to be uniquely identified by their public name, i.e. r and r ′ denote the same resource if and only if r = r ′ .

We now introduce our two working examples.

Example 2. Let e be a service that inputs an address taken from the set of network addresses Addr = {a 1 , . . . , a n }.

Then e verifies that the current address is a trusted one, i.e. checks if it belongs to a set TAddr ⊆ Addr. If so, e sends some private message to the trusted address, otherwise e terminates. We model the service e in this way:

e = λx.if [x ∈ TAddr] then send(x) else * where [x ∈ TAddr] = a∈TAddr [x = a]
Example 3. Consider now a slight variant of the previous service. Now e only sends messages to clients having a sponsor inside the service network. A sponsor is a service e ′ that, given an address a ∈ Addr, answers with a value in S = {A, R} where A (R resp.) means that e ′ accepts (refuses) the sponsorship for a. Then a possible implementation for e is:

e = λx.(λy.if [y = A] then send(x) else * )((req ρ Addr → S)x)
Note that e needs to know nothing about sponsors and their implementation.

B. Operational semantics

Clearly, the run-time behaviour of a network of services depends on the way they interact. As we already mentioned, requests do not directly refer to a specific service that will be actually invoked during the execution, but to its type, only. A plan resolves the requests by giving a finite, total mapping from requests to services locations. Needless to say, different plans lead to different executions. A plan is said to be valid if and only if the execution it drives complies with all the active security policies. A service network can have many, one or even no viable plans.

As expected, we assume that services can not be composed in a circular way. This condition amounts to say that there exists a partial order relation ≺ over services. We define Srv⌋ ℓ = {e ℓ ′ : τ ∈ Srv | ℓ ≺ ℓ ′ } as the sub-network that can be seen from a service hosted at ℓ.

A computational step of a program is a transition from a source configuration to a target one. In our model, configurations are pairs η, e where η is the execution history, that is the sequence of action events done so far, and e is the expression under evaluation.

The operational semantics of λ req is given in Table II. Given a plan π we can evaluate λ req expressions, i.e. services, accordingly with these rules.

Briefly, an action α(r) is appended to the current history (possibly after the evaluation of its parameter), a conditional branching chooses between two possible executions (depending on its guard), a security framing checks the current history before allowing the next step, an application works as usual and a service request retrieves the service that the current plan π associates with ρ.

III. TYPE AND EFFECT SYSTEM

We now introduce the type and effect system for λ req . Our system inherits its structure from [START_REF] Bartoletti | Planning and verifying service composition[END_REF] introducing two main improvements: guarded effects and a new typing rule, namely strengthening.

(S-Frm1) η, e →π η ′ , e ′ η |= ϕ η, ϕ[e] →π η ′ , ϕ[e ′ ] (S-Frm2) η |= ϕ η, ϕ[v] →π η, v (S-App1) η, e1 →π η ′ , e ′ 1 η, e1e2 →π η ′ , e ′ 1 e2 (S-App2) η, e2 →π η ′ , e ′ 2 η, ve2 →π η ′ , ve ′ 2 (S-App3) η, (λzx.e)v →π η, e{v/x, λzx.e/z} (S-Req) el : τ H -→ τ ′ ∈ Srv⌋ ℓ π(ρ) = l η, (req ρ τ → τ ′ )v →π η, elv
A. History expressions History expressions will be used to denote set of histories. They are defined through the following abstract syntax, which extend those of [START_REF] Bartoletti | Planning and verifying service composition[END_REF].

Definition 2. (Syntax of history expressions)

H, H ′ ::= ε empty h variable α(r) access event H • H ′ sequence H + H ′ choice ϕ[H]
security framing µh.H recursion gH guard A history expression can be empty (ε), a single access event to some resource (α(r)) or it can be obtained either through sequential composition (H •H ′ ) or non-deterministic choice (H + H ′ ). Moreover, we use safety framing ϕ[H] for specifying that all the execution histories represented by H are under the scope of the policy ϕ. Additionally, µh.H (where µ binds the free occurrences of h in H) represents recursive history expressions. Finally, we introduce guarded histories, namely gH (where g respects the syntax of guards

ε σ δ = ∅ h σ δ = δ(h) α(r) σ δ = {α(r)} H • H ′ σ δ = H σ δ H ′ σ δ H + H ′ σ δ = H σ δ ∪ H ′ σ δ gH σ δ =  H σ δ if σ |= g ∅ otherwise ϕ[H] σ δ = ϕ ˆ H σ δ ˜ µh.H σ δ = S n>0 f n (! )
where

f (X) = H σ δ{X/h}
given in Def. 1).

The denotational semantics of history expressions (given in Table III) maps a history expression H to a set of histories H. The domain H is the lifted complete partial order of sets of histories [START_REF] Winskel | The formal semantics of programming languages[END_REF]. Sets are ordered by (lifted) inclusion ⊆ ⊥ (where ∀H.⊥ ⊆ ⊥ H and

H ⊆ ⊥ H ′ whenever η ∈ H ⇒ η ∈ H ′ ).
In order to define the semantics of history expressions we need a couple of auxiliary notions. An environment δ binds variables (h, h ′ , . . .) to history expressions (H, H ′ , . . .) and a substitution σ maps variable names (x, y, . . .) to variable names or resources (x, y, . . . or r, r ′ , . . .). Given δ and σ, the semantic function maps a history expression to a corresponding set. As expected, ε denotes the empty set under any configuration and α(r) denotes the singleton containing only α(r). The semantics of a sequential composition H •H ′ evaluates to the set of histories obtained by juxtaposing the histories denoted by H and by H ′ . Non-deterministic choice H + H ′ denotes the union of the two sets corresponding to H and H ′ respectively. The semantics for gH is a little more tricky. We assert gH to define two distinct sets: H σ δ , if σ satisfies g (we write σ |= g if and only if B(gσ) = tt), or ∅ otherwise. The semantics of µh.H is the least fixed point of the function f (see [START_REF] Bartoletti | History-based access control with local policies[END_REF] for further details).

B. Typing relation

Before introducing a type and effect system for our calculus, we need some auxiliary definitions.

The relation ⊑ σ is a partial order between history expressions defined as:

H ⊑ σ H ′ if and only if H σ ∅ ⊆ ⊥ H ′ σ ∅ We write H ⊑ H ′ when ∀σ.H ⊑ σ H ′ .
Type environments are defined in a standard way as mappings from variables to types. Types can be either base types, i.e. unit or resources, or higher-order types τ

(T-Abs) Γ; x : τ ; z : τ H -→ τ ′ , H ⊢g e : τ ′ Γ, ε ⊢g λzx.e : τ H -→ τ ′ (T-App) Γ, H ⊢g e : τ H ′′ --→ τ ′ Γ, H ′ ⊢g e ′ : τ Γ, H • H ′ • H ′′ ⊢g e e ′ : τ ′ (T-Frm) Γ, H ⊢g e : τ Γ, ϕ[H] ⊢g ϕ[e] : τ (T-If) Γ, H ⊢ g∧g ′ e : τ Γ, H ⊢ g∧¬g ′ e ′ : τ Γ, H ⊢g if g ′ then e else e ′ : τ (T-Req) I = {H | e ℓ ′ : τ H -→ τ ′ ∈ Srv⌋ ℓ } Γ, ε ⊢g req ρ τ → τ ′ : τ P i∈I H i ------→ τ ′ (T-Wkn) Γ, H ⊢g e : τ H ⊑ H ′ Γ, H ′ ⊢g e : τ (T-Str) Γ, H ⊢g e : τ g ⇒ g ′ Γ, g ′ H ⊢g e : τ
A typing judgement (Table IV) has the form Γ, H ⊢ g e : τ and means that the expression e is associated with the type τ and the history expression H. The proposition g records information about the branching path collected during the typing process.

Rules for * , resources and variables are straightforward. An event has type 1 and produces a history that is the one obtained from the evaluation of its parameter increased with the event itself. Note that, since the class of resources is finite, we can only have a finite number of instantiations of an event 1 . An abstraction has an empty effect and a functional type carrying a latent effect, i.e. the effect that will be produced when the function is actually applied. The application moves the latent effect (labelling the function type) to the actual history expression and concatenates it with the actual effects according the call-by-value semantics. Security framing extends the scope of the property ϕ to the effect of its target. The rule for conditional branching is new. It says that if we can type e and e ′ to the same τ generating the same effect H, then we can extend τ and H to be the type and effect of the whole expression. Moreover, in typing the sub-expressions we take into account g ′ and its negation, respectively. Similarly to abstractions, service requests have an empty effect. However, the type of a request is obtained as the composition of all the types of the possible servers. In particular, the resulting latent effect is the (unguarded) non-deterministic choice among them. Observe that we only accept exact matching for input/output types (see [START_REF] Bartoletti | Planning and verifying service composition[END_REF] for a different composition of types). The last two rules are for weakening and strengthening. The first states that is always possible to make a generalisation of the effect inferred from an expression e. Finally, (T-Str) applies a guard g ′ to an effect H provided that g ⇒ g ′ (if and only if ∀ σ.σ |= g ⇒ σ |= g ′ ). This rule says that we can use the information stored in g for wrapping an effect in a guarded context. ----------------→ 1 .

. .

x : τ, ε ⊢true e ′ : R

[x=r]α(R)+[x =r]β(R) ----------------→ 1 ∅, ε ⊢true e : τ ε -→ (R [x=r]α(R)+[x =r]β(R) ----------------→ 1)
where e ′ = if [x = r] then λy.α(y) else λy.β(y).

Our type and effect system produces history expressions that approximate the run-time behaviour of programs. The validity of our approach resides in producing history expressions safely. We say a type and effect system to be safe if each trace produced by the execution of a program is always denoted by the history expression obtained typing it. To prove type and effect safety we need the following results. All the proofs of our results can be found in [START_REF] Costa | s web page[END_REF].

Lemma 1. If Γ, H ⊢ g e : τ and g ′ ⇒ g then Γ, H ⊢ g ′ e : τ In words, Lemma 1 states that type and effect inference is closed under logical implication for guards.

Lemma 2. (Subject reduction)

Let Γ, H ⊢ g e : τ and η, e → * η ′ , e ′ . For each g ′ such that g ′ ⇒ g, if Γ, H ′ ⊢ g ′ e ′ : τ then ∀σ.σ |= g ′ =⇒ η ′ H ′ σ ⊆ η H σ Lemma 2 says that history expressions are preserved by programs execution.

Then, the type safety is guaranteed by the following theorem. Unlike the type system of [START_REF] Bartoletti | History-based access control with local policies[END_REF], the presence of the rule (T-Str) makes it possible to discard some of the denoted traces. These traces correspond to executions that, due to the actual instantiation of formal parameters, can not take place. Consequently, our type and effect system produces more compact history expressions than those of [START_REF] Bartoletti | History-based access control with local policies[END_REF]. This has several advantages, and we mention here a couple of them. First, having small history expression reduces the search space contributing to speed up verification algorithms. Secondly, it removes possible false negatives raising from traces that violate the active policy but will never be produced at runtime.

IV. CONCLUSION AND RELATED WORK

We extended the type system of λ req , a service-oriented version of the call-by-value λ-calculus, with rules for inferring guarded history expressions. Our approach produces a finer, but still safe, static approximation of the possible run-time behaviours than those of [START_REF] Bartoletti | History-based access control with local policies[END_REF]. Although our type system performs similarly to others in case of closed service networks, we showed that it can be successfully applied to partially undefined networks of services. This assumption seems to be realistic. Indeed an "a priori" knowledge of clients is not always available to services at deploy-time. On the contrary, a service could be interested in verifying which compositions are viable only considering the part of the service network it is aware of at a certain time.

Many improvements are possible on the present proposal. For instance, exploiting the correspondence between history expressions and basic process algebras (BPAs [START_REF] Bergstra | Algebra of communicating processes with abstraction[END_REF]), we could apply the approach of [START_REF] Boreale | A symbolic semantics for the pi-calculus[END_REF] for defining a symbolic transition system on which some behavioural analysis are available. Additionally, it would be important studying the minimal necessary conditions under which partial plans are fully compositional. Indeed, such a result would allow the orchestration strategy to be distributed, so reducing the complexity of this problem.

Verifying security properties of orchestrations is a major issue in service oriented paradigms and many authors have studied it. However, to the best of our knowledge, little work has been done on partial orchestration.

In [START_REF] Bravetti | Contract-driven implementation of choreographies[END_REF] the authors present a framework for contract-based creation of choreographies. Roughly, they use a contract system for finding a match between contracts and choreographies. In this way they are able to find whether a given contract, declared by a service joining the network, is consistent with the current choreography. However, this framework exploits a global knowledge about the network structure while our model aims to infer partial compositions, whenever they exist. Actually, we want to verify whether a service can be composed with (a visible part of) the network respecting the active security policies.

For defining contracts, Castagna et al. [START_REF] Castagna | A theory of contracts for web services[END_REF] use a variant of CCS with internal and external choice operators [START_REF] De | Ccs without tau's[END_REF]. A subcontract relation guarantees that the choreography always respects the contracts of both client and service. Nevertheless, this approach assumes that clients always know the contract for a request and it is focused on finding a satisfactory composition with some available service. Since the composition depends on the possible instantiations of a service, such a contract could be unavailable during the analysis phase. In this sense, our technique overcomes this limitation by producing symbolic partial plans that will be instantiated over actual resources.

Busi et al. [START_REF] Busi | Choreography and orchestration: A synergic approach for system design[END_REF] propose an analysis of service orchestration and choreography. In their work, the validity of the orchestration of services is a consequence of its conformance respect to the intended choreography. The main difference with our work consists in the approach to choreography. Indeed, they start from a pre-defined choreography and verify the validity of an orchestration. Instead, our approach aims to check partial service composition without relying on any global orchestrator.

In [START_REF] Martinelli | Synthesis of web services orchestrators in a timed setting[END_REF] a framework for the synthesis of orchestrators is presented. This technique consists in automatically producing an orchestrator guaranteeing a service composition to respect the desired security policy. This approach defines a composition that complies with the client's policy. Since our method produces partial compositions that respect all the involved policies (on both clients and servers), it seems to be more general. However, as [START_REF] Martinelli | Synthesis of web services orchestrators in a timed setting[END_REF] generates dynamic orchestrators, the two systems work under completely different assumptions.

  This research has been partially supported by EU-FETPI Global Computing Project IST-2005-16004 SENSORIA (Software Engineering for Service-Oriented Overlay Computers), EU project FP7-214859 CONSEQUENCE (Context-aware data-centric information sharing) and EU project FP7-231167 CONNECT (Emergent Connectors for Eternal Software Intensive Networked Systems).

Figure 1 .

 1 Figure 1. An open service network. Request ρ can be satisfied by three services (ℓ 1 , ℓ 2 and ℓ 3 )

Example 4 .

 4 Consider the service introduced in Example 2. If it is invoked with parameter a ∈ TAddr starting from an empty trace, its execution is: ε, (e a) → ε, if [a ∈ TAddr] then send(a) else * → ε, send(a) → send(a), *

H-

  → τ ′ annotated with the history expression H. Definition 3. (Types and type environments) τ, τ ′ ::= 1 | R | τ H -→ τ ′ Γ, Γ ′ ::= ∅ | Γ; x : τ Table IV TYPING RELATION (T-Unit) Γ, ε ⊢g * : 1 (T-Res) Γ, ε ⊢g r : R (T-Var) Γ, ε ⊢g x : Γ(x) (T-Ev) Γ, H ⊢g e : R Γ, H • P r∈R α(r) ⊢g α(e) : 1

Example 5 .Example 6 . 1 xExample 7 . 1 x 1 x 1 x

 5617111 Let e be the service introduced in Example 2, then the following derivation is possible (dots stands for trivial or symmetrical derivations) . . . x : Addr, send(Addr) ⊢ [x∈TAddr] send(x) : 1 x : Addr, [x ∈ TAddr] send(Addr) ⊢ [x∈TAddr] send(x) : 1 . . . x : Addr, [x ∈ TAddr] send(Addr) ⊢true IF : 1 ∅, ε ⊢true e : Addr[x∈TAddr]send(Addr) -------------→ 1 where send(Addr) = n i=1 send(a i ) and IF = if [x ∈ TAddr] then send(x) else * . Consider now e to be the service of Example 3. For the rightmost expression we can derive x : Addr, ε ⊢true req ρ Addr -→ S : τ x : Addr, ε ⊢true x : Addr x : Addr, P i∈I H i ⊢true (req ρ Addr -→ S)x : S where τ = Addr P i∈I Hi -----→ S. Moreover we can derive . . . x : Addr; y : S, [y = A] send(Addr) ⊢ [y=A] send(x) : 1 . . . x : Addr; y : S, [y = A] send(Addr) ⊢true IF : : Addr, ε ⊢true λy.IF : S [y=A]send(Addr) -----------→ 1 with IF = if [y = A] then send(x) else * . Combining the two we obtain ∅, ε ⊢ true e : Addr H -→ 1 where H = i∈I H i • [y = A] send(Addr). Consider now the term e = λx.if [x = r] then λy.α(y) else λy.β(y) and let R = {r, s} be the set of resources compatible with actions α and β. Then the following derivation is possible x : τ ; y : R, α(R) ⊢ [x=r] α(y) : : τ ; y : R, [x = r] α(R) ⊢ [x=r] α(y) : : τ ; y : R, [x = r] α(R) + [x = r] β(R) ⊢ [x=r] α(y) : : τ, ε ⊢ [x=r] λy.α(y) : R [x=r]α(R)+[x =r]β(R)

Theorem 1 .

 1 (Type safety) If Γ, H ⊢ true e : τ and ε, e → * π η, v then ∀σ.η ∈ H σ .

If we have more different types of resources, i.e. R = R 1 ∪• • •∪R k , we can restrict the number of choices to the resources that are compatible with the event (e.g. R = Socket ∪ File and the action accept connection).