La lecture à portée de main
Découvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDécouvre YouScribe en t'inscrivant gratuitement
Je m'inscrisDescription
Sujets
Informations
Publié par | Thesee |
Nombre de lectures | 219 |
Langue | Français |
Poids de l'ouvrage | 1 Mo |
Extrait
N° d'ordre : 4088
THESE DE DOCTORAT EN CO-TUTELLE
Université de Bordeaux 1
ÉCOLE DOCTORALE DE MATHÉMATIQUES ET D’INFORMATIQUE
et
Université de Sfax
FORMATION DOCTORALE EN INFORMATIQUE
Présentée par
Monia LOULOU ALOULOU
Pour obtenir le titre de
DOCTEUR EN INFORMATIQUE
Approche Formelle pour la Spécification,
la Vérification et le Déploiement des Politiques de
Sécurité Dynamiques dans les Systèmes à base
d’Agents Mobiles
Soutenue le : Samedi le 13 Novembre 2010
Devant la commission d’examen composée de :
M. Faiez Gargouri Professeur à l’ISIM-Sfax Président
M. Frédéric Cuppens Professeur à l'ENST-Bretagne Rapporteur
M. Maher Khemekhem Maître de conférences à l’ISG-Sousse
M. Mohamed Jmaiel Professeur à l’ENI-Sfax Directeur de thèse
M. ed Mosbah Professeur à l’ENSEIRB-Bordeaux Directeur de thèse
Remerciements
Je voudrai exprimer ma profonde reconnaissance pour mes directeurs de these,` Mon
sieur Mohamed JMAIEL, Professeur a` l’Ecole Nationale d’Ingenieurs´ de Sfax et Direc
teur de l’unite´ de Recherche en Dev´ eloppement et Controleˆ d’Applications Distribuees´
(ReDCAD), et Monsieur Mohamed MOSBAH, Professeur a` l’Institut Polytechnique
de Bordeaux (ENSEIRB MATMECA), pour la confiance qu’ils m’ont accordee´ en me
del´ eguant´ ce travail. Ce travail a grandement profite´ de leurs encadrements, de leurs
grandes competences´ et de leurs qualites´ humaines.
Je tiens a` remercier vivement Monsieur Ahmed HADJ KACEM, Maˆıtre de Conferences´
a` la Faculte´ des Sciences Economiques et de Gestion de Sfax, pour son encadrement tout
ˆau long de ce travail. Je lui suis extremement reconnaissante pour sa constante disponi
bilite´ ainsi que pour la rigueur de raisonnement scientifique qui m’a permis de structurer
mes idees.´ Surementˆ les principaux resultats´ present´ es´ dans cette these` sont issus de ces
discussions et de ces conseils d’ordre methodologique,´ technique et redactionnel.´
` `J’adresse mes remerciements a Monsieur Faiez GARGOURI, Professeur a l’Institut
Superieur´ d’Informatique et de Multimedia´ de Sfax, pour avoir bien voulu me faire l’hon
neur de presider´ le jury de ma these.`
J’adresse mes sinceres` remerciements a` Monsieur Fred´ eric´ CUPPENS, Professeur a`
´l’Ecole Nationale Superieure´ de Tel´ ecommunications´ de Bretagne, ainsi qu’a` Monsieur
Maher KHEMAKHEM, Maˆıtre de conferences´ a` l’Institut Superieur´ de Gestion de
Sousse, pour l’inter´ etˆ qu’ils ont porte´ a` mon travail en acceptant d’etreˆ rapporteurs de
cette these.`
Je tiens a` remercier les etudiants´ de mastere` qui, au cours de leurs projets, se sont
interess´ es´ a` ma problematique´ de these` et m’ont apporte´ du sang neuf et des idees´ nou
velles. Je cite notamment Mohamed Tounsi et Houssem Aloulou.
Je tiens a` remercier eg´ alement tous les membres de notre equipe´ de recherche pour leur
sympathie et l’ambiance chaleureuse qu’ils donnent lors de nos reunions.´ Je remercie
particulierement` Slim Kallel, Imen Loulou et Amira Regayeg pour les cooperations´ que
nous avons eues et les informations que nous avons echang´ ees.´Table des matieres`
Introduction Gen´ erale´ 1
Problematique´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
Objectifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
Contributions et Organisation de la these` . . . . . . . . . . . . . . . . . . . . . 4
1 Technologie des agents mobiles 7
1.1 Du Modele` Client Serveur au Modele` Agent Mobile . . . . . . . . . . . 7
1.1.1eur . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.1.2 Evaluation distante . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.1.3 Code a` la demande . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.1.4 Agent Mobile . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2 Agents Mobiles : Une nouvelle approche de conception . . . . . . . . . . 9
1.2.1 Definition´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.2.2 Qualites´ de l’agent mobile . . . . . . . . . . . . . . . . . . . . . 10
1.2.3 Environnement d’execution´ des agents mobiles . . . . . . . . . . 11
1.3 Efforts de standardisation . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.3.1 MASIF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.3.2 FIPA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.3.3 Synthese` . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
1.4 Modelisation´ des systemes` a` base d’agents mobiles . . . . . . . . . . . . 15
1.4.1 Modelisation´ structurelle . . . . . . . . . . . . . . . . . . . . . . 16
1.4.2 Mod´ comportementale . . . . . . . . . . . . . . . . . . . 18
1.4.3 Synthese` . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
1.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
´2 Securit´ e´ & Mobilite´ : Etat de l’art 21
2.1 Politiques de securit´ e´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
2.1.1 Definitions´ et Fondements . . . . . . . . . . . . . . . . . . . . . 22
2.1.2 Modelisation´ de la securit´ e´ . . . . . . . . . . . . . . . . . . . . . 23
2.1.2.1 Modeles` de controleˆ d’acces` . . . . . . . . . . . . . . 23
2.1.2.2 Modeles` de controleˆ de flux . . . . . . . . . . . . . . . 24
2.1.2.3 Modeles` de controleˆ d’usage . . . . . . . . . . . . . . 24
2.1.3 Approches de specification´ des politiques de securit´ e´ . . . . . . . 25
2.1.3.1 Sp´ a` travers un langage metier´ . . . . . . . . 252.1.3.2 Specification´ a` base de regles` . . . . . . . . . . . . . . 26
2.1.3.3 Sp´ a` base de logique . . . . . . . . . . . . . 28
2.1.3.4 Synthese` . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.1.4 Mecanismes´ d’imposition des politiques de securit´ e´ . . . . . . . . 29
2.2 Securit´ e´ des systemes` a` base d’agents mobiles . . . . . . . . . . . . . . . 30
´ ´2.2.1 Besoins de securite . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.2.2 Solutions de securit´ e´ adaptees´ . . . . . . . . . . . . . . . . . . . 32
2.2.3 de securit´ e´ specifiques´ . . . . . . . . . . . . . . . . . . 33
2.3 Discussion : Une nouvelle perspective de securit´ e´ . . . . . . . . . . . . . 34
2.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3 Specification´ Formelle des Systemes` a` base d’Agents Mobiles 37
3.1 La specification´ formelle : langage & outil de preuve . . . . . . . . . . . 38
3.1.1 La Notation Z . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.1.2 Z/EVES : outil de preuve formelle . . . . . . . . . . . . . . . . . 39
3.2 Modelisation´ conceptuelle des systemes` a` base d’agents mobiles . . . . . 40
3.2.1 Cycle de vie de l’Agent Mobile . . . . . . . . . . . . . . . . . . 40
3.2.2 Taxonomie commune : Specification´ . . . . . . . . . . . . . . . . 41
3.2.2.1 Systeme` d’execution´ d’agents mobiles . . . . . . . . . 41
3.2.2.2 Agent de Service . . . . . . . . . . . . . . . . . . . . . 42
3.2.2.3 Mobile . . . . . . . . . . . . . . . . . . . . . . 43
3.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4 Cadre formel pour la securit´ e´ des systemes` a` base d’agents mobiles 47
4.1 Cadre de specification´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.1.1 Politique de securit´ e´ : Specification´ . . . . . . . . . . . . . . . . 48
4.1.2 de securit´ e´ : Raffinement . . . . . . . . . . . . . . . . . 50
4.2 Cadre de verification´ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.2.1 Preuve formelle de la consistance des specifications´ . . . . . . . . 53
4.2.2 Preuve de la intra politique . . . . . . . . . 53
4.3 Cadre de reconfiguration . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.4 Cadre d’adaptation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
4.4.1 Identification et Specification´ des differents´ cas d’incoherences´ . . 61
4.4.2 Specification´ de la politique d’adaptabilite´ . . . . . . . . . . . . . 64
4.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70
´ ´5 Approche formelle pour la specification et la verification des attaques 71
5.1 Taxonomie des attaques . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
5.1.1 Attaques contre l’authentification . . . . . . . . . . . . . . . . . 72
5.1.2 la confidentialite´ . . . . . . . . . . . . . . . . . . 72
5.1.3 Attaques contre l’integrit´ e´ . . . . . . . . . . . . . . . . . . . . . 73
5.1.4 la disponibilite´ . . . . . . . . . . . . . . . . . . 73
5.2 Approche proposee´ . . . . . . . . . . . . .