Génération de tests de sécurité pour les systèmes répartis
Institution:
Université Joseph Fourier (Grenoble)Disciplines:
Directors:
Abstract EN:
This document presents a method, based on formai conformance testing techniques, to test security in a distributed system. Conformance testing covers weil defined methods used in particular to test conformance of protocol implementations to standards. From a case study and an analysis of concepts of formai description techniques used for security modelling, we propose an original method of security test generation which is not based on the existence of a global functional model of the system. The method uses modal logies to express security rules. This method is based on the idea that predicates of the security rules are associated to atomic tests and logic operators to test combination operators. Then tests can be generated trom a well-formed formula of the security modelling formalism. This document also describes the implementation of the method we developed, and the experiments done with the implementation to validate the method presented in this document.
Abstract FR:
Ce document propose une méthode de test de la sécurité d'un système réparti basée sur les techniques de test formel de la conformité, utilisées entre autres dans le domaine des protocoles pour s'assurer qu'une implantation est bien conforme à sa spécificationD'après une analyse des concepts des formalismes dédiés à la spécification de la sécurité et une étude de cas, nous proposons une méthode de génération de tests de la sécurité qui permet de se passer d'une spécification complète du système. Elle s'appuie sur une formalisation en logique modale des règles de sécurité. Dans cette méthode, les prédicats du formalisme correspondent à des tests atomiques et les opérateurs du formalisme correspondent à des opérateurs de combinaison de tests. Il est ainsi possible de générer des tests d'après une formule bien formée du formalisme de spécification de la sécurité. Sont également présentées une description de l'implantation de cette méthode, qui demande que soient résolus les problèmes classique qui se posent avons menées pour valider notre méthode.