Orchestration et vérification de fonctions de sécurité pour des environnements intelligents / Nicolas Schnepf ; sous la direction de Stephan Merz et de Rémi Badonnel

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Catalogue Worldcat

Sécurité des systèmes

Systèmes, Analyse de

Méthodes formelles (informatique)

Qualité de service

Informatique omniprésente

SDN (architecture des réseaux d'ordinateurs)

Classification Dewey : 005.8

Merz, Stephan (Directeur de thèse / thesis advisor)

Badonnel, Rémi (1980-....) (Directeur de thèse / thesis advisor)

Charoy, François (19..-.... ; chercheur en informatique) (Président du jury de soutenance / praeses)

Secci, Stefano (1980-....) (Rapporteur de la thèse / thesis reporter)

Choppy, Christine (19..-.... ; professeur en informatique) (Rapporteur de la thèse / thesis reporter)

Vaton, Sandrine (Membre du jury / opponent)

Université de Lorraine (Organisme de soutenance / degree-grantor)

École doctorale IAEM Lorraine - Informatique, Automatique, Électronique - Électrotechnique, Mathématiques de Lorraine (Ecole doctorale associée à la thèse / doctoral school)

Laboratoire lorrain de recherche en informatique et ses applications (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Les équipements intelligents, notamment les smartphones, sont la cible de nombreuses attaques de sécurité. Par ailleurs, la mise en œuvre de mécanismes de protection usuels est souvent inadaptée du fait de leurs ressources fortement contraintes. Dans ce contexte, nous proposons d'utiliser des chaînes de fonctions de sécurité qui sont composées de plusieurs services de sécurité, tels que des pare-feux ou des antivirus, automatiquement configurés et déployés dans le réseau. Cependant, ces chaînes sont connues pour être difficiles à valider. Cette difficulté est causée par la complexité de ces compositions qui impliquent des centaines, voire des milliers de règles de configuration. Dans cette thèse, nous proposons l'architecture d'un orchestrateur exploitant la programmabilité des réseaux pour automatiser la configuration et le déploiement de chaînes de fonctions de sécurité. Il est important que ces chaînes de sécurité soient correctes afin d’éviter l'introduction de failles de sécurité dans le réseau. Aussi, notre orchestrateur repose sur des méthodes automatiques de vérification et de synthèse, encore appelées méthodes formelles, pour assurer la correction des chaînes. Notre travail appréhende également l'optimisation du déploiement des chaînes dans le réseau, afin de préserver ses ressources et sa qualité de service.

Résumé / Abstract : Smart environments, in particular smartphones, are the target of multiple security attacks. Moreover, the deployment of traditional security mechanisms is often inadequate due to their highly constrained resources. In that context, we propose to use chains of security functions which are composed of several security services, such as firewalls or antivirus, automatically configured and deployed in the network. Chains of security functions are known as being error prone and hard to validate. This difficulty is caused by the complexity of these constructs that involve hundreds and even thousands of configuration rules. In this PhD thesis, we propose the architecture of an orchestrator, exploiting the programmability brought by software defined networking, for the automated configuration and deployment of chains of security functions. It is important to automatically insure that these security chains are correct, before their deployment in order to avoid the introduction of security breaches in the network. To do so, our orchestrator relies on methods of automated verification and synthesis, also known as formal methods, to ensure the correctness of the chains. Our work also consider the optimization of the deployment of chains of security functions in the network, in order to maintain its resources and quality of service.