[PDF] Implantation dune logique de configuration pour la vérification

View - Download Implantation dune logique de configuration pour la vérification

Previous PDF

Next PDF

UNIVERSITÉ DU QUÉBEC À MONTRÉAL

IMPLANTATION D'UNE LOGIQUE DE CONFIGURATION POUR LA

VÉRIFICATION AUTOMATIQUE DE CONFIGURATIONS

D'ÉQUIPEMENTS

DE RÉSEAUX

MÉMOIRE

PRÉSENTÉ

COMME EXIGENCE PARTIELLE

DE LA MAÎTRISE EN INFORMATIQUE

PAR

ÉRIC WENAAS

DÉCEMBRE 2006

UNIVERSITÉ DU QUÉBEC À MONTRÉAL

Service des bibliothèques

Avertissement

La diffusion de ce mémoire se fait dans le respect des droits de son auteur, qui a signé le formulaire Autorisation de reproduire et de diffuser un travail de recherche de cycles supérieurs (SDU-522 -Rév.01-2006). Cette autorisation stipule que "conformément

à l'article

11 du Réglement no 8 des études de cycles supérieurs, [l'auteur] concède à l'Université du

Québec

à Montréal une licence non exclusive d'utilisation et de publication de la totalité ou d'une partie importante de [son] travail de recherche pour des fins pédagogiques et non commerciales. Plus précisément, [l'auteur] autorise l'Université du Québec à Montréal à reproduire, diffuser, prêter, distribuer ou vendre des copies de [son] travail de recherche à des fins non commerciales sur quelque support que ce soit, y compris l'Internet. Cette licence et cette autorisation n'entraînent pas une renonciation de [la] part [de l'auteur]

à [ses] droits

moraux ni à [ses] droits de propriété intellectuelle. Sauf entente contraire, [l'auteur] conserve

la liberté de diffuser et de commercialiser ou non ce travail dont [il] possède un exemplaire.»

REMERCIEMENTS

Ce travail de recherche n'aurait pu être possible sans le concours de nombreuses per sonnes. Je tiens d'abord à remercier mon directeur de recherche, monsieur Roger Villemaire, pour ses pertinents conseils et la rigueur de son analyse. Je remercie également monsieur Omar Cherkaoui, directeur du Laboratoire de téléinformatique de l'Université du Québec à Montréeal, pour m'avoir accueilli dans son équipe et m'avoir guidé tout au long de ce projet. Son expertise en réseautique et ses commentaires furent des plus précieux. J'adresse également mes remerciements à messieurs Sylvain Hailé et Rudy Deca, res pectivement étudiants au doctorat en mathématique à l'Université du Québec à Montréal et

à l'École polytechnique de Montréal. Leurs conseils et leur aide furent très appréciés.

Enfin, je tiens à reconnaître

le support financier du Fonds québécois de la recherche sur la nature et les technologies et du Laboratoire de téléinformatique de l'Université du

Québec à Montréal.

Table des matières

REMERCIEMENTS ii

Liste des tableaux vi

Table des figures vii

Résumé

.. viii

Chapitre l

INTRODUCTION 1

1.1 Objectifs et contribution du travail 1

1.2 Division du document 2

Chapitre II

ARBRES DE CONFIGURATION 4

2.1 Représentation de la configurations des appareils 4

2.2 Arbre de configuration 5

Chapitre III

VALIDMAKER 6

3.1 Principales fonctions de

ValidMaker 6

3.1.1 Représentation graphique de la configuration d'un matériel 7

3.1.2 Génération de la configuration . 8

3.2 Organisation conceptuelle des services réseaux dans ValidMaker 8

3.2.1 Étapes de création et déploiement de services réseaux dans ValidMaker 8

3.2.2 Services génériques. . . . . . . . . . . 9

3.2.3

Instantiation d'un services génériques 9

3.2.4 Déploiement

d'un service . . . . . . 9 3.3 Format antérieur des règles de ValidMaker 10 3.3.1

Description de l'ancien format de règles 10

3.3.2 Objectifs recherchés par l'introduction de la logique de configuration 11

Chapitre IV

PRÉSENTATION DE LA LOGIQUE DE CONFIGURATION 13

4.1 Exemple où la logique peut être appliquée . . . . . . . . . 13

IV

4.2 Syntaxe de la logique de configuration 14

4.3

Quantificateurs

............. 14

4.3.1 Description

du chemin et quantification des variables. 14 4.3.2

Sémantique récursive. 16

4.4

Prédicats 17

Chapitre V

RÈGLES DE CONFIGURATION ASSOCIÉES AUX RÉSEAUX LOCAUX VIRTUELS

STATIQUES

ET AU PROTOCOLE VTP ..... 19

5.1

Présentation des VLANs et du protocole VTP 19

5.1.1 Définition

et fonction des VLANs . 19

5.1.2 Configuration des VLANs 20

5.1.3 Fonction

de VTP ..... 22

5.2 Définition des services de VLAN

dans le cadre de Validflilaker 23

5.2.1 Activer

VTP . 24

5.2.2 Associer une interface à un VLAN 24

5.2.3 Créer

un VLAN . 25 5.2.4

Créer un faisceau de jonction 25

5.3 Expérimentations faites sur les VLANs et règles de configuration en découlant 25

5.3.1 Première règle 26

5.3.2 Deuxième règle

28

5.4 Exemple de configuration 30

Chapitre VI

STRUCTURES DE DONNÉES ET ALGORITHMES UTILISÉS 33 6.1

Structures de données 33

6.1.1 Règles

.. 33 6.1.2

Prédicats 34

6.1.3

Autres classes. 34

6.2 Trace de déroulement de

la vérification. 36 6.2.1

Justification en cas de réponse négative 40

6.2.2 Construction récursive de la justification. 41

6.2.3 Reprise à partir d'un noeud particulier .. 43

v

6.2.4 Vérification à partir d'un prédicat 45

6.3 Résultats obtenus. 47

CONCLUSION 49

Bibliographie . 52

Liste des tableaux

6.1 Variation du nombre de commutateurs 47

6.2 Variation du nombre d'interfaces . . . 48

Table des figures

2.1 Arbre de configuration . 5

3.1 Représentation d'un appareil dans ValidMaker 7

6.1 Diagramme de classes arbre expression 35

6.2 Diagramnme de classe arbre expression(suite) 35

6.3 Arbre expression de la règle 1 . 38

6.4 La partie fausse d'une règle est surlignée 42

6.5 Choix de noeuds présenté à l'utilisateur 42

6.6 Résultat de la reprise de la vérification. 44

6.7 Arbre Expression SwitchlnVTPDomain 46

6.8 Changement de variables lorsqu'un prédicat est évalué 46

Résumé

Ce travail montre comment un formalisme logique, la logique de configuration, est intégré au sein d'un outil de gestion de configuration de réseaux, ValidMaker. Le principal objectif de ce travail est de démontrer que la logique de configuration est particulièrement bien adaptée à la vérification automatique de configuration de réseaux. À cette fin, nous développons un exemple réel de configuration de réseaux et nous trouvons des règles qui

doivent être vérifiées pour qu'une telle configuration soit fonctionnelle. Ensuite, nous expli

quons comment nous avons implanté la logique de configuration dans ValidMaker et nous illustrons le fonctionnement de notre algorithme de vérification.

Chapitre l

INTRODUCTION

1.1 Objectifs et contribution du travail

La complexité croissante des réseaux posent divers problèmes de configuration aux adminis trateurs. Le déploiement de services réseaux devient de plus en plus compliqués et le fait de déployer un nouveau service dans un réseau peut avoir comme effet de causer des problèmes d'incompatibilité avec d'autres services. Des outils existent afin d'aider un administrateur réseau dans sa tâche. Notre travail s'intègre dans le cadre de l'un de ces outils: ValidMa ker. Nous y implantons un formalisme logique permettant de faire des vérifications dans des structures arborescentes. Ce formalisme est la logique de configuration. Le premier objectif de notre travail est de démontrer de façon empirique que la logique de

configuration est particulièrement bien adaptée à la vérification automatique de configuration

de réseaux. Nous implantons donc un moteur de validation au sein de ValidMaker. Notre moteur de validation utilise la logique de configuration.

Le deuxième objectif de notre travail

est

d'ajouter à ValidMaker une plus grande flexibilité quant à l'édition de règles pouvant

être vérifiées dans

un réseau.

Notre approche sera

tout d'abord de présenter les différents éléments que nous allons utiliser soit ValidMaker et la logique de configuration. Ensuite, nous développerons un exemple réel de configuration réseaux en utilisant les réseaux locaux virtuels. De cet exemple réel, nous dégagerons des règles de configuration qui devront

être vérifiées afin d'obtenir une

configuration fonctionnelle. 2 La contribution de notre de travail consiste en l'implantation de la logique dans ValidMaker. Nous expliquerons quelles sont nos structures de données pour représenter une règle de logique de configuration. Nous expliquerons également de façon détaillée le fonctionnement

de notre algorithme de vérification. Une trace d'exécution sera également présentée. Nous

verrons également comment notre algorithme offre une valeur ajoutée

à l'outil ValidMaker en

permettant à un administrateur réseau d'analyser une vérification en reprenant la vérification

à partir d'une partie d'une règle de validation.

1.2 Division du document

Le chapitre 2 présente les arbres de configuration. Les arbres de configuration sont des arbres dont les noeuds correspondent à des couples paramètre-valeur. Ces arbres seront utilisées dans l'outil

ValidMaker et dans la logique de configuration.

Le chapitre 3 présente l'outil

Validmaker. Nous y présentons différentes fonctionnalités nécessaires à la compréhension du déploiement de services à l'aide de ValidMaker. Nous y présentons également comment fonctionne la vérification du format de règles antérieur à notre travail. Le chapitre 4 présente la logique de configuration. Nous y présentons la syntaxe de cette logique et montrons comment la notion de prédicat peut y être introduite.

Le chapitre 5 présente les

Virtual Local Area Networks(VLAN). Notre exemple de configura tion est basé sur ce service réseau. Dans ce chapitre, nous expliquerons comment fonctionnent les VLANs. Nous expliquerons également la démarche que nous avons prise afin de représenter les configurations de VLANs dans ValidMaker et de trouver des règles de configuration qui doivent être respectées afin de s'assurer que les services de VLANs soient fonctionnels dans un réseau.

Le chapitre 6 présente les structures de données et les algorithmes que nous avons utilisées

afin d'implanter la logique de configuration dans

ValidMaker. Nous présentons également

une trace d'exécution afin d'illustrer le fonctionnement de la vérification Le chapitre 7 est la conclusion, un rappel des principaux points de ce document sera fait et 3 nous y présenterons les travaux futurs qui pourraient être envisagés suite à notre travail.

Chapitre II

ARBRES DE CONFIGURATION

Nous présentons dans ce chapitre comment la configuration d'un appareil peut être représentée

sous forme d'un arbre de configuration. À cette fin, nous commencerons par traiter de la façon

que la configuration des appareils réseaux est représentée. Ensuite, nous expliquerons en quoi

consiste un arbre de configuration et nous donnerons un exemple d'arbre de configuration.

2.1 Représentation de la configurations des appareils

La configuration d'appareils réseaux se fait de façon hiérarchique. La hérarchie est représentée

par différents modes et sous-modes. Par exemple, pour configurer une interface particulière, il faut d'abord entrer dans le mode de configuration de cette interface. La configuration d'un appareil est généralement stockée sous la forme d'un fichier texte 1 .

Ce fichier suit une

structure hiérarchique similaire à la structure hiérarchique des modes et des sous-modes. On

se retrouve donc avec un arbre de couples paramètre-valeur. Il est possible à partir du fichier

de configuration de reconstituer la hiérarchie des couples paramètre-valeur correspondant aux

différents paramètres de configuration. Lors du démarrage de l'appareil, la configuration de

départ est chargée et le fichier est interprété par l'appareil. L'appareil ajustera ses paramètres en fonction de ce qu'il trouve dans son fichier de configuration.

1 Par exemple, sur un commutateur ou un routeur Cisco ce fichier se nomme config. txt.

5 ip adress = 192,168.0.1 ip adress = 243.54.10.25

Fig. 2.1 Arbre de configuration

2.2 Arbre de configuration

Puisque les paramètres d'un appareil sont représentés d'une façon hiérarchique, il est possible

de représenter la configuration d'un appareil réseau sous la forme d'un arbre où les noeuds correspondent à des couples paramètre-valeur. Nous appelons ce type d'arbre, un arbre de configuration. La configuration globale du réseau est alors une forêt d'arbres de configuration. La racine d'un arbre identifie un appareil. Les descendants de la racine correspondent aux paramètres directement reliés à cet appareil. La figure 2.1 représente un arbre de configuration simple. Dans cet arbre, on peut voir que les valeurs pour l'adresse IP des interfaces se situent sous les noeuds des interfaces correspondantes. Une caractéristique importante des arbres de configuration est que, étant

donné un type de matériel et une version du système d'exploitation donnés, la structure de

l'arbre est connue d'avance. On connaît le nombre de paramètres possibles ainsi que leurs positions relatives dans l'arbre. Ce que l'on ne connaît pas sont les paramètres présents ainsi que la valeur associée à chacun des paramètres. L'exercice consistant en la vérification de configuration consistera donc en la vérification de valeurs de certains paramètres dont les positions dans l'arbre de configuration sont prédéterminées.

Chapitre III

VALIDMAKER

ValidMaker est un outil de gestion de configuration de réseaux informatiques qui a été

développé au laboratoire de téléinformatique de l'université du Québec à Montréal (5). Va

lidMaker représente la configuration d'un appareil réseau en utilisant la notation Meta-CL! (6). Les configurations d'appareils réseaux sont représentés sous forme d'arbres de configu ration. Chaque appareil d'un réseau correspond à un arbre différent. Puisque nous avons introduit la logique de configuration au sein de l'outil ValidMaker, il est impératif de faire une présentation de cet outil avant d'aborder comment nous y avons introduit la logique. Afin de présenter ValidMaker, nous traiterons des points qu'il faut comprendre afin d'être capable de bien saisir la démarche d'intégration de la logique de configuration au sein de cet outil. Notre présentation de ValidMaker comporte trois parties. En premier lieu, nous présenterons certaines des fonctionnalités de ValidMaker. Ensuite, nous traiterons de la façon dont la création et le déploiement de services réseaux se font dans ValidMaker. En dernier lieu, nous présenterons comment fonctionnait l'édition et la

vérification de règle dans ValidMaker préalablement à notre travail d'intégration de la logique

de configuration.

3.1 Principales fonctions de ValidMaker

Dans cette section nous traitons des principales fonctions de ValidMaker. Nous présenterons comment ValidMaker représente la configuration d'un matériel et comment il peut générer 7 .:JQJ2!.I

Irlo 1o.',,,,. Node 1Cft.! 1s......1

15-'+ T.... Aoo<

Node "'_fiet

• "Pmodo:eim

Il....

• ",p_:O"""",

8-......i"'" :FortEJhemel 0/1

• ....ch:>oeaU_: 101

è • r-w/oee: FMlEthem lWitchPCW' ùtrl: IFMlE&"'''''' 0/23

Serr;;e

J Fig. 3.1 R.eprésentation d'un appareil dans ValidMaker une configuration de matériel. Certes,

ValidMaker comprend d'autres fonctionnalités

1 mais la compréhension de celles que nous présentons ici sont suffisantes à la compréhension de notre démarche.

3.1.1 Représentation graphique de la configuration d'un matériel

Une importante faculté de ValidMaker est d'être capable de construire un arbre de configu ration à partir d'un fichier de configuration et ainsi d'obtenir une représentation graphique de la configuration d'un appareil. À cet égard, ValidMaker est un outil flexible car il permet de représenter la configuration de plusieurs types d'appareil.

Pour ce faire, il suffit d'ajouter

les paramètres de configuration du matériel en question. C'est ainsi par exemple, qu'en un tour de main nous avons pu y ajouter la reconnaissance des paramètres de configuration des

VLANs.

ValidMaker n'est donc pas dépendant d'un type de matériel ou encore d'un système d'exploitation particuliers. La figure 3.1 montre un arbre de configuration tel que représenté au sein de ValidMaker. Cette fonctionnalité permet de voir facilement les configurations de tous les appareils d'un

Ivoir à ce titre (5)

8 réseau. Les configurations peuvent être obtenues avec un protocole comme NetConf (8) par exemple.

3.1.2 Génération de la configuration

S'il est possible de représenter graphiquement une configuration au sein de ValidMaker, il est

également possible de générer une configuration fonctionnelle à partir de la représentation

graphique d'un arbre. Puisque ValidMaker permet de modifier la représentation graphique d'une configuration, les modifications peuvent par la suite se refléter dans un fichier de configuration fonctionnel. Ceci permet à un ingénieur réseau d'utiliser ValidMaker pour

charger les configurations des appareils du réseau, modifier ces configurations à l'intérieur de

ValidMaker et ensuite générer de nouvelles configurations et les remettre sur les équipements

du réseau.

3.2 Organisation conceptuelle des services réseaux dans ValidMaker

Un réseau dans ValidMaker comprend les appareils du réseau, les services rattachés au réseau

et les règles devant être appliquées dans le réseau. Les configurations d'appareils du réseau

sont modifiées par le déploiement et le retrait de services sur un appareil. Nous expliquerons dans cette section comment créer et déployer des services réseaux dans ValidMaker.

3.2.1 Étapes de création et déploiement de servIces réseaux dans Valid

Maker Afin de déployer un service sur un appareil dans ValidMaker, trois étapes sont nécessaires.

Il faut

tout d'abord définir un service générique. Ensuite, ce service générique doit être instantié. Et finalement, le service instantié sera déployé sur un appareil.

Une fois que le service

est déployé, l'ingénieur réseau peut faire générer les fichiers configura tion et modifier les configurations des appareils concernés. Nous expliquons dans cette section les distinctions entre services génériques, services instantiés et déploiements de services. 9

3.2.2 Services génériques

Tous les services que l'on veut déployer dans ValidMaker doivent tout d'abord être des instantiations d'un service générique. Un service générique est une représentation abstraite

d'un service. Il contient les paramètres qui doivent être ajoutés à la configuration mais sans

contenir de valeur pour ces paramètres. Le service est donc décrit mais sans tenir compte du cadre dans lequel il sera déployé. La représentation sous forme d'arbre de configuration d'un service générique va comprendre les noeuds que l'on doit ajouter dans la configuration

d'un matériel où le service va être déployé. Toutefois, ces noeuds ne contiendront que des

paramètres et n'auront pas encore de valeur. On retrouve donc dans la description du service générique le squelette complet des noeuds qui devront apparaître dans la configuration d'un appareil pour que le service soit déployé correctement. Pour des fins de regroupement logique, il est possible de regrouper les services en familles de services. Une famille de service regroupera tous les services génériques qui ont un lien entre eux.

3.2.3 Instantiation d'un services génériques

Un service générique n'est pas fonctionnel. 1'instantiation d'un service générique consiste en

la création d'un service plus spécifique en spécifiant certaines valeurs du service générique.

Les valeurs spécifiées sont celles qui ne seront pas dépendantes de l'appareil sur lequel le

service sera déployé. Il est donc possible qu'une instantiation d'un service ne permette pas de donner des valeurs à tous les paramètres du service. On laissera en blanc les noeuds qui sont spécifiques au matériel sur lequel le service sera déployé. Lors de l'instantiation du service générique, on spécifie les valeurs des paramètres qui qualifieront le service mais sans pour autant spécifier des valeurs qui varieront selon les décisions qui seront prises lors du choix de l'équipement sur lequel le service sera déployé.

3.2.4 Déploiement d'un service

Lorsqu'un service aura été instantié, il sera possible de le déployer. Un service doit toujours

être déployé sur un appareil et ce n'est qu'avec le déploiement d'un service que la configu

10 ration d'un appareil pourra être modifiée. Il est possible que des valeurs supplémentaires doivent être spécifiées lors du déploiement du service. Ce qui est le cas des paramètres se

rattachant directement à l'appareil. Un bon exemple se présente lorsque le service doit être

rattaché à une interface de l'appareil. Il est alors évident que la valeur affectée au paramètre

interface du service ne peut être déterminée que lors du déploiement du service.

3.3 Format antérieur des règles de ValidMaker

Une fois que des services ont été déployés et avant de faire générer des nouvelles configura

tions, l'ingénieur réseau peut vérifier que l'ajout des nouveaux services n'a pas introduit de problème dans le réseau. Pour ce faire, des règles peuvent être appliquées dans le réseau. Les règles permettront d'éviter certaines erreurs qui auraient pu être commises dans le cadre du

déploiement des services. Les règles peuvent aussi être utlisées afin de détecter des erreurs

dans une configuration de réseau existante. Les règles doivent

être définies par l'ingénieur

réseau.

Préalablement à notre travail, il existait déjà un format pour définir des règles et un moteur

pour vérifier ces règles dans ValidMaker. Nous faisons ici un survol du fonctionnement de la

création et de la vérification de ce format de règles. Nous en donnerons également quelques

avantages et inconvénients. Nous conclurons sur ce sujet en présentant les objectifs que nous poursuivons en introduisant un nouveau format de règles dans ValidMaker.

3.3.1 Description de l'ancien format de règles

Les règles de l'ancien format sont principalement basées sur la logique propositionnelle. Les seules opérations logiques possibles sont l'implication logique, la conjonction et la disjonction. Les propositions de base sont des opérations de haut niveau permettant de faire diverses comparaisons entre des noeuds ou entre des branches d'arbres. Ces opérations sont alors combinées avec des conjonctions ou des disjonctions à l'intérieur d'une implication logiquequotesdbs_dbs33.pdfusesText_39

[PDF] Les congés de maladie dans la fonction publique fédérale

[PDF] OFFRE MODULAIRE* «Emplois d avenir» *Moins de 400 heures

[PDF] Panorama du mécénat des entreprises du CAC 40 2013

[PDF] SCM-IT Consulting. Supply Chain Management & Information Technology. Avril 2015. Hubert POULIQUEN. 32A, Avenue Pasteur 17200 SAINT SULPICE DE ROYAN

[PDF] Règlement. relatif à l'octroi de. prêts hypothécaires. aux collaborateurs actifs et retraités en Suisse

[PDF] HERMINE DE NANTES ATLANTIQUE. Avenant 2008-2009 / n 1 à la convention conclue au titre des saisons 2006-2007, 2007-2008, 2008-2009, 2009-2010

[PDF] En partenariat avec :

[PDF] À L INTENTION DE VOTRE FAMILLE

[PDF] LFI 2016 - EXTRAIT DE LA MISSION : ENGAGEMENTS FINANCIERS DE L'ÉTAT

[PDF] Politique d aménagement linguistique de l Ontario pour l éducation postsecondaire et la formation en langue française

[PDF] développe les solidarités

[PDF] United Nations Audiovisual Library of International Law

[PDF] POLIT FLASH. Recommandation pour la session d été des Chambres fédérales. du 1 au 19 juin 2015

[PDF] FICHE TECHNIQUE n 3 mai 2009 Organisation des élections

[PDF] CONCOURS. sur épreuves. Rédacteur territorial. 1 er grade d'accès au cadre d'emplois