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 run-time 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 plansin most cases.