Cette thèse traite du problème d’une protection en profondeur qui puisse être assurée par un système d’exploitation. Elle établit la faiblesse des solutions existantes pour l’expression des besoins de sécurité. Les approches supportent en général une seule propriété de sécurité. Nous proposons donc un langage qui permet de formaliser un large ensemble de propriétés de sécurité. Ce langage exprime les activités système directes et transitives. Il permet de formaliser la majorité des propriétés de confidentialité et d’intégrité de la littérature. Il est adapté à l’expression de modèles de protection dynamique. A titre d’exemple, un nouveau modèle dynamique est proposé pour la protection des différents domaines d’usage d’un navigateur Web. Nous définissons une méthode de compilation du langage pour analyser les appels systèmes réalisés par les processus utilisateurs. La compilation repose sur la construction et l’analyse d’un graphe de flux d’information. Nous montrons qu’en pratique la complexité reste faible. Une implantation de ce langage est proposée sous la forme d’un contrôle d’accès mandataire dynamique pour Linux. Une expérimentation à large échelle a été réalisée sur des pots-de-miel à haute interaction. Notre protection a montré son efficacité aussi bien pour les serveurs que les postes client. Il présente des perspectives intéressantes aussi bien pour la protection des systèmes que pour l’analyse de vulnérabilités. Ce travail a contribué au projet SPACLik vainqueur du défi sécurité de l’ANR SEC&SI. / The subject of this thesis is to propose an in-depth protection that can be enforced by the operating system. First, we present that current security solutions are weak in the expression of security. Indeed, most of them support only one security properties. We introduce a language that allows to formalize a large set of security properties. This language expresses directs and transitives system activities. It allows to formalize the majority of integrity and confidentiality security properties introduced in the litterature. Moreover, the language can also expresses dynamic security properties. We introduces a new dynamic security model for the protection of multiple security domains managed by a web browser. We define a method to compil our language. The purpose is to analyze the system call done by the users processes. The compilation process build and analyze an information flow graph. Futhermore, we show that the complexity of our protection solution is low. We propose an implementation of this language as a dynamic mandatory access control for Linux. We experiment it on large scale high interaction honeypots. Our protection shows its efficiency both for clients and servers. Moreover, it presents interesting perspectives for the protection of other systems and for the vulnerability analysis. This work has contributed to the SPACLik project that wins the security contest of the French National Research Agency : ANR SEC&SI.

Cette thèse traite du problème d'une protection en profondeur qui puisse être assurée par un système d'exploitation. Elle établit la faiblesse des solutions existantes pour l'expression des besoins de sécurité. Les approches supportent en général une seule propriété de sécurité. Nous proposons donc un langage qui permet de formaliser un large ensemble de propriétés de sécurité. Ce langage exprime les activités système directes et transitives. Il permet de formaliser la majorité des propriétés de confidentialité et d'intégrité de la littérature. Il est adapté à l'expression de modèles de protection dynamique. A titre d'exemple, un nouveau modèle dynamique est proposé pour la protection des différents domaines d'usage d'un navigateur Web. Nous définissons une méthode de compilation du langage pour analyser les appels systèmes réalisés par les processus utilisateurs. La compilation repose sur la construction et l'analyse d'un graphe de flux d'information. Nous montrons qu'en pratique la complexité reste faible. Une implantation de ce langage est proposée sous la forme d'un contrôle d'accès mandataire dynamique pour Linux. Une expérimentation à large échelle a été réalisée sur des pots-de-miel à haute interaction. Notre protection a montré son efficacité aussi bien pour les serveurs que les postes client. Il présente des perspectives intéressantes aussi bien pour la protection des systèmes que pour l'analyse de vulnérabilités. Ce travail a contribué au projet SPACLik vainqueur du défi sécurité de l'ANR SEC&SI.

La mise en oeuvre de systèmes autonomes nécessite le développement et l'utilisation d'architectures logicielles multi-couches qui soient adaptées. Typiquement, une couche fonctionnelle renferme des modules en charge de commander les éléments matériels du système et de fournir des services élémentaires. Pour être robuste, la couche fonctionnelle doit être dotée de mécanismes de protection vis-à-vis de requêtes erronées ou inopportunes issues de la couche supérieure. Nous présentons une méthodologie pour tester la robustesse de ces mécanismes. Nous définissons un cadre général pour évaluer la robustesse d'une couche fonctionnelle par la caractérisation de son comportement vis-à-vis de requêtes inopportunes. Nous proposons également un environnement de validation basé sur l'injection de fautes dans le logiciel de commande d'un robot simulé. Un grand nombre de cas de tests est généré automatiquement par la mutation d'une séquence de requêtes valides. Les statistiques descriptives des comportements en présence de requêtes inopportunes sont analysées afin d'évaluer la robustesse du système sous test.

La mise en oeuvre de systèmes autonomes nécessite le développement et l'utilisation d'architectures logicielles multi-couches qui soient adaptées. Typiquement, une couche fonctionnelle renferme des modules en charge de commander les éléments matériels du système et de fournir des services élémentaires. Pour être robuste, la couche fonctionnelle doit être dotée de mécanismes de protection vis-à-vis de requêtes erronées ou inopportunes issues de la couche supérieure. Nous présentons une méthodologie pour tester la robustesse de ces mécanismes. Nous définissons un cadre général pour évaluer la robustesse d'une couche fonctionnelle par la caractérisation de son comportement vis-à-vis de requêtes inopportunes. Nous proposons également un environnement de validation basé sur l'injection de fautes dans le logiciel de commande d'un robot simulé. Un grand nombre de cas de tests est généré automatiquement par la mutation d'une séquence de requêtes valides. Les statistiques descriptives des comportements en présence de requêtes inopportunes sont analysées afin d'évaluer la robustesse du système sous test. / The implementation of autonomous systems requires the development and the using of multi-layer software architecture. Typically, a functional layer contains several modules that control the material of the system and provide elementary services. To be robust, the functional layer must be implemented with protection mechanisms with respect to erroneous or inopportune requests sent from the superior layer. We present a methodology for robustness testing these mechanisms. We define a general framework to evaluate the robustness of a functional layer by characterizing its behavior with respect to inappropriate requests. We also propose an validation environment based on fault injection in the control software of a simulated robot. A great number of test cases is generated automatically by the mutation of a sequence of valid requests. The descriptive statistics of the behaviors in the presence of inappropriate requests are analyzed in order to evaluate the robustness of the system under test.

Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA. / Software-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA.

