Tesis sobre el tema "Isolation de l'accès à la mémoire"

En tant que composant important de la plate-forme cloud, le commutateur virtuel (vSwitch) est responsable de la réalisation de la connectivité réseau entre les machines virtuelles (VM) et les périphériques externes. La plupart des vSwitches existants adoptent le principe de conception partagée, qui détruit l'isolation entre les VMs. Dans vSwitch, différentes VMs se disputent les ressources partagées et accèdent à la mémoire sans restriction, cela les rend incapables de garantir une qualité de service (QoS) réseau stable, tout en faisant face au risque d'attaques de plans de données et d'accès illégaux à la mémoire. Afin de résoudre ces problèmes de performance, de défaillance et de sécurité causés par le manque d'isolement, les principaux travaux et contributions de cette thèse sont les suivants : 1) Méthode QoS réseau basée sur l'isolation du cycle CPU (C2QoS). Cette approche garantit la bande passante du réseau VM en isolant la concurrence des ressources CPU, et en même temps réduisant de 80 % la latence supplémentaire du réseau de VM causée par la concurrence. 2) Mécanisme de défense contre les attaques du plan de données basé sur l'isolement de la table de flux (D-TSE). D-TSE utilise VM comme unité pour séparer la structure de la table de flux afin d'obtenir des performances de classification de paquets indépendantes et une isolation des pannes au prix d'une utilisation CPU supplémentaire de 5 %. 3) Mécanisme d'E/S réseau virtualisé (VNIO) basé sur l'isolation de l'accès mémoire (S2H). Basé sur un modèle de partage de mémoire sécurisé, S2H assure l'isolation et la sécurité de la mémoire des VM au prix d'une latence accrue de 2 à 9 %
As an important component of cloud platform, virtual switch (vSwitch) is responsible for achieving network connectivity between virtual machines (VMs) and external devices. Most existing vSwitches adopt the split design principle, which destroys the isolation between VMs. In vSwitch, different VMs compete for shared resources and unrestricted memory access, making them unable to guarantee stable network quality of service (QoS), while facing the risk of data plane attacks and illegal access to memory. In order to solve these performance, failure and security problems caused by the lack of isolation, the main works and contributions of this thesis are as follows: 1) Network QoS method based on CPU cycle isolation (C2QoS). This approach secures VM network bandwidth by isolating concurrency from CPU resources, and at the same time reduces additional VM network latency caused by concurrency by 80%. 2) Data plane attack defense mechanism based on stream table isolation (D-TSE). D-TSE uses VM as the unit to separate the flow table structure to achieve independent packet classification performance and fault isolation at the cost of 5% additional CPU usage. 3) Virtualized Network I/O (VNIO) mechanism based on Memory Access Isolation (S2H). Based on a secure memory sharing model, S2H provides VM memory isolation and security at the cost of 2-9% increased latency

Notre recherche s'inscrit dans le cadre de la sociologie de la mémoire. L'étude intègre la définition de la mémoire individuelle dans ses conditions sociales de constitution et comme point de vue de l'agent. Nous regardons la production des souvenirs de l'accès à une profession comme expression de l'identité pour soi. L’individu actualise sa mémoire de manière à produire son point de vue sur sa définition objective. Il confirme, infirme ou nuance l'idée de son identité véhiculée par sa profession. Nous accueillons ici l'hypothèse de la dualité entre identité pour soi et identité pour autrui. Une enquête par entretien nous a permis de construire trois manières d'exprimer le point de vue de l'individu sur lui-même et indissociablement son rapport à sa profession, à sa définition pour autrui. Les discours recueillis ne peuvent être analyses ni en terme de mémoire rétrospective ni en terme de mémoire prospective. Nos informateurs affirment, au travers de scènes se développant sur la même trame, ou au travers d'un discours construit autour des mêmes oppositions, une identité avec soi-même. La mémoire qui est ainsi produite est introspective. Selon le rapport à la profession, cette mémoire est celle de l'action, de la virtualité ou de l'indétermination
Our research gets place in sociology of memory. This study integrates the definition of the individual memory in its social conditions of composition and as the point of view of a person. We consider the production of memory in professional access as expression of identity for oneself. The individual actualizes his memory by forming his point of view according to his self-definition. He confirms, denies or changes the idea of his self by means of his profession. We make a distinction between identity for oneself and identity for others. An examination by interview allowed us to frame three ways to express the point of view of the individual on himself together with the relation to his job. There is no possibility to analyze the collected speeches in terms of retrospective memory or prospective memory. Our informants maintain trough acts developing on the same theme, or through speeches constructed around the same oppositions, an identity with oneself. The memory produced in this way in an introspective one. According to the relation to profession, introspective memory is one of action, of potentiality, or of indefiniteness

