Nous nous intéressons au sujet de la confidentialité et de la déclassification. Nous étudions en particulier l'usage d'un système de types et d'effets pour assurer de manière statique des politiques de sécurité flexibles pour un langage d'ordre supérieur impératif avec concurrence. Une méthodologie générale pour définir et prouver la correction du système de types et d'effets pour de telles propriétés est présentée. Nous considérons deux points principaux : - La question de trouver un mécanisme flexible de contrôle d'information qui permet la déclassification. Notre mécanisme de déclassification prend la forme d'une déclaration de politique locale de flux qui implémente une politique locale de flux d'information. - La question jusqu'ici inexplorée de contrôler les flux d'information dans un environnement global. Notre modèle de réseau, qui généralise l'environnement global, inclut une notion de domaine et une primitive de migration standard pour le code et les ressources. De nouvelles formes de perte d'information, introduites par la mobilité du code, sont révélées. Dans les deux cas mentionnés ci-dessus, pour prendre en compte les politiques de flux globales nous introduisons des généralisations de la non-interférence, qui sont nommées non-divulgation et non-divulgation pour les réseaux. Ces généralisations sont obtenues `a l'aide d'une représentation concrète des treillis de sécurité, où les nivaux de confidentialité sont des ensembles de principaux, semblables `a des listes de contrôle d'accès.

La criticité des systèmes complexes programmables nécessite de garantir un niveau de fiabilité et de sécurité convenable. Des études de sûreté de fonctionnement doivent être menées tout au long du cycle de développement du système. Ces études permettent une meilleure maîtrise des risques et de la fiabilité. Les points faibles sont mis en évidence et permettent aux concepteurs de spécifier des stratégies de reconfiguration avant la phase de prototype réel et les tests réels. Les études de sûreté de fonctionnement doivent être menées au plus tôt dans la phase de conception, afin de réduire les coûts et le nombre de prototypes nécessaires à la validation du système. Le travail présenté dans ce mémoire de thèse a pour objectif de définir une méthodologie de conception des systèmes complexes programmables dédiés à une application mécatronique [Belhadaoui et al., 2008-a], intégrant dès les premières phases du cycle de développement [Aït-Kadi et al., 2000], les aspects sûreté de fonctionnement. L'apport d'une telle méthodologie doit permettre de faire face à un certain nombre de contraintes propres au domaine des capteurs intelligents (les exigences de cahier des charges, le respect des normes législatives en vigueur). La méthodologie développée doit permettre de :  Modéliser et simuler les comportements fonctionnels et dysfonctionnels des systèmes  Estimer la fiabilité par modélisation  Réaliser des mesures de sensibilité afin de connaître la contribution de chaque composant à la fiabilité du système  Capitaliser la connaissance sur le système au cours des différentes phases d'évaluation (prévisionnelle, expérimentale et opérationnelle) pour affiner les estimations de fiabilité Ce Travail introduit le concept d'information en sûreté de fonctionnement. Nous interprétons la défaillance de celle-ci comme étant le résultat de l'initiation et de la propagation d'informations erronées à travers l'architecture d'un capteur intelligent dédié à une application mécatronique. Cette propagation s'est accompagnée de contraintes (partage de ressources matérielles et informationnelles, modes dégradés d'information...) qui tendent à influencer fortement la crédibilité de cette information. Nous débutons sur un état de l'art pour montrer l'intérêt de l'approche flux informationnel sur un cas d'étude complexe. Ceci est lié à la présence d'une partie programmable (interaction matériel-logiciel) et évidement du système hybride (signaux mixtes analogique-numérique). Cette nouvelle approche distingue, les phénomènes d'apparition et de disparition d'erreurs (matérielles, logicielles et environnementales), ainsi que les séquences de propagation aboutissant à un mode de dysfonctionnement du système. Grâce à cette distinction nous expliquons les concepts mal traités par les méthodes conventionnelles, tels que la défaillance simultanée, la défaillance de cause commune et abordons d'une manière réaliste les problématiques des interactions matériel-logiciel et celle des signaux mixtes. Les séquences de propagation d'erreurs générées permettent à l'aide d'un modèle markovien non homogène, de quantifier d'une manière analytique les paramètres de la sûreté de fonctionnement du système (fiabilité, disponibilité, sécurité) et de positionner le capteur dans un mode de fonctionnement parmi les six que nous avons définis suivant les spécifications du cahier des charges.

