Le but de ce travail est de montrer qu'il est possible de concilier sécurité et flexibilité dans un noyau de système d'exploitation. Nous démontrons qu'il est possible de garantir à la fois la flexibilité et la sécurité d'un système, en séparant la gestion de la politique de sécurité des outils servant à sa mise en oeuvre. Notre travail se découpe en deux partie. Dans la première nous proposons des outils élémentaires de protection ayant pour rôle de protéger le système contre certains types d'attaques choisis tout en restant totalement indépendants de la politique de sécurité mise en oeuvre dans le système. Dans la deuxième partie nous présentons le canevas logiciel sécurisé que nous avons implanté, et notamment le composant chargé de la gestion des politiques de sécurité que nous appelons gestionnaire de sécurité. Nos résultats sont validés sur des exemples mettant en évidence la flexibilité de la protection dans le système.

Java est une technologie attractive pour les équipements embarqués et contraints, de par ses propriétés de sûreté, de portabilité et de faible empreinte mémoire du code. Cependant, la taille imposante d'un environnement Java complet a obligé les producteurs d'équipements embarqués à utiliser des spécifications dégradées de Java aux fonctionnalités limitées, telles que J2ME ou Java Card. Ces spécialisations précoces de Java perdent la compatibilité au niveau applicatif avec l'édition standard, et ne peuvent ainsi s'adresser qu'à des cas d'utilisation particuliers.Notre travail consiste à permettre l'utilisation de l'édition standard de Java sur les systèmes contraints, au travers d'une spécialisation tardive et agressive du système qui intervient après déploiement de ses applications. L'occurrence tardive de la spécialisation permet de mieux déterminer les conditions d'utilisation du système, et donc de le spécialiser « sur mesure » par rapport aux applications qu'il exécute.Nos contributions sont les suivantes : dans un premier temps, nous définissons la notion de « romization », consistant à déployer un système hors-ligne avant de capturer et de transférer son image mémoire vers l'équipement sur lequel il doit s'exécuter. De cette définition, nous proposons une architecture de romization capable de capturer une image mémoire du système à n'importe quel moment de son exécution. Dans un second temps, nous traitons des moyens d'analyse et de spécialisation permettant de rendre cette image mémoire embarquable. L'évaluation effectuée montre que cette spécialisation tardive, appliquée à un environnement Java standard déployé, permet effectivement d'en obtenir une version minimaliste et embarquable sur un équipement contraint.

Autant les applications Android ont réussi à positionner Android parmi les systèmes d'exploitation les plus utilisés, autant elles ont facilité aux créateurs de maliciels de s'introduire et de compromettre ses appareils. Une longue liste de menaces causées par les applications téléchargées vise l'intégrité du système et la vie privée de ses utilisateurs. Malgré l'évolution incessante du système Android pour améliorer son mécanisme de sécurité, le niveau de sophistication des logiciels malveillants a augmenté et s'adapte continuellement avec les nouvelles mesures. L'une des principales faiblesses menaçant la sécurité de ce système est le manque abyssal d'outils et d'environnements permettant la spécification et la vérification formelle des comportements des applications avant que les dommages ne soient causés. À cet égard, les méthodes formelles semblent être le moyen le plus naturel et le plus sûr pour une spécification et une vérification rigoureuses et non ambiguës de telles applications. Notre objectif principal est de développer un cadre formel pour le renforcement de politiques de sécurité dans les applications Android. L'idée est d'établir une synergie entre le paradigme orienté aspect et les méthodes formelles. L'approche consiste à réécrire le programme de l'application en ajoutant des tests de sécurité à certains points soigneusement sélectionnés pour garantir le respect de la politique de sécurité. La version réécrite du programme préserve tous les bons comportements de la version originale qui sont conformes à la politique de sécurité et agit contre les mauvais. / As much as they have positioned Android among the most widely used operating systems, Android applications have helped malware creators to break in and infect its devices. A long list of threats caused by downloaded applications targets the integrity of the system and the privacy of its users. While the Android system is constantly evolving to improve its security mechanism, the malware's sophistication level is skyrocketing and continuously adapting with the new measures. One of the main weaknesses threatening smartphone security is the abysmal lack of tools and environments that allow formal specification and verification of application behaviors before damage is done. In this regard, formal methods seem to be the most natural and secure way for rigorous and unambiguous specification and verification of such applications. Our ultimate goal is to formally enforce security policies on Android applications. The main idea is to establish a synergy between the aspect-oriented paradigm and formal methods such as the program rewriting technique. The approach consists of rewriting the application program by adding security tests at certain carefully selected points to ensure that the security policy is respected. The rewritten version of the program preserves all the good behaviors of the original one that comply with the security policy and acts against the bad ones.