Cette thèse porte sur la sécurité des programmes et particulièrement en utilisant la compilation pour parvenir à ses fins. La compilation correspond à la traduction des programmes sources écrits par des humains vers du code machine lisible par nos systèmes. Nous explorons les deux manières possible de faire de la compilation sécurisée : la sécurisation et la préservation. Premièrement, nous avons développé CompCertSFI, un compilateur qui sécurise des modules en les isolant dans des zones mémoires restreintes appelées bac à sable. Ces modules sont ensuite incapables d'accéder à des zones mémoires hors de leur bac à sable, ce qui empêche un module malveillant de corrompre d'autres entités du système. Sur le sujet de la préservation, nous avons défini une notion de Préservation de Flot d'Information qui s'applique aux transformations de programme. Cette propriété, lorsqu'elle est appliquée, permet de s'assurer qu'un programme ne devienne moins sécurité durant sa compilation. Notre propriété de préservation est spécifiquement conçus pour préserver les protections contre les attaques de type canaux cachés. Cette nouvelle catégorie d'attaque utilise des médiums physique comme le temps ou la consommation d'énergie qui ne sont pas pris en compte par les compilateurs actuels
Our society has been growingly dependent on computer systems and this tendency will not slow down in the incoming years. Similarly, interests over cybersecurity have been increasing alongside the possible consequences brought by successful attacks on these systems. This thesis tackles the issue of security of systems and especially focuses on compilation to achieve its goal. Compilation is the process of translating source programs written by humans to machine code readable by our systems. We explore the two possible behaviours of a secure compiler which are enforcement and preservation. First, we have developed CompCertSFI, a compiler which enforces the isolation of modules into closed memory areas called sandboxes. These modules are then unable to access memory regions outside of their sandbox which prevents any malicious module from corrupting other entities of the system. On the topic of security preservation, we defined a notion of Information Flow Preserving transformation to make sure that a program does get less secure during compilation. Our property is designed to preserve security against side-channel attacks. This new category of attacks uses physical mediums such as time or power consumption which are taken into account by current compilers

L'évolution de la technologie VLSI permet aux systèmes sur puce (SoCs) d'intégrer de nombreuses fonctions hétérogènes dans une seule puce et demande, en raison de contraintes économiques, une unique mémoire externe partagée (SDRAM). Par conséquent, la conception du système de mémoire principale, et plus particulièrement l'architecture du contrôleur de mémoire, est devenu un facteur très important dans la détermination de la performance globale du système. Le choix d'un contrôleur de mémoire qui répond aux besoins de l'ensemble du système est une question complexe. Cela nécessite l'exploration de l'architecture du contrôleur de mémoire, puis la validation de chaque configuration par simulation. Bien que l'exploration de l'architecture du contrôleur de mémoire soit un facteur clé pour une conception réussite d'un système, l'état de l'art sur les contrôleurs de mémoire ne présente pas des architectures aussi flexibles que nécessaire pour cette tâche. Même si certaines d'entre elles sont configurables, l'exploration est restreinte à des ensembles limités de paramètres tels que la profondeur des tampons, la taille du bus de données, le niveau de la qualité de service et la distribution de la bande passante. Plusieurs classes de trafic coexistent dans les applications réelles, comme le trafic de service au mieux et le trafic de service garanti qui accèdent à la mémoire partagée d'une manière concurrente. En conséquence, la considération de l'interaction entre le système de mémoire et la structur d'interconnexion est devenue vitale dans les SoCs actuels. Beaucoup de réseaux sur puce (NoCs) fournissent des services aux classes de trafic pour répondre aux exigences des applications. Cependant, très peu d'études considèrent l'accès à la SDRAM avec une approche système, et prennent en compte la spécificité de l'accès à la SDRAM dans les systèmes sur puce à base de réseaux intégrés. Cette thèse aborde le sujet de l'accès à la mémoire dynamique SDRAM dans les systèmes sur puce à base de réseaux intégrés. Nous introduisons une architecture de contrôleur de mémoire totalement configurable basée sur des blocs fonctionnels configurables, et proposons un modèle de simulation associé relativement précis temporellement et à haut niveau d'abstraction. Ceci permet l'exploration du sous-système de mémoire grâce à la facilité de configuration de l'architecture du contrôleur de mémoire. En raison de la discontinuité de services entre le réseau sur puce et le contrôleur de mémoire, nous proposons également dans le cadre de cette thèse un protocole de contrôle de flux de bout en bout pour accéder à la mémoire à travers un contrôleur de mémoire multiports. L'idée, simple sur le principe mais novatrice car jamais proposée à notre connaissance, se base sur l'exploitation des informations sur l'état du contrôleur de mémoire dans le réseau intégré. Les résultats expérimentaux montrent qu'en contrôlant l'injection du trafic de service au mieux dans le réseau intégré, notre protocole augmente les performances du trafic de service garanti en termes de bande passante et de latence, tout en préservant la bande passante moyenne du trafic de service au mieux.

