Skip to Main content Skip to Navigation
Theses

Synthèse et compilation de services web sécurisés

Mohammed Anis Mekki 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Résumé : 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.
Document type :
Theses
Complete list of metadatas

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/tel-01293742
Contributor : Michaël Rusinowitch <>
Submitted on : Friday, March 25, 2016 - 1:25:20 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Document(s) archivé(s) le : Sunday, June 26, 2016 - 3:22:20 PM

Identifiers

  • HAL Id : tel-01293742, version 1

Citation

Mohammed Anis Mekki. Synthèse et compilation de services web sécurisés . Informatique [cs]. Universite de Lorraine, 2011. Français. ⟨tel-01293742⟩

Share

Metrics

Record views

395

Files downloads

112