Skip to Main content Skip to Navigation
Conference papers

Secure Service Composition with Symbolic Effects

Abstract : 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 plans in most cases.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Brigitte Briot Connect in order to contact the contributor
Submitted on : Monday, February 22, 2010 - 3:49:24 PM
Last modification on : Friday, August 23, 2019 - 11:02:03 AM
Long-term archiving on: : Friday, June 18, 2010 - 9:36:50 PM


Files produced by the author(s)


  • HAL Id : inria-00458891, version 1



Gabriele Costa, Pierpaolo Degano, Fabio Martinelli. Secure Service Composition with Symbolic Effects. SEEFM'09 : 4th South-East European Workshop on Formal Methods, Dec 2009, Thessaloniki, Greece. ⟨inria-00458891⟩



Record views


Files downloads