L'évolution de la technologie VLSI permet aux systèmes sur puce (SoCs) d'intégrer de nombreuses fonctions hétérogènes dans une seule puce et demande, en raison de contraintes économiques, une unique mémoire externe partagée (SDRAM). Par conséquent, la conception du système de mémoire principale, et plus particulièrement l'architecture du contrôleur de mémoire, est devenu un facteur très important dans la détermination de la performance globale du système. Le choix d'un contrôleur de mémoire qui répond aux besoins de l'ensemble du système est une question complexe. Cela nécessite l'exploration de l'architecture du contrôleur de mémoire, puis la validation de chaque configuration par simulation. Bien que l'exploration de l'architecture du contrôleur de mémoire soit un facteur clé pour une conception réussite d'un système, l'état de l'art sur les contrôleurs de mémoire ne présente pas des architectures aussi flexibles que nécessaire pour cette tâche. Même si certaines d'entre elles sont configurables, l'exploration est restreinte à des ensembles limités de paramètres tels que la profondeur des tampons, la taille du bus de données, le niveau de la qualité de service et la distribution de la bande passante. Plusieurs classes de trafic coexistent dans les applications réelles, comme le trafic de service au mieux et le trafic de service garanti qui accèdent à la mémoire partagée d'une manière concurrente. En conséquence, la considération de l'interaction entre le système de mémoire et la structure d'interconnexion est devenue vitale dans les SoCs actuels. Beaucoup de réseaux sur puce (NoCs) fournissent des services aux classes de trafic pour répondre aux exigences des applications. Cependant, très peu d'études considèrent l'accès à la SDRAM avec une approche système, et prennent en compte la spécificité de l'accès à la SDRAM dans les systèmes sur puce à base de réseaux intégrés. Cette thèse aborde le sujet de l'accès à la mémoire dynamique SDRAM dans les systèmes sur puce à base de réseaux intégrés. Nous introduisons une architecture de contrôleur de mémoire totalement configurable basée sur des blocs fonctionnels configurables, et proposons un modèle de simulation associé relativement précis temporellement et à haut niveau d'abstraction. Ceci permet l'exploration du sous-système de mémoire grâce à la facilité de configuration de l'architecture du contrôleur de mémoire. En raison de la discontinuité de services entre le réseau sur puce et le contrôleur de mémoire, nous proposons également dans le cadre de cette thèse un protocole de contrôle de flux de bout en bout pour accéder à la mémoire à travers un contrôleur de mémoire multiports. L'idée, simple sur le principe mais novatrice car jamais proposée à notre connaissance, se base sur l'exploitation des informations sur l'état du contrôleur de mémoire dans le réseau intégré. Les résultats expérimentaux montrent qu'en contrôlant l'injection du trafic de service au mieux dans le réseau intégré, notre protocole augmente les performances du trafic de service garanti en termes de bande passante et de latence, tout en préservant la bande passante moyenne du trafic de service au mieux
The ongoing advancements in VLSI technology allow System-on-Chip (SoC) to integrate many heterogeneous functions into a single chip, but still demand, because of economical constraints, a single and shared main off-chip SDRAM. Consequently, main memory system design, and more specifically the architecture of the memory controller, has become an increasingly important factor in determining the overall system performance. Choosing a memory controller design that meets the needs of the whole system is a complex issue. This requires the exploration of the memory controller architecture, and then the validation of each configuration by simulation. Although the architecture exploration of the memory controller is a key to successful system design, state of the art memory controllers are not as flexible as necessary for this task. Even if some of them present a configurable architecture, the exploration is restricted to limited sets of parameters such as queue depth, data bus size, quality-of-service level, and bandwidth distribution. Several classes of traffic co-exist in real applications, e.g. best effort traffic and guaranteed service traffic, and access the main memory. Therefore, considering the interaction between the memory subsystem and the interconnection system has become vital in today's SoCs. Many on chip networks provide guaranteed services to traffic classes to satisfy the applications requirements. However, very few studies consider the SDRAM access within a system approach, and take into account the specificity of the SDRAM access as a target in NoC-based SoCs. This thesis addresses the topic of dynamic access to SDRAM in NoC-based SoCs. We introduce a totally customizable memory controller architecture based on fully configurable building components and design a high level cycle approximate model for it. This enables the exploration of the memory subsystem thanks to the ease of configuration of the memory controller architecture. Because of the discontinuity of services between the network and the memory controller, we also propose within the framework of this thesis an Extreme End to End flow control protocol to access the memory device through a multi-port memory controller. The simple yet novel idea is to exploit information about the memory controller status in the NoC. Experimental results show that by controlling the best effort traffic injection in the NoC, our protocol increases the performance of the guaranteed service traffic in terms of bandwidth and latency, while maintaining the average bandwidth of the best effort traffic

