Secure compilation for memory protection

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