Les environnements d’informatique en nuage sont des environnements hétérogènes et dynamiques, ce qui les rend complexes à sécuriser. Dans cette thèse, nous proposons un langage et une architecture permettant d’exprimer et d’appliquer des propriétés de sécurité dans un environnement en nuage. Le langage permet à un client de l’informatique en nuage d’exprimer des besoins de sécurité sans préciser comment ils seront appliqués. Le langage se base sur des contextes abstrayant les ressources et des propriétés correspondant aux besoins de sécurité. Les propriétés sont ensuite appliquées en utilisant les mécanismes de sécurité disponibles (tels que SELinux, PAM, iptables ou firewalld) via une architecture autonome. Cette architecture permet d’abstraire et de réutiliser les capacités de sécurité des mécanismes existants. Une propriété de sécurité est ainsi définie comme une combinaison de capacités et peut être appliquée grâce à la collaboration de plusieurs mécanismes. Les mécanismes sont alors automatiquement configurés en accord avec les propriétés établies par l’utilisateur. L’architecture dispose aussi d’un système d’assurance qui lui permet de détecter une défaillance d’un mécanisme ou une erreur d’application. L’architecture peut ainsi répondre aux problèmes rencontrés, par exemple en ré-appliquant des propriétés avec d’autres mécanismes. De plus, le système d’assurance fournit une évaluation de l’application des propriétés. La thèse propose ainsi un système autonome d’application et d’assurance de la sécurité dans des environnements hétérogènes. / Cloud environnements are heterogeneous and dynamic, which makes them difficult to protect. In this thesis, we introduce a language and an architecture that can be used to express and enforce security properties in a Cloud. The language allows a Cloud user to express his security requirements without specifying how they will be enforced. The language is based on contexts (to abstract the resources) and properties (to express the security requirements). The properties are then enforced through an autonomic architecture using existing and available security mechanisms (such as SELinux, PAM, iptables, or firewalld). This architecture abstracts and reuses the security capabilities of existing mechanisms. A security property is thus defined by a combination of capabilities and can be enforced through the collaboration of several mechanisms. The mechanisms are then automatically configured according to the user-defined properties. Moreover, the architecture offers an assurance system to detect the failure of a mechanism or an enforcement error. Therefore, the architecture can address any problem, for instance by re-applying a property using different mechanisms. Lastly, the assurance system provides an evaluation of the properties enforcement. This thesis hence offers an autonomic architecture to enforce and assure security in Cloud environnements.

La composition automatique de services web est une tâche difficile. De nombreux travaux ont considérés des modèles simplifiés d'automates qui font abstraction de la structure des messages échangés par les services. Pour le domaine des services sécurisés nous proposons une nouvelle approche pour automatiser la composition des services basée sur leurs politiques de sécurité. Étant donnés, une communauté de services et un service objectif, nous réduisons le problème de la synthèse de l'objectif à partir des services dans la communauté à un problème de sécurité, où un intrus que nous appelons médiateur doit intercepter et rediriger les messages depuis et vers la communauté de services et un service client jusqu'à atteindre un état satisfaisant pour le dernier. Nous avons implémenté notre algorithme dans la plateforme de validation du projet AVANTSSAR et nous avons testé l'outil correspondant sur plusieurs études de cas. Ensuite, nous présentons un outil qui compile les traces obtenues décrivant l'exécution d'un médiateur vers le code exécutable correspondant. Pour cela nous calculons d'abord une spécification exécutable aussi prudente que possible de son rôle dans l'orchestration. Cette spécification est exprimé en ASLan, un langage formel conçu pour la modélisation des services Web liés à des politiques de sécurité. Ensuite, nous pouvons vérifier avec des outils automatiques que la spécification ASLan obtenue vérifie certaines propriétés requises de sécurité telles que le secret et l'authentification. Si aucune faille n'est détectée, nous compilons la spécification ASLan vers une servlet Java qui peut être utilisé par le médiateur pour contrôler l'orchestration / Automatic composition of web services is a challenging task. Many works have considered simplified automata models that abstract away from the structure of messages exchanged by the services. For the domain of secured services we propose a novel approach to automated composition of services based on their security policies. Given a community of services and a goal service, we reduce the problem of composing the goal from services in the community to a security problem where an intruder we call mediator should intercept and redirect messages from the service community and a client service till reaching a satisfying state. We have implemented the algorithm in AVANTSSAR Platform and applied the tool to several case studies. Then we present a tool that compiles the obtained trace describing the execution of a the mediator into its corresponding runnable code. For that we first compute an executable specification as prudent as possible of her role in the orchestration. This specification is expressed in ASLan language, a formal language designed for modeling Web Services tied with security policies. Then we can check with automatic tools that this ASLan specification verifies some required security properties such as secrecy and authentication. If no flaw is found, we compile the specification into a Java servlet that can be used by the mediatior to lead the orchestration