Cette thèse cherche à définir la fonction du chant dans un système nord-amérindien de transmission orale des savoirs, et cela à l’exemple des Shuswap, qui attribuent une grande importance à leur « propriété intellectuelle ». La thèse est divisée en 4 sections. Section 1 comporte une introduction ethnographique générale au travail (l’ »aire culturelle » du Plateau et son histoire, ensuite les Secwepemc plus précisément) et présente le concept de la thèse, fondée sur une méthode de travail combinant une longue recherche sur le terrain et l’étude des sources écrites. Section 2 confronte les études éthno-musicologiques existantes sur le Plateau avec la manière secwepemc. Section 3 présente quelques aspects de la manière secwepemc de concevoir le « monde intégral », ainsi que les trois systèmes de classification du répertoire (utilisation, origine, droits d’accès). Section 4 comporte l’analyse de la place du chant face à d’autres voies de transmission orale (cérémonies, rituels, mythes et histoires), et la tentative d’approcher de manière holistique cette culture à partir de sa conception du chant
Cette thèse cherche à définir la fonction du chant dans un système nord-amérindien de transmission orale des savoirs, et cela à l’exemple des Shuswap, qui attribuent une grande importance à leur « propriété intellectuelle ». La thèse est divisée en 4 sections. Section 1 comporte une introduction ethnographique générale au travail (l’ »aire culturelle » du Plateau et son histoire, ensuite les Secwepemc plus précisément) et présente le concept de la thèse, fondée sur une méthode de travail combinant une longue recherche sur le terrain et l’étude des sources écrites. Section 2 confronte les études éthno-musicologiques existantes sur le Plateau avec la manière secwepemc. Section 3 présente quelques aspects de la manière secwepemc de concevoir le « monde intégral », ainsi que les trois systèmes de classification du répertoire (utilisation, origine, droits d’accès). Section 4 comporte l’analyse de la place du chant face à d’autres voies de transmission orale (cérémonies, rituels, mythes et histoires), et la tentative d’approcher de manière holistique cette culture à partir de sa conception du chant