L'utilisation d'architectures électroniques et programmables tolérantes aux fautes s'accompagne de contraintes grandissantes qui tendent à influencer fortement la qualité de service de telles fonctions. Devant l'influence grandissante des défaillances multiples sur la fiabilité de fonction de sécurité, cette thèse propose une méthode permettant, par une meilleure prise en compte de l'aspect temporel, d'estimer de manière plus précise les indicateurs de performances fiabilistes d'une fonction EP dédiée à la sécurité. Ce travail introduit le concept d'information et interprète un mode de défaillance de la fonction d'étude comme le résultat de l'initiation et de la propagation d'information(s) erronée(s) jusqu'au niveau des actionneurs. Il propose donc de distinguer d'une part les phénomènes d'apparition et de disparition d'erreurs (matérielles et environnementales), et les séquences d'activation d'erreurs et événements particuliers aboutissant à un mode de défaillance du système.

La sécurité des systèmes d'information sont primordiales dans la vie d'aujourd'hui, en particulier avec la croissance des systèmes informatiques complexes et fortement interconnectés. Par exemple, les systèmes bancaires ont l'obligation de garantir l'intégrité et la confidentialité de leurs comptes clients. Le vote électronique, des ventes aux enchères et le commerce doit aussi assurer leurs la confidentialité et l'intégrité.Cependant, la vérification de la sécurité et sa mise en œuvre en distribuée sont des processus lourds en général, les compétences de sécurité avancées sont nécessaires puisque les deux configuration de sécurité et l'implementation de systèmes distribué sont complexes et sujette d'erreurs. Avec les attaques de sécurité divers menés par l'environnement Internet, comment pouvons-nous être sûrs que les systèmes informatiques que nous construisons ne satisfont la propriété de sécurité prévu?La propriété de la sécurité que nous étudions dans cette thèse est la non-ingérence, qui est une propriété globale qui permet de suivre les informations sensibles dans l'ensemble du système et de garantir la confidentialité et l'intégrité. La non-ingérence est exprimée par l'exigence selon laquelle aucune information sur des données secrètes est une fuite à travers l'observation de la variation des données publiques. Cette définition est plus subtile qu'une spécification de base de l'accès légitime pour les informations sensibles, ce qui permet d'exploiter et de détecter les dysfonctionnements et malveillants programmes intrusions pour les données sensibles (par exemple, un cheval de Troie qui envoie des données confidentielles aux utilisateurs non fiables). Cependant, comme une propriété globale, la non-interférence est difficile à vérifier et à mettre en œuvre.À cette fin, nous proposons un flux de conception basée sur un modèle qui assure la propriété non-interference dans un logiciel d'application de son modèle de haut niveau conduisant à la mise en œuvre sécurisée décentralisée. Nous présentons la plateforme secureBIP, qui est une extension pour le modèle à base de composants avec des interactions multi-partie pour la sécurité. La non-interference est garantie à l'aide de deux manières pratiques: (1) nous annotons les variables et les ports du modèle, puis selon un ensemble défini de contraintes syntaxiques suffisantes, nous vérifions la satisfaction de la propriété, (2), nous annotons partiellement le modèle, puis en extrayant ses graphes de dépendances de composition nous appliquons un algorithme de synthèse qui calcule la configuration sécurisée moins restrictive du modèle si elle existe.Une fois que la sécurité des flux d'information est établie et la non-interference est établie sur un modèle de haut niveau du système, nous suivons une méthode automatisée pratique pour construire une application distribuée sécurisée. Un ensemble de transformations sont appliquées sur le modèle abstrait de transformer progressivement en bas niveau des modèles distribués et enfin à la mise en œuvre distribuée, tout en préservant la sécurité des flux d'information. La transformations du modèles remplacent coordination de haut niveau en utilisant des interactions multi-partites par des protocoles en utilisant des envoies et reception de messages asynchrone. La distribution est donc prouvé "sécuriser par construction" qui est, le code final est conforme à la politique de sécurité souhaitée. Pour montrer la facilité d'utilisation de notre méthode, nous appliquons et d'expérimenter sur des études et des exemples de cas réels de domaines d'application distincts. / The security of information systems are paramount in today’s life, especially with the growth of complex and highly interconnected computer systems. For instance, bank systems have the obligation to guarantee the integrity and confidentiality of their costumers accounts. The electronic voting, auctions and commerce also needs confidentiality and integrity preservation.However, security verification and its distributed implementation are heavy processes in general, advanced security skills are required since both security configuration and coding distributed systems are complex and error-prone. With the diverse security attacks leaded by the Internet advent, how can we be sure that computer systems that we are building do satisfy the intended security property?The security property that we investigate in this thesis is the noninterference, which is a global property that tracks sensitive information in the entire system and ensures confidentiality and integrity. Non-interference is expressed by the requirement that no information about secret data is leaked through the observation of public data variation. Such definition is more subtle than a basic specification of legitimate access for sensitive information, allowing to exploit and detect malfunctioning and malicious programs intrusions for sensitive data (e.g, Trojan horse that sends confidential data to untrusted users). However as a global property, the noninterference is hard to verify and implement.To this end, we propose a model-based design flow that ensures the noninterference property in an application software from its high-level model leading to decentralized secure implementation. We present the secureBIP framework that is an extension for the component-based model with multyparty interactions for security. Non-interference is guaranteed using two practical manners: (1) we annotate the entire variables and ports of the model and then according to a defined set of sufficient syntactic constraints we check the satisfaction of the property, (2) we partially annotate the model way and then by extracting its compositional dependency graphswe apply a synthesis algorithm that computes the less restrictive secure configuration of the model if it exists.Once the information flow security is established and non-interference is established on an high-level model of the system, we follow a practical automated method to build a secure distributed implementation. A set of transformations are applied on the abstract model to progressively transform it into low-level distributed models and finally to distributed implementation, while preserving information flow security. Model transformations replace high-level coordination using multiparty interactions by protocols using asynchronous Send/Receive message-passing. The distributedimplementation is therefore proven ”secure-by-construction” that is, the final code conforms to the desired security policy. To show the usability of our method, we apply and experiment it on real case studies and examples from distinct application domains.

