Une approche formelle pour le test des politiques de sécurité
Institution:
Evry, Institut national des télécommunicationsDisciplines:
Directors:
Abstract EN:
Security is a critical issue especially in dynamic and open distributed environments such as World Wide Web or wireless networks. To ensure that a certain level of security is always maintained, the system behavior must be restrained by a security policy. In this thesis, we propose a framework to specify security policies and test their implementation on networking and information systems. Security policies, nowadays, are a key point for the success of every modern infrastructure. The specification and the testing of security policies are the fundamental steps in the development of a secure system since any error in a set of rules is likely to harm the global security. We rely on two different test approaches to build our framework: the active and the passive approaches. The active testing consists in generating a set of test cases that can be applied on a specific implementation to study its conformance according to its security requirements. Whereas, the passive testing consists in passively observing the traffic of the system under test, without interrupting its normal operations. In the active approach, we propose a framework to automatically generate test sequences to validate the conformance of a security policy. The functional behavior of the system is specified using a formal description technique based on Extended Finite State Machines (EFSM), while the security requirement is specified using two formals languages (Or-BAC and Nomad). We developed specific algorithms to integrate the security rules within the functional system specification. In this way, we obtain a complete specification of the secured system. Then, the automatic test generation is performed using dedicated tools to produce test suites in a standard language (TTCN or MSC) facilitating their portability. In the passive testing approach, we specify, using Nomad formal language, the security policy the system under test has to respect. We analyze then the collected traces of the system execution in order to deduce verdicts of their conformity with respect to the system security requirements. Several algorithms are developed to check whether the collected traces conform or not to the security policy. We applied our framework on diverse systems ranging from wireless networking (OLSR ad hoc routing protocol) to computer systems including audit systems (SAP R/3), web services (France Télécom Travel) and web applications (Weblog Application). This wide range of applications allows to demonstrate the efficiency and the reliability of the proposed approaches.
Abstract FR:
Les politiques de sécurité sont devenues de nos jours un point clé dans toutes les infrastructures modernes. La spécification et le test de telles politiques constituent deux étapes fondamentales dans le développement d'un système sécurisé dans la mesure où toute erreur dans l'une de ces règles est susceptible de nuire à la sécurité globale du système. Pour faire face à ces deux défis, nous proposons une approche formelle pour spécifier les politiques de sécurité et vérifier leur déploiement sur des systèmes d'informations en réseau. Pour atteindre cet objectif, nous nous basons dans ce manuscrit sur deux approches différentes de test: l'approche active et l'approche passive. Le principe du test actif consiste à générer automatiquement une suite de scénarios de tests qui peut être appliquée sur un système sous test pour en étudier sa conformité par rapport à ses besoins en matière de sécurité. Quand au test passif, il consiste à observer et analyser passivement le système sous test, sans interrompre le flux normal de ses opérations. Pour l'approche active, nous proposons une méthodologie qui permet de générer automatiquement des séquences de test afin de valider la conformité d'un système par rapport à sa politique de sécurité. Le comportement fonctionnel du système est spécifié en utilisant un modèle formel basé sur des machines à états finis étendues (EFSM). Tandis que les besoins de sécurité sont spécifiés en utilisant deux langages formels (Or-BAC et Nomad). L'intégration de règles de sécurité au sein de la spécification fonctionnelle du système est réalisée grâce à des algorithmes dédiés et permet l'obtention d'une spécification sécurisée du système. La génération automatique des tests est ensuite effectuée en utilisant des outils développés dans notre laboratoire et permet d'obtenir des cas de tests abstraits décrits dans des notations standards (TTCN ou MSC) facilitant ainsi leur portabilité. Dans l'approche passive, nous spécifions la politique de sécurité que le système sous test doit respecter en utilisant le langage formel Nomad. Nous analysons ensuite les traces d'exécution d'un système afin d'élaborer un verdict sur leur conformité par rapport à la politique de sécurité. Plusieurs algorithmes sont fournis dans ce manuscrit pour vérifier si les traces recueillies sont conformes à la politique de sécurité. Nous avons appliqué notre méthodologie à divers systèmes allant des réseaux sans fil (le protocole de routage ad hoc OLSR) à des systèmes informatiques comme les systèmes d'audit (SAP R/3), les Web services (application Travel de France Télécom) et des applications Web (Weblog). Cette large gamme d'applications permet de démontrer l'efficacité et la fiabilité des approches proposées.