Projet de recherche doctoral numero :3026

Date depot: 1 janvier 1900
Titre: Test de sécurité pour Internet of Services à travers le model checking
Directeur de thèse: Davide BALZAROTTI (Eurecom)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini

Resumé: 1. Introduction La vision de l’ Internet des Services (IoS) et l'émergence des architectures orientées services (SOA) ont imposé un important changement de paradigme dans la façon dont les technologies de l'information et de la communication (TIC) et les applications sont créées, implémentées, déployées et consommées: elles ne sont plus le résultat de composants de programmation dans le sens traditionnel, mais ils sont construits sur la base de composition de services, distribués sur le réseau, regroupés et consommés à l’exécution, de façon flexible et à la demande. L’exposition de services dans les nouvelles infrastructures réseau entraine un certain nombre de problèmes liés à la sécurité et à la confiance. Afin de fournir les garanties nécessaires aux fournisseurs et aux utilisateurs de services distribués, une validation relative à la sécurité doit être appliquée. De nombreuses techniques de validation sont disponibles. En particulier, le model checking s'est révélé efficace pour détecter des défauts dans la logique lors de la spécification des applications distribuées tandis que les tests d’ intrusion, une forme particulière du domaine des tests de sécurité, est efficace pour trouver des vulnérabilités de bas niveau (e.g. Cross-Site Scripting (XSS)) dans les applications Web en ligne. Ces techniques sont déjà largement utilisées pour détecter de graves vulnérabilités et elles jouent un rôle central pour l'amélioration de la sécurité du IoS. Toutefois, il y a un potentiel énorme dans l'utilisation combinée plutôt qu’isolée de ces technologies. Des exemples sont les défauts découverts en utilisant les techniques de model checking pour les services de SSO basés sur SAML pour Google Apps [1, 2]. Les vulnérabilités découvertes ont été manuellement reproduites et prouvées pour les services de SSO basés sur SAML pour Google Apps par les auteur des [1, 2]. Une question fondamentale est: est-il possible de vérifier si un système réel est exposé à des vulnérabilité par l’utilisation des techniques de model checking? L'objectif principal de cette thèse sera de concevoir et développer une méthodologie générale pour combiner efficacement les technologies de l'état de l'art pour le model checking et le security testing pour améliorer la sécurité de l’ IoS (voir section 3). Cette méthodologie sera intégrée dans un prototype (voir section 5) qui sera examiné par rapport aux applications IoS industrielles et open source appropriées pour SAP (voir section 4). Cette étude pourrait permettre de transférer avec succès les résultats de cette thèse dans le domaine industriel, particulier à SAP (voir section 5). Cette thèse sera réalisée à SAP, dans l'environnement international de projets de l'Union Européenne auxquels participent d'autres partenaires de l'industrie et de l'académie. En particulier, le model checking et d'autres techniques similaires de raisonnement automatisé seront examinés dans le contexte du projet européen AVANTSSAR (Automated VAlidatioN of Trust and Security of Service-oriented Architecture), alors que le sujet de ‘security testing’ aussi bien que sa combinaison synergique avec le model checking seront étudiés dans le contexte du projet européen SPaCIoS (Secure Provision and Consumption in the Internet of Services). 2. Etat de l'art L'analyse automatisée de protocoles de securité a été largement étudiée et de nombreux instruments d'analyse avec différents degrés d'automatisation ont été développés [3, 4, 5, 6, 7, 8, 9]. Ceux-ci comprennent aussi la plateforme AVANTSSAR pour l'analyse de services et de leurs politiques de sécurité [10]. Les techniques de model checking ont déjà été utilisées pour découvrir des vulnérabilités dans la logique de protocoles comme [1,2]. Le premier a révélé un grave défaut de sécurité dans le protocole SAML SSO de Google qui permettait à un fournisseur de services malhonnête de personnifier un utilisateur méconnaissant de Google. Le dernier décrit un défaut inconnu dans le protocole SAML 2.0 SSO dans lequel si les deux requêtes faites par le client au fournisseur du service prescrites par le protocole ne sont pas transportées sur la même connexion SSL, alors le fournisseur du service ne peut pas être certain de l'authenticité de la dernière même s'il peut vérifier la validité de l'assertion d'authenticité qu'elle contient. Il y a eu aussi beaucoup d'applications de model checking à l'analyse formelle des aspects de sécurité dans les services Web [11, 12, 13, 14, 15]. Les techniques de ‘security testing ‘ sont largement utilisées pour vérifier le comportement du système réel en ce qui concerne le respect des exigences. Une forme spéciale de ‘security testing’, c'est-à-dire le test d’intrusion (Penetration Testing), est efficace pour trouver des vulnérabilités de bas niveau dans les applications en ligne (e.g., cross-site scripting), mais il se base fortement sur les compétences de l'utilisateur qui doit créer le cas de test. Les instruments de test d’

Doctorant.e: Pellegrino Giancarlo