Nous nous intéressons à la mise en œuvre des politiques de confidentialité et d'intégrité des données dans le contexte des applications Web côté client. Étant donné que la plupart des applications Web est développée en JavaScript, on propose des mécanismes statiques, dynamiques et hybrides pour sécuriser le flux d'information en Core JavaScript - un fragment de JavaScript qui retient ses caractéristiques fondamentales. Nous étudions en particulier: une sémantique à dispositif de contrôle afin de garantir dynamiquement le respect des politiques de sécurité en Core JavaScript aussi bien qu'un compilateur qui instrumente un programme avec le dispositif de contrôle proposé, un système de types qui vérifie statiquement si un programme respecte une politique de sécurité donnée, un système de types hybride qui combine des techniques d'analyse statique à des techniques d'analyse dynamique afin d'accepter des programmes surs que sa version purement statique est obligée de rejeter. La plupart des programmes JavaScript s'exécute dans un navigateur Web dans le contexte d'une page Web. Ces programmes interagissent avec la page dans laquelle ils sont inclus parmi des APIs externes fournies par le navigateur. Souvent, l'exécution d'une API externe dépasse le périmètre de l'interprète du langage. Ainsi, une analyse réaliste des programmes JavaScript côté client doit considérer l'invocation potentielle des APIs externes. Pour cela, on présente une méthodologie générale qui permet d'étendre des dispositifs de contrôle de sécurité afin qu'ils prennent en compte l'invocation potentielle des APIs externes et on applique cette méthodologie à un fragment important de l'API DOM Core Level 1. / In this thesis, we address the issue of enforcing confidentiality and integrity policies in the context of client-side Web applications. Since most Web applications are developed in the JavaScript programming language, we study static, dynamic, and hybrid enforcement mechanisms for securing information flow in Core JavaScript --- a fragment of JavaScript that retains its defining features. Specifically, we propose: a monitored semantics for dynamically enforcing secure information flow in Core JavaScript as well as a source-to-source transformation that inlines the proposed monitor, a type system that statically checks whether or not a program abides by a given information flow policy, and a hybrid type system that combines static and dynamic analyses in order to accept more secure programs than its fully static counterpart. Most JavaScript programs are designed to be executed in a browser in the context of a Web page. These programs often interact with the Web page in which they are included via a large number of external APIs provided by the browser. The execution of these APIs usually takes place outside the perimeter of the language. Hence, any realistic analysis of client-side JavaScript must take into account possible interactions with external APIs. To this end, we present a general methodology for extending security monitors to take into account the possible invocation of arbitrary APIs and we apply this methodology to a representative fragment of the DOM Core Level 1 API that captures DOM-specific information flows.