Autant les applications Android ont réussi à positionner Android parmi les systèmes d'exploitation les plus utilisés, autant elles ont facilité aux créateurs de maliciels de s'introduire et de compromettre ses appareils. Une longue liste de menaces causées par les applications téléchargées vise l'intégrité du système et la vie privée de ses utilisateurs. Malgré l'évolution incessante du système Android pour améliorer son mécanisme de sécurité, le niveau de sophistication des logiciels malveillants a augmenté et s'adapte continuellement avec les nouvelles mesures. L'une des principales faiblesses menaçant la sécurité de ce système est le manque abyssal d'outils et d'environnements permettant la spécification et la vérification formelle des comportements des applications avant que les dommages ne soient causés. À cet égard, les méthodes formelles semblent être le moyen le plus naturel et le plus sûr pour une spécification et une vérification rigoureuses et non ambiguës de telles applications. Notre objectif principal est de développer un cadre formel pour le renforcement de politiques de sécurité dans les applications Android. L'idée est d'établir une synergie entre le paradigme orienté aspect et les méthodes formelles. L'approche consiste à réécrire le programme de l'application en ajoutant des tests de sécurité à certains points soigneusement sélectionnés pour garantir le respect de la politique de sécurité. La version réécrite du programme préserve tous les bons comportements de la version originale qui sont conformes à la politique de sécurité et agit contre les mauvais. / As much as they have positioned Android among the most widely used operating systems, Android applications have helped malware creators to break in and infect its devices. A long list of threats caused by downloaded applications targets the integrity of the system and the privacy of its users. While the Android system is constantly evolving to improve its security mechanism, the malware's sophistication level is skyrocketing and continuously adapting with the new measures. One of the main weaknesses threatening smartphone security is the abysmal lack of tools and environments that allow formal specification and verification of application behaviors before damage is done. In this regard, formal methods seem to be the most natural and secure way for rigorous and unambiguous specification and verification of such applications. Our ultimate goal is to formally enforce security policies on Android applications. The main idea is to establish a synergy between the aspect-oriented paradigm and formal methods such as the program rewriting technique. The approach consists of rewriting the application program by adding security tests at certain carefully selected points to ensure that the security policy is respected. The rewritten version of the program preserves all the good behaviors of the original one that comply with the security policy and acts against the bad ones.

.

Les développeurs des systèmes informatiques, y compris critiques, font souvent appel à des systèmes d'exploitation sur étagère. Cependant, un mauvais fonctionnement d'un système d'exploitation peut avoir un fort impact sur la sûreté de fonctionnement du système global, d'où la nécessité de trouver des moyens efficaces pour caractériser sa sûreté de fonctionnement. Dans cette thèse, nous étudions l'étalonnage de la sûreté de fonctionnement des systèmes d'exploitation par rapport aux comportements défectueux de l'application. Nous spécifions les propriétés qu'un étalon de sûreté de fonctionnement doit satisfaire. Après, nous spécifions les mesures et la mise en oeuvre des trois étalons destinés à comparer la sûreté de fonctionnement de différents systèmes d'exploitation. Ensuite, nous développons les prototypes des trois étalons. Ces prototypes servent à comparer les différents systèmes d'exploitation des familles Windows et Linux, et pour montrer la satisfaction des propriétés identifiées.

L'étude des réseaux a jusqu'à maintenant été abordée par l'aspect télécommunication en repoussant à plus long terme les points de vue système et externe. L'aspect externe concerne l'utilisateur qui se voit confronté à une multitude de systèmes d'exploitation différents. Or, très peu d'utilisateurs peuvent prétendre connaitre parfaitement deux ou plusieurs systèmes; ce que l'on pensait être un avantage des réseaux généraux devient donc un inconvénient. Avec leur développement croissant et notamment l'entrée dans l'ère de la télématique, il semble que le moment soit venu de chercher à faciliter l'utilisation de l'outil informatique dans le cadre d'une informatique répartie.