Ce travail de thèse, s'inscrit dans une vision où la mémoire est considérée comme un système unique conservant l'ensemble de nos expériences vécues sous forme de traces multidimensionnelles, c'est-à-dire reflétant les propriétés sensori-motrices de nos expériences passées. De plus, dans cette perspective, les connaissances ne sont pas récupérées en mémoire (i.e. mémoire de contenu) mais émergent de l'interaction entre la situation actuelle et les traces de situations passées (i.e. mémoire des processus). Cette émergence des connaissances est le produit de la dynamique de mécanismes d'activation et d'intégration (modèle Act-In, Versace et al, 2014). Notre objectif était d'étudier l'influence de cette dynamique sur l'efficacité d'une activité discriminante, c'est-à-dire sur notre capacité à distinguer une connaissance d'une autre connaissance (e.g. rappel, reconnaissance). Nous avons alors réalisé deux séries d'expériences, afin de montrer que cette efficacité dépend à la fois des caractéristiques de la trace (i.e. distinctivité de la trace) et de celles de la situation (i.e. similarité entre les indices de récupération et les traces). Dans un premier temps, nous avons choisi de manipuler la distinctivité de la trace par le biais d'un paradigme d'isolation. Dans un deuxième temps nous nous sommes centrés sur la similarité motrice entre la situation de récupération et les traces d'expériences passées. La difficulté à observer des différences significatives (1ère série d'expériences) et l'originalité de certains résultats (2ème série d'expériences) tendent à confirmer l'idée d'une mémoire permettant la construction d'un comportement en réponse à une situation donnée
This thesis is part of a vision where memory is considered as a unique system maintaining all of our experiences in multidimensional memory traces, that is to say, reflecting sensorimotor properties from our past experiences. Moreover, from this perspective, knowledge is not retrieved in memory (i.e. memory content), but emerges from the interaction between the current situation and traces of past situations (i.e. memory processes). This emerging knowledge is the product of the dynamics of activation and integration mechanisms (Act-In Model, Versace et al, 2014). Our objective was to investigate the influence of these dynamics on the effectiveness of discriminant activity, that is to say, our ability to distinguish one specific knowledge from other ones (e.g. recall, recognition). We then conducted two sets of experiments to show that this efficiency depends on both the characteristics of the memory trace (i.e. trace distinctiveness) and those of the situation (i.e. similarity between the retrieval cues and memory traces). Primarily, we chose to manipulate the trace distinctiveness through an isolation paradigm. Secondly we focused on motor similarity between the retrieval situation and traces of past experiences. The difficulty to observe significant differences (first serie of experiments) and the originality of some results (second serie of experiments) tend to support the idea of a memory allowing the construction of behavior in response to a given situation

Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C.

Dans cette thèse nous proposons un nouveau concept de noyau adapté à la preuve que nous avons appelé « proto-noyau ». Il s’agit d’un noyau de système d’exploitation minimal où la minimisation de sa taille est principalement motivée par la réduction du coût de la preuve mais aussi de la surface d’attaque. Ceci nous amène à définir une nouvelle stratégie de « co-design » du noyau et de sa preuve. Elle est fondée principalement sur les feedbacks entre les différentes phases de développement du noyau, allant de la définition des besoins jusqu’à la vérification formelle de ses propriétés. Ainsi, dans ce contexte nous avons conçu et implémenté le proto-noyau Pip. L’ensemble de ses appels système a été choisi minutieusement pendant la phase de conception pour assurer à la fois la faisabilité de la preuve et l’utilisabilité du système. Le code de Pip est écrit en Gallina (le langage de spécification de l’assistant de preuve Coq) puis traduit automatiquement vers le langage C. La propriété principale étudiée dans ces travaux est une propriété de sécurité, exprimée en termes d’isolation mémoire. Cette propriété a été largement étudiée dans la littérature de par son importance. Ainsi, nos travaux consistent plus particulièrement à orienter le développement des concepts de base de ce noyau minimaliste par la vérification formelle de cette propriété. La stratégie de vérification a été expérimentée, dans un premier temps, sur un modèle générique de micro-noyau que nous avons également écrit en Gallina. Par ce modèle simplifié de micro-noyau nous avons pu valider notre approche de vérification avant de l’appliquer sur l’implémentation concrète du proto-noyau Pip
In this thesis we propose a new kernel concept adapted to verification that we have called protokernel. It is a minimal operating system kernel where the minimization of its size is motivated by the reduction of the cost of proof and of the attack surface. This leads us to define a new strategy of codesign of the kernel and its proof. It is based mainly on the feedbacks between the various steps of development of the kernel, ranging from the definition of its specification to the formal verification of its properties. Thus, in this context we have designed and implemented the Pip protokernel. All of its system calls were carefully identified during the design step to ensure both the feasibility of proof and the usability of the system. The code of Pip is written in Gallina (the specification language of the Coq proof assistant) and then automatically translated into C code. The main property studied in this work is a security property, expressed in terms of memory isolation. This property has been largely discussed in the literature due to its importance. Thus, our work consists more particularly in guiding the developer to define the fundamental concepts of this minimalistic kernel through the formal verification of its isolation property. The verification strategy was first experimented with a generic microkernel model that we also wrote in Gallina. With this simplified microkernel model we were able to validate our verification approach before applying it to the concrete implementation of the Pip protokernel

Les travaux présentés dans ce mémoire ont pour objectif de renforcer le niveau de sûreté et de sécurité des systèmes embarqués dans les cartes à puce grâce à l'utilisation des Méthodes Formelles. D'une part nous présentons la vérification formelle de l'isolation des données de différentes applications chargées sur une même carte à puce, et plus précisément la preuve formelle, dans le système de preuve Coq, que le contrôle dynamique d'accès aux données implémenté par Java Card assure les propriétés de confidentialité et d'intégrité. D'autre part, nous nous sommes intéressés à la correction et à l'innocuité du code source bas niveau d'un système d'exploitation embarqué. Cette étude est illustrée par un module de gestion de mémoire Flash par journalisation, assurant la cohérence des données de la mémoire en cas d'arrachage de la carte du terminal. La vérification de propriétés fonctionnelles et locales a été développée à l'aide de l'outil Caduceus. Cet outil n'acceptant pas certaines constructions de bas niveau du langage C, telles que les unions et les casts, nous proposons des solutions pour la formalisation de ces constructions. Nous proposons également une extension de Caduceus permettant de spécifier et de vérifier le comportement d'une fonction en cas d'interruption soudaine de son exécution. Puis nous introduisons une méthodologie de vérification de propriétés globales de haut niveau sur un modèle formellement lié au code source. Plus précisément, nous décrivons l'extraction automatique d'un système de transitions formel, à partir d'annotations vérifiées par le code source. Ce système de transitions peut alors être plongé dans une logique d'ordre supérieur
The work presented in this thesis aims at strengthening the security and safety level of smart card embedded systems, with the use of Formal Methods. On one hand, we present the formal verification of the isolation of the data belonging to different applets loaded on the same card. More precisely, we describe the formal proof, in the Coq proof system, that the run-time access control, performed by the Java Card platform, ensures data confidentiality and integrity. On the other hand, we study the correctness and the safety of low level source code of an embedded operating system. Such source code is illustrated by a case study of a Flash memory management module, using a journalling mechanism and ensuring the memory consistency in the case of a card tear. The verification of functional and local properties has been developed using the Caduceus program verification tool. Since this tool does not support some low level constructions of the C language, such as the unions and the casts, we propose an analysis and some solutions for the formalisation of such constructions. We also propose an extension of Caduceus that allows to specify and verify the behaviour of a function in the case of sudden interruption of its execution. Then, we introduce a methodology for the verification of high level and global properties, which is meant for the expression and proof of this kind of properties on a model formally linked to the source code. More precisely, we describe an automatic extraction of a transition system from the annotations that are verified by the source code. This transition system can then be translated in a high order logic

Avec la croissance majeure de l’Internet des Objets et du Cloud Computing, la sécurité dans ces systèmes est devenue un problème majeur. Plusieurs attaques ont eu lieu dans les dernières années, mettant en avant la nécessité de garanties de sécurité fortes sur ces systèmes. La plupart du temps, une vulnérabilité dans le noyau ou un de ses modules est suffisante pour compromettre l’intégralité du système. Établir et prouver des propriétés de sécurité par le biais d’assistants de preuve semble être un grand pas en avant vers l’apport de garanties de sécurité. Cela repose sur l’utilisation de modèles mathématiques dans le but de raisonner sur leur comportement, et d’assurer que ce dernier reste correct. Cependant, en raison de la base de code importante des logiciels s’exécutant dans ces systèmes, plus particulièrement le noyau, cela n’est pas une tâche aisée. La compréhension du fonctionnement interne de ces noyaux, et l’écriture de la preuve associée à une quelconque propriété de sécurité, est de plus en plus difficile à mesure que le noyau grandit en taille. Dans cette thèse, je propose une nouvelle approche de conception de noyau, le proto-noyau. En réduisant les fonctionnalités offertes par le noyau jusqu’à leur plus minimal ensemble, ce modèle, en plus de réduire au maximum la surface d’attaque, réduit le coût de preuve au maximum. Il permet également à un vaste ensemble de systèmes d’être construits par-dessus, considérant que la minimalité des fonctionnalités comprises dans le noyau oblige les fonctionnalités restantes à être implémentées en espace utilisateur. Je propose également dans cette thèse une implémentation complète de ce noyau, sous la forme du proto-noyau Pip. En ne fournissant que les appels systèmes les plus minimaux et indispensables, l’adaptation du noyau à des usages concrets et la faisabilité de la preuve sont assurées. Afin de réduire le coût de transition modèlevers-binaire, la majorité du noyau est écrite directement en Gallina, le langage de l’assistant de preuve Coq, et est automatiquement convertie en code C compilable pendant la phase de compilation. Pip ne repose alors que sur une fine couche d’abstraction matérielle écrite dans des langages de bas niveau, qui ne fournit que les primitives que le modèle requiert, telles que la configuration du matériel. De plus, étant donné que l’Internet des Objets et le Cloud Computing nécessitent aujourd’hui ces architectures, je propose plusieurs extensions au modèle de Pip afin de supporter le matériel multi-cœur. Soutenus par des implémentations, ces modèles permettent d’apporter le proto-noyau Pip dans les architectures multi-coeur, apportant ainsi des garanties de sécurité fortes dans ces environnement. Enfin, je valide mon approche et son implémentation par le biais d’évaluations de performances et d’une preuve de concept de portage de noyau Linux, démontrant ainsi la flexibilité du proto-noyau Pip dans des environnements réels
Due to the major growth of the Internet of Things and Cloud Computing worlds, security in those systems has become a major issue. Many exploits and attacks happened in the last few years, highlighting the need of strong security guarantees on those systems. Most of the times, a vulnerability in the kernel or one of its modules is enough to compromise the whole system. Etablishing and proving security properties through proof assistants seems to be a huge step towards bringing security guarantees. This relies on using mathematical models in order to reason on their behaviour, and prove the latter remains correct. Still, due to the huge and complex code base of the software running on those systems, especially the kernel, this is a tedious task. Understanding the internals of those kernels, and writing an associated proof on some security property, is more and more difficult as the kernel grows in size. In this thesis, I propose a new approach of kernel design, the proto-kernel. By reducing the features provided by the kernel to their most minimal subset, this model, in addition to lowering the attack surface, reduces the cost of the proof effort. It also allows a wide range of systems to be built on top of it, as the minimality of the features embedded into the kernel causes the remaining features to be built at the userland level. I also provide in this thesis a concrete implementation of this model, the Pip proto-kernel. By providing only the most minimal and mandatory system calls, both the usability of the kernel and the feasibility of the proof are ensured. In order to reduce the model-to-binary transition effort, most of the kernel is written directly in Gallina, the language of the Coq Proof Assistant, and is automatically converted to compilable C code during compilation phase. Pip only relies on a thin hardware abstraction layer written in low-level languages, which provides the operations the model requires, such as modifying the hardware configuration. Moreover, as Internet of Things and Cloud Computing use cases would require, I propose some extensions of Pip’s model, in order to support multicore hardware. Backed up by real implementations, those models bring the Pip proto-kernel to multicore architectures, bringing strong security guarantees in those modern environments. Finally, I validate my approach and its implementation through benchmarks and a Linux kernel port proof-of-concept, displaying the flexibility of the Pip proto-kernel in real world environments

Le déploiement et l'exécution d'applications dans le cloud sont aujourd'hui une réalité. L'existence de celui-ci est intrinsèquement liée à celle de la virtualisation. Ce concept consiste à découper une machine physique en plusieurs sous-machines, dites machines virtuelles, isolées les unes des autres. Plus récemment, les conteneurs se sont posés comme une alternative viable aux machines virtuelles. Les conteneurs sont plus légers que ces dernières et apportent les mêmes garanties d'isolation et de sécurité. Néanmoins, l'isolation, un conteneur ne peut affamer ses congénères, proposée est peut-être trop poussée. En effet, les mécanismes existants permettant l'isolation mémoire ne s'adaptent pas aux changements de charge de travail. Il n'est donc pas possible de consolider la mémoire, c'est-à-dire récupérer la mémoire inutilisée d'un conteneur pour en faire un meilleur usage. Pour répondre à ce problème et garantir, à la fois, l'isolation et la consolidation mémoire, nous proposons MemOpLight. Ce mécanisme s'adapte aux changements de charge de travail grâce à un retour applicatif. Chaque conteneur indique donc s'il a de bonnes performances pour guider la répartition de la mémoire. Celle-ci est récupérée aux conteneurs ayant de bonnes performances pour que les autres conteneurs puissent augmenter celles-ci. L'idée étant de trouver un équilibre mémoire où tous les conteneurs ont des performances satisfaisantes. MemOpLight permet d'augmenter la satisfaction des conteneurs de 13% comparé aux mécanismes existants
Nowadays, deploying and executing applications in the cloud is a reality. The cloud can not exist without virtualization. This concept consists of slicing physical machines into several sub-machines, isolated from one another, known as virtual machines. Recently, containers emerged as a viable alternative to virtual machines. Containers are lighter than virtual machines and bring the same isolation and security guarantees. Nonetheless, the isolation they offer is maybe too important. Indeed, existing mechanisms enforce memory isolation by ensuring that no container starves the others; however, they do not adapt to changes in workload. Thus, it is impossible to consolidate memory, i.e. to reclaim memory unused by some containers to make a better use of it. To answer this problem and ensure both isolation and consolidation, we introduce MemOpLight. This mechanism adapts to workload changes thanks to application feedback. Each container tells the kernel whether it has good or bad performance to guide memory reclaim. Memory is first reclaimed from containers with good performance in the hope that the others can improve their own performance. The idea is to find a balance where all containers have satisfying performance. MemOpLight increases container satisfactions by 13% compared to existing mechanisms

Le cancer du sein est actuellement dans les pays occidentaux le premier cancer chez la femme, en termes d’incidence et de mortalité (taux standardisés de 101,5 et 17.7 pour 100 000 personnes années en 2005 respectivement). De très nombreux facteurs de risque et facteurs pronostiques sont déjà connus et étudiés, plusieurs axes de recherche sont développés sur toutes les étapes de la maladie, mais l’influence des facteurs socio-économiques et géographiques, aux niveaux individuel et environnemental n’avait pas encore été étudiée en France sur le cancer du sein.L’objectif général de ce travail était d’explorer cette influence par différents moyens afin d’en tirer des connaissances et une application pratique dans la prévention du cancer du sein, qu’elle soit primaire, secondaire ou tertiaire.Dans notre première étude nous avons montré que les femmes d’un niveau socio-éducatif faible étaient moins à même d’avoir bénéficié d’au moins une mammographie dans les 6 ans ou d’au moins un suivi gynécologique dans les 3 ans précédant leur diagnostic de cancer du sein. Egalement elles ont un stade de diagnostic plus avancé que les femmes de niveau socio-éducatif plus élevé. Ces variables sont ensuite retrouvées comme facteurs pronostiques péjoratifs de la survie. Dans notre seconde étude nous avons montré que l’accès à un chirurgien spécialisé dans les interventions du cancer du sein, gage d’une meilleure survie, était influencé par le niveau socio-économique du lieu de résidence de la patiente, ainsi que par son éloignement géographique par rapport aux centres de traitement de référence du cancer, où travaillent les chirurgiens spécialisés. Dans notre troisième étude nous avons montré qu’à l’inverse de nombre de cancers, l’incidence du cancer du sein était plus élevée dans les zones socio-économiquement plus favorisées, et ce quelle que soit la classe d’âge de la patiente, phénomène pour lequel nous n’avons pas vraiment d’explication, surtout pour les femmes les plus jeunes. Enfin dans notre quatrième étude actuellement en cours, nous avons pour objectif d’étudier au niveau individuel, conjointement avec le nouvel indice de défavorisation européen adapté à la France, en quoi le degré de richesse économique et sociale et la proximité des services médicaux des patientes atteintes de cancer du sein joue sur le stade de la tumeur, l’accès et les modalités de traitement, et la survie
In developed countries, breast cancer is currently the leading cancer in women in terms of incidence and mortality (standardized rate of 101.5 and 17.7 per 100,000 person-years in 2005, respectively). Many risk factors and prognostic factors have been studied and are well known. Research is under way with regard to every step in the development of breast cancer, but the impact of socio-economic and geographic factors, at the individual and environmental level with regard to the disease have never been studied in France.The general aim of this work was to explore the impact of these factors in different ways to build on our knowledge and to develop practical applications in the primary, secondary or tertiary prevention of breast cancer.In our first study, we showed that women with a low socio-educational level were less likely to have benefited from at least one mammography within the 6 years or at least one gynaecological consultation within the 3 years before the diagnosis of breast cancer. These women also had a more advanced tumour at diagnosis than did women with a higher socio-educational level. These variables also came to light as predictors of a poor prognosis in terms of survival. In our second study, we showed that access to a surgeon specialised in breast cancer surgery, which is associated with better survival, was influenced by the socio-economic level of the patient’s place of residence, as well as the distance between the patient’s home and reference centres for cancer treatment, where the specialised surgeons work. In our third study, we showed that in contrast to many cancers, the incidence of breast cancer was highest in the most socio-economically privileged areas, and this whatever the age of the patient. We have no explanation for this phenomenon, particularly with regard to the youngest age group of women. Finally, the aim of our fourth study, which is currently on-going, is to study at the individual level, using the new European deprivation index adapted to France, to what extent economic wealth and social standing, as well as the proximity of medical services for patients with breast cancer have an impact on tumour stage, access to treatment, treatment techniques and survival

La virtualisation des ressources informatiques a donné naissance au Cloud Computing. Plus récemment, la virtualisation légère à base de conteneur est devenu de plus en plus populaire. En effet, les conteneurs offrent une isolation des performances comparable à celle des machines virtuelles, mais promettent une meilleur consolidation des ressources grâce à leur flexibilité. Dans cette thèse nous mettons en lumière des pertes d'isolation de performance supposé garanti à un conteneur actif. Ces pertes apparaissent pendant la consolidation, c'est-à-dire, lorsque la mémoire inutilisée d'un conteneur inactif est transférée vers un nouveau conteneur qui démarre. Or, dans un environnement non virtualisé, ce scénario de consolidation mémoire n'aboutit pas à une chute de performances chez les processus les plus actifs. Nous proposons donc, dans un premier temps, de mesurer l'activité mémoire des conteneurs à l'aide de métriques présentes dans l'état de l'art. Puis, pour garantir l'isolation des conteneurs les plus actifs lors des consolidations mémoire, nous modifions le comportement du noyau Linux afin de récupérer en priorité la mémoire des conteneurs définis comme étant les plus inactifs par la métrique. Dans un deuxième temps, nous proposons une autre méthode d'estimation de l'activité mémoire des conteneurs qui repose sur une horloge globale d'événements mémoire. Cette méthode est plus réactive que la précédente car elle cherche à protéger les conteneurs dont l'activité mémoire est la plus récente
The virtualization of computing resources has given rise to cloud computing. More recently, container-based lightweight virtualization has become increasingly popular. Containers offer performance isolation comparable to that of virtual machines, but promise better resource consolidation due to their flexibility. In this thesis we highlight performance isolation losses assumed to be guaranteed to an active container. These losses occur during consolidation, i.e. when the unused memory of an inactive container is transferred to a new container that starts. However, in a non-virtualized environment, this memory consolidation scenario does not result in a drop in performance among the most active processes. We therefore propose, as a first step, to measure the memory activity of containers using state-of-the-art metrics. Then, to ensure the isolation of the most active containers during memory consolidations, we modify the behavior of the Linux kernel in order to reclaim the memory of the containers defined as being the most inactive by the metric. In a second step, we propose another method for estimating the memory activity of containers based on a global clock of memory events. This method is more reactive than the previous one because it seeks to protect containers with the most recent memory activity

Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C
Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture

Cette thèse cherche à comprendre comment les mineur.e.s isolé.e.s en situation de migration, arrivé.e.s sans représentant légal sur le territoire français, peuvent bénéficier de la protection de l’enfance. Arrivé.e.s sur la scène de l’évaluation de la minorité et de l’isolement, ces jeunes migrant.e.s sont soumis.e.s à une épreuve de crédibilité narrative, comportementale et physique : ils ou elles doivent dévoiler leurs récits, leurs corps et leurs expressions non verbales en restant à tout prix un « enfant » aux yeux de ceux qui les jugent. Plusieurs questions sont alors posées : comment se construit le jugement de l’âge ? comment se forment les décisions de classement entre les « vrais » et les « faux » mineurs ? comment les acteurs de la protection de l’enfance sont-ils amenés à mobiliser des arguments, critères et justifications qui mènent à des pratiques de « gestion migratoire » ? Pour étudier les pratiques du jugement dans ce contexte d’incertitude qu’est l’évaluation de la minorité et de l’isolement, je propose donc une analyse de la sphère interne institutionnelle. A partir d’une enquête de terrain réalisée entre octobre 2014 et novembre 2016, d’abord dans un lieu d’évaluation de la minorité et de l’isolement géré par l’association France terre d’asile en région parisienne, puis auprès des différents acteurs de la « distribution » de la protection dans différents départements parisiens, et enfin autour de deux campements urbains auto-gérés par des migrant.e.s, cette thèse interroge, en étudiant le « quotidien » de l’institution, la façon dont les mineur.e.s isolé.e.s sont jugé.e.s, étiqueté.e.s et sélectionné.e.s avant d’avoir accès – ou non – à la protection de l’enfance
This research seeks to understand how unaccompanied migrant children, that have arrived on French territory without a legal guardian can access child protective services. Arrived on the stage of the assessment of age and isolation, these young migrants’ narrative, behavioral and physical credibility is tested. Through their narratives, physical and non-verbal expressions, these children must demonstrate to those who judge them that they are a “child”, at all costs. Consequently, several questions can be asked: How can age be judged? How are the decisions of classification between the "true" and "fake" minors taken? How are child protection actors brought to mobilize arguments, criteria and justifications which lead to practices of "migratory management "? To study the practices of judgment in this context of uncertainty, meaning the assessment of age and isolation, this dissertation offers an analysis of the internal workings of institutions. The field investigation was carried out between October 2014 and November 2016, firstly in a centre of evaluation of age and isolation managed by the association France terre d’asile in Paris region, then with the various actors in charge of “distributing" the protection in various Parisian departments, and finally in two urban camps that are self-managed by migrants. Based on this investigation and through the study of everyday life of the institution, this dissertation questions the way unaccompanied children are judged, labelled and selected before having access - or not - to child protection