Université de Rennes 1 Suivi de flux d'information correct pour les systèmes d'exploitation Linux Correct information flow tracking for Linux operating systems Systèmes d'exploitation LinuxContrôle de flux d'informationAnalyse statique LinuxLinux Security ModulesInformation flow controlStatic analysis Linux (système d'exploitation des ordinateurs) Thèses et écrits académiques Logiciels -- Vérification Thèses et écrits académiques 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. Electronic Thesis or DissertationText fr application/pdf1 : 2393 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/94791c3d-36b3-45e0-b40e-ae6816a39aee Georget Laurent 1992-01-04 FR 221427821 georgetlaurent@laposte.net 2017REN1S040 http://www.theses.fr/2017REN1S040 2017-09-28 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiViêt Triêm TôngValérieintervenant_1075956667JaumeMathieuintervenant_2177111712 MATISSEecoleDoctorale_1 139007164 Universite Bretagne LoirepartenaireRecherche_1 191639044 IRISA partenaireRecherche_2 026386909 ddc:004 Viêt Triêm TôngValérieJaumeMathieuUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATISSEÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) IRISA ASCII PDF 2450174