Alors que la recherche sur la qualité du code des systèmes a connu un formidable engouement, les systèmes d'exploitation sont encore aux prises avec des problèmes de fiabilité notamment dus aux bogues de programmation au niveau des services noyaux tels que les pilotes de périphériques et l'implémentation des systèmes de fichiers. Des études ont en effet montré que chaque version du noyau Linux contient entre 600 et 700 fautes, et que la propension des pilotes de périphériques à contenir des erreurs est jusqu'à sept fois plus élevée que toute autre partie du noyau. Ces chiffres suggèrent que le code des services noyau n'est pas suffisamment testé et que de nombreux défauts passent inaperçus ou sont difficiles à réparer par des programmeurs non-experts, ces derniers formant pourtant la majorité des développeurs de services. Cette thèse propose une nouvelle approche pour le débogage et le test des services noyau. Notre approche est focalisée sur l'interaction entre les services noyau et le noyau central en abordant la question des "trous de sûreté" dans le code de définition des fonctions de l'API du noyau. Dans le contexte du noyau Linux, nous avons mis en place une approche automatique, dénommée Diagnosys, qui repose sur l'analyse statique du code du noyau afin d'identifier, classer et exposer les différents trous de sûreté de l'API qui pourraient donner lieu à des fautes d'exécution lorsque les fonctions sont utilisées dans du code de service écrit par des développeurs ayant une connaissance limitée des subtilités du noyau. Pour illustrer notre approche, nous avons implémenté Diagnosys pour la version 2.6.32 du noyau Linux. Nous avons montré ses avantages à soutenir les développeurs dans leurs activités de tests et de débogage.

L'extraordinaire évolution de la micro-informatique au cours de ces dernières années, et son utilisation de plus en plus fréquente dans les domaines les plus variés, sont à l'origine du développement des postes de travail autonomes scientifiques. Point de rencontre entre l'ordinateur se miniaturisant et le terminal devenant intelligent, le poste de travail a amene, avec l'introduction de la notion d'environnement de programmation, une véritable révolution dans la méthodologie de développement et d'utilisation de l'informatique. A l'heure actuelle, on observe principalement deux courants en ce qui concerne le développement des environnements de programmation La première orientation, que nous qualifierons de "classique", consiste à adapter aux pistes de travail autonomes des systèmes développés à l'origine pour des ordinateurs traditionnels, que ce soient des minis ou des gros ordinateurs, et reposant sur les mêmes principes fondamentaux. Le meilleur représentant de cette catégorie est le système UNIX. Le prix de revient, assez faible, d'un poste autonome et les progrès constants en logiciel de base qui ont permis la définition de noyaux de systèmes d'exploitation relativement peu volumineux, constituent les deux raisons essentielles de l'évolution des environnements "classiques" vers les postes de travail autonomes. Dans la deuxième catégorie sont regroupés les environnements orientés vers l'intelligence artificielle. Les chercheurs de ce vaste domaine de l'informatique ont été amenés à passer assez rapidement à un autre "style" de programmation, à une autre manière de concevoir et de réaliser leurs applications, ceci essentiellement à cause d'une incompatibilité entre leur mode de pensée et le "mode de pensée" des systèmes classiques. Aussi, et pour des raisons de performances, ils ont commencé à réaliser en totalité, dès le début des années 1970, leurs systèmes spécifiques. De cette façon, un certain nombre de notions ont pris beaucoup d'importance~ comme la programmation interactive, les programmes adaptatifs et l'accès agréable aux différentes ressources du système (systèmes Interlisp, Zetalisp).

Cette thèse présente le système d'exploitation MutekH, capable de s'exécuter nativement sur une plateforme matérielle multiprocesseur, où les processeurs peuvent être de complexité différente et disposer de spécificités ou de jeux d'instructions différents. Les travaux présentés ici s'insèrent dans un contexte où les systèmes multi-core et les processeurs spécialisés permettent tous deux de réduire la consommation énergétique et d'optimiser les performances dans les systèmes embarqués et dans les systèmes sur puce. Les autres solutions logicielles existantes permettant l'exécution d'applications sur des plateformes multiprocesseurs hétérogènes ne permettent pas, à ce jour, la communication par mémoire partagée, telle qu'on l'envisage habituellement pour les systèmes multiprocesseurs homogènes. Cette solution est la seule qui permet la réutilisation du code source d'applications parallèles existantes pour leur exécution directe par des processeurs différents. La solution proposée est mise en oeuvre en deux phases: grâce au développement d'un noyau dont l'abstraction rend transparente l'hétérogénéité des processeurs, puis à la réalisation d'un outil spécifique d'édition des liens, capable d'harmoniser le code et les données des fichiers exécutables chargés en mémoire partagée. Les résultats obtenus montrent que MutekH permet l'exécution d'applications préexistantes utilisant des services standards, tels que les Threads POSIX, sur des plateformes multiprocesseurs hétérogènes sans dégradation des performances par rapport aux autres systèmes d'exploitation opérant sur des plateformes multiprocesseurs classiques.