De nos jours, les ordinateurs sont omniprésents. Tous ces ordinateurs stockent et manipulent de l'information, parfois sensible, d'où l'intérêt de protéger et de confiner la dissémination de cette information. Les mécanismes de contrôle de flux d'information permettent justement d'analyser des programmes manipulant de l'information sensible, afin de prévenir les fuites d'information. Les contributions de cette thèse incluent des techniques d'analyse de programmes pour le contrôle de flux d'information tant qualitatif que quantitatif. Les techniques d'analyse qualitatives permettent la détection et la prévention des fuites d'information. Les techniques quantitatives permettent d'estimer ces fuites afin de décider si elles sont négligeables. / Computers have become widespread nowadays. All these computers store and process information. Often, some of this information is sensitive; hence the need to confine and control its dissemination. An important field in computer science, that is concerned about analysing programs in order to confine and control the release of sensitive information, is the information flow control field. The contributions of this thesis include program analysis techniques for qualitative and quantitative information flow control. Qualitative techniques aim at detecting and preventing information leaks. Quantitative techniques go beyong the detection of information leaks, by estimating the leakage in order to decide whether it is negligeable.

L'objectif de ce travail est de fournir des modèles et outils pour simplifier la construction des systèmes distribués à base de composants sécurisés, ainsi que la gestion des propriétés de sécurité, en utilisant des outils de haut niveau d'abstraction pour la configuration et la reconfiguration dynamique. En plus des propriétés d'accessibilité et de communications sécurisées classiques, nous focalisons notre travail sur une propriété des systèmes répartis plus générale : la non-interférence. Cette propriété atteste qu'il ne doit pas y avoir de flux d'information entre des parties publiques et privées du système. Ce qui implique le suivi de l'acheminement de l'information entre les différentes composantes du système distribué. Notre objectif principal est donc de proposer un modèle, accompagné d'un ensemble d'outils, garantissant la propriété de la non-interférence à la construction du système, et ce à une plus grosse granularité : celle des composants. Ces outils permettent de (1) configurer les paramètres de sécurité des composants et des liaisons entre eux, (2) vérifier la propriété de non-interférence dans le code d'un composant et entre les différents composants du système et (3) générer automatiquement le code nécessaire pour appliquer ces propriétés de sécurité. D'autre part, nous proposons une architecture permettant de vérifier dynamiquement la propriété de non-interférence dans un système réparti.

