@INPROCEEDINGS{BDFZ07a,
  title = {{Secure Service Orchestration}},
  author = {{Massimo} {Bartoletti} and {Pierpaolo} {Degano} and {Gianluigi} {Ferrari} and {Roberto} {Zunino}},
  booktitle = {FOSAD 2007},
  abstract = {We present a framework for designing and composing ser- vices in a secure manner. Services can enforce security policies locally, and can invoke other services in a “call-by-contract” fashion. This mech- anism offers a significant set of opportunities, each driving secure ways to compose services. We discuss how to correctly plan service orchestrations in some relevant classes of services and security properties. To this aim, we propose both a core functional calculus for services and a graphical design language. The core calculus is called lambda-req. It features primitives for selecting and invoking services that respect given behavioural requirements. Critical code can be enclosed in security framings, with a possibly nested, local scope. These framings enforce safety properties on execution histories. A type and effect system over-approximates the actual run-time behaviour of services. Effects include the actions with possible security concerns, as well as information about which services may be selected at run-time. A verification step on these effects allows for detecting the viable plans that drive the selection of those services that match the security requirements on demand. },
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4677},
  year = {2007},
  url = {http://www.di.unipi.it/~giangi/fosad07.pdf},
  partner = {PISA},
  school = {Pisa},
  task = {T2.3, T2.3a, T2.4, T3.4},
}