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.
Type de document :
Communication dans un congrès
SEEFM'09 : 4th South-East European Workshop on Formal Methods, Dec 2009, Thessaloniki, Greece. 2009
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger
Contributeur : Brigitte Briot <>
Soumis le : lundi 22 février 2010 - 15:49:24
Dernière modification le : vendredi 26 février 2010 - 14:07:37
Document(s) archivé(s) le : vendredi 18 juin 2010 - 21:36:50


Fichiers produits par l'(les) auteur(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. 2009. 〈inria-00458891〉



Consultations de la notice


Téléchargements de fichiers