Modern organisations rely intensively on information and communication technology infrastruc- tures. Such infrastructures offer a range of services from simple mail transport agents or blogs to complex e-commerce platforms, banking systems or service hosting, and all of these depend on distributed systems. The security of these systems, with their increasing complexity, is a chal- lenge. Cloud services are replacing traditional infrastructures by providing lower cost alternatives for storage and computational power, but at the risk of relying on third party companies. This risk becomes particularly critical when such services are used to host privileged company information and applications, or customers' private information. Even in the case where companies host their own information and applications, the advent of BYOD (Bring Your Own Device) leads to new security related issues. In response, our research investigated the characterization and detection of malicious activities at the operating system level and in distributed systems composed of multiple hosts and services. We have shown that intrusions in an operating system spawn abnormal information flows, and we developed a model of dynamic information flow tracking, based on taint marking techniques, in order to detect such abnormal behavior. We track information flows between objects of the operating system (such as files, sockets, shared memory, processes, etc.) and network packets flowing between hosts. This approach follows the anomaly detection paradigm. We specify the legal behavior of the system with respect to an information flow policy, by stating how users and programs from groups of hosts are allowed to access or alter each other's information. Illegal information flows are considered as intrusion symptoms. We have implemented this model in the Linux kernel4 , as a Linux Security Module (LSM), and we used it as the basis for practical demonstrations. The experimental results validated the feasibility of our new intrusion detection principles. This research is part of a joint research project between Supélec (École supérieure d'éléctricité) and QUT (Queensland University of Technology).

Nous cherchons à améliorer l'état de l'art des implémentations de contrôle de flux d'information dans les systèmes Linux. Le contrôle de flux d'information vise à surveiller la façon dont l'information se dissémine dans le système une fois hors de son conteneur d'origine, contrairement au contrôle d'accès qui ne peut permettre d'appliquer des règles que sur la manière dont les conteneurs sont accédés. Plusieurs défis scientifiques et techniques se sont présentés. Premièrement, la base de code Linux est particulièrement grande, avec quinze millions de lignes de code réparties dans trente-mille fichiers. La première contribution de cette thèse a été un plugin pour le compilateur GCC permettant d'extraire et visualiser aisément les graphes de flot de contrôle des fonctions du noyau. Ensuite, le framework des Linux Security Modules qui est utilisé pour implémenter les moniteurs de flux d'information que nous avons étudiés (Laminar [1], KBlare [2] et Weir [3]) a été conçu en premier lieu pour le contrôle d'accès, et non de flux. La question se pose donc de savoir si le framework est implémenté de telle sorte à permettre la capture de tous les flux produits par les appels système. Nous avons créé et implémenté une analyse statique permettant de répondre à ce problème. Cette analyse statique est implémenté en tant que plugin GCC et nous a permis d'améliorer le framework LSM pour capturer tous les flux. Enfin, nous avons constaté que les moniteurs de flux actuels n'étaient pas résistants aux conditions de concurrence entre les flux et ne pouvaient pas traiter certains canaux ouverts tels que les projections de fichiers en mémoire et les segments de mémoire partagée entre processus. Nous avons implémenté Rfblare, un nouvel algorithme de suivi de flux, pour KBlare, dont nous avons prouvé la correction avec Coq. Nous avons ainsi montré que LSM pouvait être utilisé avec succès pour implémenter le contrôle de flux d'information, et que seules les méthodes formelles, permettant la mise en œuvre de méthodologie, d'analyses ou d'outils réutilisables, permettaient de s'attaquer à la complexité et aux rapides évolutions du noyau Linux. / We look forward to improving the implementations of information flow control mechanisms in Linux Operating Systems. Information Flow Control aims at monitoring how information disseminates in a system once it is out of its original container, unlike access control which can merely apply rule on how the containers are accessed. We met several scientific and technical challenges. First of all, the Linux codebase is big, over fifteen millions lines of code spread over thirty three thousand files. The first contribution of this thesis is a plugin for the GCC compiler able to extract and let a user easily visualize the control flow graphs of the Linux kernel functions. Secondly, the Linux Security Modules framework which is used to implement the information flow trackers we have reviewed (Laminar, KBlare, and Weir) was designed in the first place to implement access control, rather than information flow control. One issue is thus left open: is the framework implemented in such a way that all flows generated by system calls can be captured? We have created and implemented static analysis to address this problem and proved its correction with the Coq proof assistant system. This analysis is implemented as a GCC plugin and have allowed us to improve the LSM framework in order to capture all flows. Finally, we have noted that current information flow trackers are vulnerable to race conditions between flows and are unable to cover some overt channels of information such as files mapping to memory and shared memory segments between processes. We have implemented Rfblare, a new algorithm of flow tracking, for KBlare. The correction of this algorithm has been proved with Coq. We have showed that LSM can be used successfully to implement information flow control, and that only formal methods, leading to reusable methodology, analysis, tools, etc., are a match for the complexity and the fast-paced evolution of the Linux kernel.

Dans cette thèse, nous nous intéressons à l'évaluation efficace de requêtes top-k continues sur des flux d'informations textuelles avec des feedbacks utilisateurs. La première contribution est une généralisation des modèles de requêtes top-k continues proposés dans l'état de l'art. Cette généralisation est fondée sur une famille des scores non-homogènes définis comme une combinaison linéaire de scores d'importance de l'information (indépendants des requêtes) et de scores de pertinence du contenu avec une décroissance continue de score reflétant la fraîcheur de l'information. La deuxième contribution est la définition et la mise en ¿uvre de structures de données en mémoire pour l'indexation et l'évaluation de cette nouvelle famille de requêtes top-k continues. Nos expériences montrent que notre solution est évolutive et, limitées aux fonctions homogènes, surpasse les performances d'autres solutions. Dans la deuxième partie de cette thèse, nous considérons le problème de l'intégration des signaux de feedback à notre famille de scores non-homogènes. Nous proposons un nouveau cadre général pour l'évaluation de ces requêtes du "web en temps réel" (real-time web queries) avec un ensemble d'algorithmes minimisant le coût d'évaluation d'un signal de feedback utilisateur dynamique sur un item d'information. Enfin, nous présentons MeowsReader, notre prototype de recommandation d'actualités qui intègre l'ensemble des résultats obtenus et illustre comment une classe générale de requêtes continues top-k propose une abstraction appropriée pour la modélisation et le filtrage continu d'information sur le web "temps-réel". / In this thesis, we are interested in efficient evaluation techniques of continuous top-k queries over text and feedback streams featuring generalized scoring functions which capture dynamic ranking aspects. As a first contribution, we generalize state of the art continuous top-k query models, by introducing a general family of non-homogeneous scoring functions combining query-independent item importance with query-dependent content relevance and continuous score decay reflecting information freshness. Our second contribution consists in the definition and implementation of efficient in-memory data structures for indexing and evaluating this new family of continuous top-k queries. Our experiments show that our solution is scalable and outperforms other existing state of the art solutions, when restricted to homogeneous functions. Going a step further, in the second part of this thesis we consider the problem of incorporating dynamic feedback signals to the original scoring function and propose a new general real-time query evaluation framework with a family of new algorithms for efficiently processing continuous top-k queries with dynamic feedback scores in a real-time web context. Finally, putting together the outcomes of these works, we present MeowsReader, a real-time news ranking and filtering prototype which illustrates how a general class of continuous top-k queries offers a suitable abstraction for modelling and implementing continuous online information filtering applications combining keyword search and real-time web activity.