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.

Le nombre croissant de logiciels malveillants Android s’accompagne d’une préoccupation profonde liée aux problèmes de la sécurité des terminaux mobiles. Les enjeux deviennent sans conteste de plus en plus importants, suscitant ainsi beaucoup d’attention de la part de la communauté des chercheurs. En outre, la prolifération des logiciels malveillants va de pair avec la sophistication et la complexité de ces derniers. En effet, les logiciels malveillants plus élaborés, tels que les maliciels polymorphes et métamorphiques, utilisent des techniques d’obscurcissement du code pour créer de nouvelles variantes qui préservent la sémantique du code original tout en modifiant sa syntaxe, échappant ainsi aux méthodes de détection usuelles. L’ambition de notre recherche est la proposition d’une approche utilisant les méthodes formelles et l’apprentissage automatique pour la détection des maliciels sur la plateforme Android. L’approche adoptée combine l’analyse statique et l’apprentissage automatique. En effet, à partir des applications Android en format APK, nous visons l’extraction d’un modèle décrivant de manière non ambiguë le comportement de ces dernières. Le langage de spécification formelle choisi est LNT. En se basant sur le modèle généré, les comportements malicieux exprimés en logique temporelle sont vérifiés à l’aide d’un vérificateur de modèle. Ces propriétés temporelles sont utilisées comme caractéristiques par un algorithme d’apprentissage automatique pour classifier les applications Android. / The ever-increasing number of Android malware is accompanied by a deep concern about security issues in the mobile ecosystem. Unquestionably, Android malware detection has received much attention in the research community and therefore it becomes a crucial aspect of software security. Actually, malware proliferation goes hand in hand with the sophistication and complexity of malware. To illustrate, more elaborated malware like polymorphic and metamorphic malware, make use of code obfuscation techniques to build new variants that preserve the semantics of the original code but modify it’s syntax and thus escape the usual detection methods. In the present work, we propose a model-checking based approach that combines static analysis and machine learning. Mainly, from a given Android application we extract an abstract model expressed in terms of LNT, a process algebra language. Afterwards, security related Android behaviours specified by temporal logic formulas are checked against this model, the satisfaction of a specific formula is considered as a feature, finally machine learning algorithms are used to classify the application as malicious or not.

.

.

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. / Despite the existence of an overwhelming amount of research on the quality of system software, Operating Systems are still plagued with reliability issues mainly caused by defects in kernel-level services such as device drivers and file systems. Studies have indeed shown that each release of the Linux kernel contains between 600 and 700 faults, and that the propensity of device drivers to contain errors is up to seven times higher than any other part of the kernel. These numbers suggest that kernel-level service code is not sufficiently tested and that many faults remain unnoticed or are hard to fix bynon-expert programmers who account for the majority of service developers. This thesis proposes a new approach to the debugging and testing of kernel-level services focused on the interaction between the services and the core kernel. The approach tackles the issue of safety holes in the implementation of kernel API functions. For Linux, we have instantiated the Diagnosys automated approach which relies on static analysis of kernel code to identify, categorize and expose the different safety holes of API functions which can turn into runtime faults when the functions are used in service code by developers with limited knowledge on the intricacies of kernel code. To illustrate our approach, we have implemented Diagnosys for Linux 2.6.32 and shown its benefits in supporting developers in their testing and debugging tasks.

Nous présentons ici l'architecture d'un noyau de système d'exploitation pour machines parallèles. Nous discutons les paradigmes de base pour le support d'applications parallèles au niveau d'un noyau de système. Les aspects lies aux modèles de processus et de communication sont développés. Notre démarche s'appuie d'une part sur l'étude des modèles de programmation parallèles sous-jacents aux langages, d'autre part sur les architectures de machines parallèles modernes. Cette approche sur deux fronts convergents nous permet de prendre en compte a la fois les progrès dans l'expression et l'utilisation du parallélisme, et les tendances et les possibilités technologiques de construction de machines parallèles. Le résultat principal de cette étude est la conception d'une architecture de système d'exploitation parallèle original, Parx, et la réalisation d'un noyau de communication pour ce système. Les systèmes d'exploitation ne peuvent plus prétendre offrir une gamme de services dont puissent se satisfaire toutes les applications. Ils doivent supporter un nombre croissant d'applications de types différents, et décomposent leurs fonctionnalités en un noyau qualifie de micro, léger etc., et un ensemble de serveurs de haut niveau, s'occupant de gérer des fichiers, de la mémoire etc. C'est l'approche que nous adoptons ici

