Secure service orchestration in open networks

Service Oriented Computing is a paradigm for creating a fully compositional service infrastructure. Compositionality makes security issues difficult to establish. As a matter of fact, defining global security properties on distribute, large-scale network seems to have little or even no sense at all.In a recent proposal, every single service specify its ad hoc security policies that are applied to (parts of) programs or services. These are called local policies and are amenable for developers. They are specified using a simple automaton-like structure, they offer full compositionality (through scope nesting) and a direct enforcing through a corresponding execution monitor. Compliance w.r.t. local policies is statically verified against a superset of the possible program execution traces, namely a history expression. History expressions for services are obtained through a type and effect system and then model checked for validity. A valid history expression only contains traces that never rise policy exceptions. Such history expressions drive the synthesis of composition plans, i.e. safe service orchestration.In this paper this approach is extended to work also on open networks, i.e. networks that are only partially specified. This allows one to compose services in a bottom-up fashion, while guaranteeing their correctness by construction. The potential, practical impact of our proposal is shown by applying it to a well known case study