Analyse de sécurité de systèmes IoT à l’aide d’arbres d’attaques

LoT is a rapidly emerging paradigm that provides a way to the user to instrument and control a large variety of objects interacting between each other over the Internet. In IoT systems, the security risks are multiplied as they involve hetero- geneous devices that are connected to a shared network and that carry critical tasks, and hence, are targets for malicious users. In this thesis, we propose a security-based framework for modeling IoT systems where attack trees are defined alongside the model to detect and prevent security risks in the system. The language we implemented aims to model the IoT paradigm in a simple way. The IoT systems are composed of entities having some communication capabilities between each other. Two entities can communicate if (i) they are connected through a communication protocol and (ii) they satisfy some constraints imposed by the protocol. In order to identify and analyze attacks on the security of a system we use attack trees which are an intuitive and practical formal method to do so. A successful attack can be a rare event in the execution of a well-designed system. When rare, such attacks are hard to detect with usual model checking techniques. Hence, we use importance splitting as a statistical model checking technique for rare events.L’Internet des Objects (IoT) est un modèle qui évolue rapidement et qui permet à des utilisateursd’utiliser et contrôler une large variété d’objets connectés entre eux. Ces environnementsconnectés augmentent la surface d’attaque d’un système puisque les risques sont multipliés parle nombre d’appareils connectés. Ces appareils sont responsables de tâches plus ou moinscritiques, et peuvent donc être la cible d’utilisateurs malveillants. Dans ce travail de thèse nousprésentons une méthodologie pour évaluer la sécurité de systèmes IoT. Nous proposons unemanière de représenter les systèmes IoT, couplée avec des arbres d’attaques afin d’évaluer leschances de succès d’une attaque sur un système donné. La représentation des systèmes est faitevia un langage formel que nous avons développé : SOML (Security Oriented Modeling Language).Ce langage permet de définir le comportement des différents acteurs du système et d’ajouterdes probabilités sur leurs actions. L’abre d’attaque nous offre un moyen simple et formel dereprésenter de possibles attaques sur le système. L’analyse probabiliste est ensuite effectuée viaun outil de Statistical Model Checking : Plasma. Nous utilisons deux algorithmescomplémentaires pour effectuer cette analyse : Monte Carlo et importance splitting