La question traitée dans cette thèse a été celle de la fiabilité des résultats d'Analyse de Cycle de Vie (ACV) appliquée aux productions agricoles. La production porcine a été prise comme cas d'étude. Construite autour du fil conducteur de l'incertitude des résultats d'ACV, cette thèse a eu pour objet de rechercher et hiérarchiser les sources d'incertitude de ces résultats, afin de contribuer à leur réduction. Cette réduction de l'incertitude peut être atteinte par une meilleure prise en compte de la variabilité des systèmes à la fois anthropiques et environnementaux. A cette fin, des références ont été produites sur la performance environnementale et son incertitude (à l'aide de scénarios favorable et défavorable) pour trois modes de production de porc contrastés répondant respectivement aux cahiers des charges de la production conventionnelle raisonnée, du label rouge fermier d'Argoat et de l'agriculture biologique. L'influence de la qualité des pratiques de fertilisation a également été analysée en évaluant un quatrième scénario de production conventionnel sur-fertilisé. Pour ces scénarios moyens types, une distinction claire a été obtenue pour chaque indicateur, grâce à l'usage de références sur les émissions spécifiques des postes clé de ces systèmes. Le scénario label rouge est notamment apparu comme une alternative intéressante au scénario conventionnel. Pour chaque scénario des points faibles ont été mis en évidence, ainsi que d'importantes marges d'amélioration. L'incertitude liée aux modèles d'évaluation des impacts a été étudiée en analysant dans un premier temps les concepts sous-jacents et modèles employés en ACV pour les catégories d'impact affectant les écosystèmes (eutrophisation, effet de serre, toxicité, acidification). Dans un second temps, une analyse des sources de variabilité principales pour la catégorie eutrophisation aquatique, impact prépondérant pour les systèmes de production agricoles, a permis de proposer un cadre d'amélioration pour son évaluation. La mise en oeuvre de ces propositions pour l'étape du devenir du nitrate dans les bassins versants a confirmé l'existence d'une importante marge d'amélioration pour évaluer l'eutrophisation aquatique. Elle a également permis de montrer la sensibilité du résultat du changement climatique à l'usage de ces facteurs de devenir du nitrate et l'importance du transfert potentiel de pollution depuis le compartiment eau (nitrate) vers le compartiment air (N20) par le processus de dénitrification dans les zones humides. A l'échelle courante de mise en oeuvre de l'ACV, c'est à dire pour des systèmes de production moyens à une grande échelle (région, pays), la hiérarchisation finale des sources d'incertitude a permis d'identifier comme source principale d'incertitude, celle liée aux modèles d'évaluation des impacts. Pour produire une ACV comparative pertinente d'exploitations réelles, la connaissance et la modélisation des émissions directes sur le site d'exploitation, tenant compte des pratiques de l'agriculteur et du milieu, devraient être profondément améliorées.

Dans cette thèse, nous nous intéressons aux techniques et outils qui permettent de concevoir et d'opti- miser les applications parallèles et réparties sur les réseaux et grappes de stations de travail. Le premier problème abordé est celui de la répartition dynamique de charge en environnement fortement hétérogène : pour répartir dynamiquement et efficacement la charge d'une application répartie, il faut (i) être en mesure d'évaluer et de comparer la disponibilité des différentes machines du réseau et (ii) savoir mettre ces informations en correspondance avec les besoins en ressources des tâches de l'application. Pour cela, nous proposons une méthodologie de modélisation empirique du comportement des éléments d'un réseau de stations de travail face à la charge. Cette méthodologie nous permet de construire des indica- teurs de charge multi-dimensions et multi-critères. Pour mettre cette méthodologie en pratique, nous avons conçu LoadBuilder, une plate-forme répartie d'expérimentation. Le deuxième problème abordé est celui de l'accès à des mécanismes et protocoles de communication multipoints fiables et ordonnés, à partir d'un système d'exploitation UNIX. Pour répondre à ce besoin des applications réparties, nous proposons une solution originale, le sys- tème de fichiers virtuel MPCFS. Ce système de fichiers permet la création de groupes de communication dynamiques et la réalisation de communications multipoints dans ces groupes, au travers de simples manipulations de fichiers et répertoires. Nous avons développé un prototype de ce système, qui peut être chargé dynamiquement dans le noyau du système Linux 2.0.

Le développement d'applications informatiques passe souvent par l'utilisation de langages évolués pour la programmation et de systèmes d'exploitation pour la gestion de l'exécution. Une famille de langages de programmation (les LPC pour "langages à parallélisme Compilé") peuvent procurer les même fonctionnalités et avantages qu'un langage de programmation couplé à un système d'exploitation multi-tâches. Notre intention est de montrer que les LPC ont certains attraits supplémentaires surtout dans le domaine d'application qu'est l'informatique industrielle. Pour mettre ceci en évidence, nous avons développé plusieurs versions d'une même application en utilisant d'une part un LPC et, d'autre part, un langage évolué classique avec un système d'exploitation. Ensuite, nous avons fait une comparaison chiffrée des différentes versions.

La consommation énergétique est devenue un problème majeur dans la conception des systèmes aussi bien d'un point de vue de la fiabilité des circuits que de l'autonomie d'un équipement embarqué. Cette thèse vise à caractériser et modéliser le coût énergétique du système d'exploitation (OS) embarqué en vue d'explorer des solutions faibles consommation. La première contribution consiste à définir une approche globale de modélisation de la consommation des services de base de l'OS: la stimulation de l'exécution de ces services, tels que le changement de contexte, l'ordonnancement et la communication interprocessus, est effectuée à travers des programmes de test adéquats. Sur la base de mesures de la consommation d'énergie sur la carte OMAP35x EVM, des paramètres pertinents soit matériels soit logiciels ont été identifiés pour en déduire des modèles de consommation. Dans une seconde étape, la prise en compte de ces paramètres doit intervenir au plus haut niveau de la conception. L'objectif sera d'exploiter les fonctionnalités offertes par un langage de modélisation et d'analyse architecturale AADL tout en modélisant les aspects logiciel et matériel en vue d'estimer la consommation d'énergie. Ensuite, les modèles énergétiques de l'OS ont été intégrés dans un simulateur multiprocesseur de politique d'ordonnancement STORM afin d'identifier la consommation de l'OS et ceci pour des politiques d'ordonnancement mettant en œuvre des techniques de réduction de la consommation tel que le DVFS et le DPM. Enfin, la définition et vérification de certaines contraintes temps-réel et énergétiques ont été effectuées avec des langages de spécification de contraintes (QAML, RDAL).