Automatic synthesis of secured web services
Synthèse et compilation de services web sécurisés
Résumé
Automatic composition of web services is a challenging task. Many works have considered simplified automata models that abstract away from the structure of messages exchanged by the services. For the domain of secured services (using e.g. digital signing or timestamping) we propose a novel approach to automated
composition of services based on their security policies. Given a community of services and a goal service, we reduce the problem of
composing the goal from services in the community to a security problem where
an intruder should intercept and redirect messages from the service community
and a client service till reaching a satisfying state. We have implemented the algorithm in Avantssar Platform and applied the tool to several case studies. Then we present a tool that compiles the obtained trace describing the execution of a the mediator
into its corresponding runnable code.
For that we first compute an executable specification as prudent as possible of her role
in the orchestration. This specification
is expressed in ASLan language, a
formal language designed for modeling Web Services tied with security policies.
Then we can check with automatic tools that this ASLan specification verifies some
required security properties such as secrecy and authentication.
If no flaw is found, we compile the specification into a Java servlet that can be used by the mediator to lead the orchestration.
La composition automatique de services web est une tâche difficile. De nombreux travaux ont
considérés des modèles simplifiés d'automates qui font abstraction de la structure des
messages échangés par les services. Pour le domaine des services sécurisés (par exemple utilisant
la signature numérique ou l'horodatage), nous proposons une nouvelle approche pour automatiser
la composition des services basés sur leurs politiques de sécurité.
Étant donnés, une communauté de services et un service objectif, nous réduisons le problème de la
synthèse de l'objectif à partir des services dans la communauté à un problème de sécurité, où
un intrus doit intercepter et rediriger les messages depuis et vers la communauté de services
et un service client jusqu'à atteindre un état satisfaisant pour le dernier.
Nous avons implémenté notre algorithme dans la plateforme de validation du projet AVANTSSAR
et nous avons testé l'outil correspondant sur plusieurs études de cas.
Ensuite, nous présentons un outil qui compile les traces obtenues décrivant l'exécution d'un médiateur vers
le code exécutable correspondant.
Pour cela nous calculons d'abord une spécification exécutable aussi prudente que possible de son rôle
dans l'orchestration. Cette spécification est exprimé dans la langue ASLan, un
langage formel conçu pour la modélisation des services Web liés à des politiques de sécurité.
Ensuite, nous pouvons vérifier avec des outils automatiques que la spécification ASLan obtenue vérifie certaines
propriétés requises de sécurité telles que le secret et l'authentification.
Si aucune faille n'est détectée, nous compilons la spécification ASLan vers une servlet Java qui peut être
utilisé par le médiateur pour contrôler l'orchestration.
Loading...