Approche formelle pour la verification des ids

Les Systmes de Dtection d'Intrusions (IDS) ont de nos jours une importance capitale dans la scurisation des rseaux, ce qui a fait d'eux des cibles d'attaques privilgies. Face cet tat de fait, le test de leur bon fonctionnement est devenu primordial dans tout processus de scurisation d'un rseau. Cependant les techniques de test usuelles s'avrent aujourd'hui insuffisantes. Nous nous sommes intresss dans ce travail la modlisation, la spcification, et la vrification formelle des proprits, des mcanismes, et des protocoles de scurit des IDS. Pour ce faire, nous avons utilis le langage de spcification formelle TLA+, et son Model Checker TLC. TLA+ ayant t conu pour la spcification des systmes concurrents et rpartis, nous l'avons adopt dans le cadre de ce travail pour couvrir des problmatiques de scurit. Aprs un travail de spcification et de validation des IDS, nous avons propos une extension TLA+ et TLC, afin de pouvoir dtecter les cycles indsirables pouvant surgir suite une spcification errone.