Conteneurs d’information du noyau Linux

Modèles de politiques et de traçage de flux

Comme expliqué plus haut, appliquer une politique de contrôle des flux d’information plus générale que celles permises par le contrôle d’accès nécessite de maintenir un historique des flux passés dans le système. Cependant, cet historique n’a pas besoin d’être un détail complet de tous les flux individuels ayant eu lieu. Il sut de savoir, pour chaque conteneur d’information, quelles sont les classes de sécurité ayant participé à au moins un flux à destination de ce conteneur. Cela permet de savoir quelles sortes d’informations sont susceptibles de fuiter lors d’un flux depuis ce conteneur. Il s’agit donc d’abstraire le flux.

Propagation de teinte

La manière de loin de la plus répandue de maintenir cette connaissance est la propagation de teinte, ou taint tracking en anglais. Cette approche consiste à attacher à chaque conteneur d’information un label, une méta-donnée indiquant quelles classes de sécurité ont influencé le contenu courant du conteneur. Ce label est propagé en même temps que les données lorsqu’un flux a lieu d’un conteneur à un autre, et le label du conteneur destination est mis à jour pour repéter le fait que son contenu a été modié par la source. Le terme de propagation de teinte vient de ce mécanisme. Tout se passe comme si les conteneurs étaient marqués d’un coup de peinture et que les conteneurs en participant à des flux d’information se « tachaient ». À tout instant de la vie du système, la couleur des tâches d’un conteneur permet de savoir qui l’a touché.
Ce concept de marquage remonte au moins aux travaux séminaux de Fenton [29]. En réalité, Fenton a exposé l’idée de la propagation tout en l’écartant dans son premier modèle. Les marques associées aux conteneurs, les registres d’un modèle abstrait de machine dans son cas, sont statiques. Les mérites de la propagation ont donc été redécouverts plus tard, notamment par McIlroy et Reeds [56] comme détaillé en section 2.3.
Le concept de propagation de teinte est très générique et a été adapté pour de nombreux usages. On peut citer notamment le langage Perl qui possède un mécanisme permettant de marquer les données provenant de sources non sûres (les entrées de l’utilisateur, essentiellement) et d’empêcher qu’elles ne soient évaluées comme du code, ou comme une requête de base de données [70, 80].

Implémentations de contrôle de flux d’information dans les systèmes d’exploitation par propagation de teinte

Dans cette section, nous nous intéressons plus particulièrement aux implémentations de contrôle de flux d’information par propagation de teinte à l’échelle des systèmes d’exploitation. Cette catégorie comprend à la fois des systèmes d’exploitation entiers [56], des noyaux de systèmes d’exploitation [100, 109], des composants de sécurité pour ces noyaux [17, 33, 51, 67, 76], des moniteurs implémentés comme des programmes surveillant les flux depuis l’extérieur du noyau de tout ou partie des processus [28, 51] ou encore des Application Programming Interfaces (API)
∗ permettant le développement d’applications distribuées contrôlant les flux entre les processus de ces applications [10]. Le seul critère retenu est que les conteneurs d’information considérés sont de la granularité du système d’exploitation (processus, chiers, InterProcess Communication (IPC)
∗ divers, etc.) et que les flux sont caractérisés par des appels des processus au système d’exploitation.
Il faut noter qu’il n’y a pas vraiment de barrières étanches entre les différents niveaux d’application (matériel, langage, système, etc.) du contrôle de flux. En eet, les travaux de Denning [20, 21] et de Myers et Liskov [64, 66] présentent des modèles très généraux qui sont ensuite appliqués au cas particulier des langages de programmation mais les modèles de systèmes d’exploitation détaillés plus bas y font référence néanmoins [51, 100, 109]. Les distinctions que nous avons introduites entre les expressions « contrôle de flux d’information », « contrôle d’accès obligatoire » et « propagation de teinte » ne sont pas non plus présentes dans tous les articles et travaux. Nous rappelons donc ici que la différence fondamentale qui est intéressante dans la présente thèse est le fait que le contrôle de flux d’information nécessite de maintenir un état sur les flux passés s’étant produits dans le système. Dans le cas où cet état prend la forme d’un label attaché aux objets (y compris les processus du système) et évoluant au fur et à mesure que des flux se produisent, nous considèrons qu’il s’agit de propagation de teinte.

Implémentations de systèmes d’exploitation sur mesure

Les premiers prototypes de systèmes d’exploitation centrés autour du contrôle de flux d’information ont été construits sur mesure dans ce but précis, an de démontrer l’implémentabilité et les avantages de ce type de solution. Ils réutilisent des portions de systèmes pré-existants, réécrits en profondeur pour intégrer le mécanisme de propagation de teintes. Le premier système d’exploitation à avoir implémenté le contrôle de flux d’information, à notre connaissance, est IX par McIlroy et Reeds en 1992 [56]. Ce système est une variante du système d’exploitation UNIX supportant une politique de sécurité forte, à plusieurs niveaux, dans la tradition des préconisations de l’Orange Book du DoD [53]. McIlroy et Reeds décrivent leur système comme appliquant du contrôle d’accès obligatoire. En réalité, d’après nos définitions données plus tôt il s’agit bien de contrôle de flux d’information. En eet, plusieurs éléments distinguent clairement IX du modèle de Bell–LaPadula ou même du high water mark. En premier lieu, IX abandonne la dualité sujet–objet et ne considère plus que des conteneurs d’information impliqués dans des flux (ou dans leurs propres termes « places between which data occasionally flows »). Deuxièmement, les auteurs font le constat que contrairement au contrôle d’accès où seules les ouvertures de fichiers ont besoin d’être contrôlées, le contrôle de flux requiert d’appliquer la politique à chaque opération de lecture et écriture car les labels peuvent être modiés à chaque flux.
McIlroy et Reeds expliquent également les problèmes liés au fait que le contrôle de flux crée lui-même des canaux cachés de communication. L’exemple donné par les auteurs est celui d’un processus avec un niveau d’autorisation bas voulant obtenir des données d’un processus collaborant, mais de niveau bien supérieur. Une méthode simple à mettre en œuvre et relativement able est pour le processus haut d’écrire ou non dans un certain chier de niveau de sensibilité bas initialement. S’il écrit, cela augmente automatiquement le niveau de sensibilité du chier. Le processus bas peut facilement observer le niveau du chier en tentant de le lire : si la lecture échoue, c’est que le niveau de sensibilité était haut. De la sorte, le processus haut peut donc communiquer un bit d’information au processus bas. L’opération peut être « industrialisée » en la répétant à intervalles réguliers (et en remplaçant le chier pour le ramener au niveau bas) an de transmettre n’importe quelle donnée, un bit à la fois. Enn, l’article évoque aussi le problème de l’explosion de teintes, qui est le nom donné au phénomène faisant que dans un système appliquant du contrôle de flux d’information, au l du temps, les conteneurs tendent à acquérir des labels de plus en plus restrictifs, et que les possibilités de flux d’information deviennent donc de plus en plus restreintes. Le problème est similaire a celui d’un programme qui allouerait toujours plus de mémoire sans jamais la libérer. Cela met en danger la disponibilité du système, qui est un objectif de sécurité.

Asbestos

Asbestos est un autre exemple de nouveau système d’exploitation conçu en vue de la protection des données et de l’isolation des services. Ses créateurs, VanDeBogart et al., prêchent pour l’exploration de nouvelles possibilités dans le contexte non restreint d’un nouveau système d’exploitation [100]. Une des idées nouvelles constituant une avancée majeure est la décentralisation des politiques de ux d’information. En effet, Asbestos propose non seulement une politique globale permettant de donner des garanties classiques comme celles du DoD mais aussi la possibilité pour chaque application de dénir sa politique d’isolation et de protection de ses données vis-à-vis des autres processus du système. Enn, Asbestos propose, pour la première fois à notre connaissance, un moyen de lutter contre l’explosion de teintes par un mécanisme connu dans le contexte des bases de données sous le nom de poly-instanciation [55].
On se reférera avec prot à l’article « Solutions to the Polyinstanciation Problem » [43] pour une présentation détaillée de ce mécanisme dans son contexte original. La polyinstanciation consiste à séparer les états ou sessions qu’un serveur maintient avec diérents clients. D’ordinaire, le seul but est celui de l’isolation, an de garantir la condentialité des données de chaque processus vis-à-vis des autres. Dans un système à propagation de teintes, ce mécanisme prévient également la contamination par les teintes qui empêcherait le serveur de s’adresser à plus d’un client. L’alternative pourrait évidemment être le lancement dynamique d’un serveur diérent pour chaque arrivée d’un nouveau client mais cela aurait un coût important en termes de ressources.
La poly-instanciation, si elle est supportée par le système d’exploitation qui garantit une isolation correcte entre les diérentes sessions d’un même processus, fournit unesolution à la fois plus légère, plus flexible et plus robuste.
Les labels d’Asbestos sont organisés autour de la notion de tags, qui sont des identiants associés à certaines classes de contenus. Les tags sont alloués par les utilisateurs du système et administrés chacun par son allocateur. Les labels sont simplement dénis comme un ensemble de tags, provenant de diérents utilisateurs. Lorsqu’un flux d’information survient d’un conteneur vers un autre, les tags de la source sont ajoutés dans ceux de la destination. L’allocation d’un tag confère automatiquement le privilège d’ajouter ce tag au label de n’importe quel conteneur possédé par l’utilisateur et de le retirer du label de n’importe quel conteneur du système (naturellement, si un utilisateur quelconque avait le droit de marquer n’importe quel conteneur avec son tag, il pourrait empêcher son propriétaire légitime d’y accéder). Ce modèle confère donc à chaque utilisateur le droit de dénir une politique sur ses propres données, tout en étant contraint par les politiques dénies par les autres utilisateurs quant aux tags qui ne lui appartiennent pas. Le système est l’arbitre garant de la bonne application des politiques. Asbestos est donc une implémentation de DIFC dans un système d’exploitation [65].
Les « nouvelles primitives » qu’Asbestos promet se résument à un élément central : le passage de message. Les messages sont considérés comme des objets à part entière du système et obéissent donc aux règles présentées plus haut. Pour empêcher que ces règles ne créent des canaux cachés, Asbestos rend ces interfaces non ables. Si l’envoi d’un message échoue à cause de permissions insusantes et que le révéler exposerait de l’information sur les labels du destinataire, alors l’erreur n’est pas signalée à l’émetteur.
Ceci cause bien sûr des problèmes car il est malaisé pour un développeur d’applications de ne pouvoir compter que sur des canaux non ables, y compris localement — il est plus habituel de considérer uniquement les communications de machine à machine non fiables. Pour comprendre quel canal caché est évité par ce mécanisme, on peut considérer deux processus, un processus H pouvant lire du contenu marqué du tag t mais n’ayant pas la possibilité de le déclassier et un processus L ne pouvant pas le lire.
Supposons que le processus L souhaite lire un chier marqué t, avec la complicité du processus H. H peut allouer un nouveau tag t0 puis créer un port de communication qu’il marque ou non d’intégrité haute avec son nouveau tag. Ensuite, L tente d’envoyer un message à ce port. Si le port n’a pas été marqué avec t 0 , le message de L pourra arriver, en revanche si le port a été marqué, comme L ne possède pas le niveau d’intégrité susante, L n’a pas le droit d’envoyer ce message. Si l’erreur est rapportée à L, selon que l’envoi échoue ou non, L sait si H a tagué ou non son port, ce qui permet à H d’envoyer passivement un bit d’information à L sans communiquer directement avec lui. H peut ainsi envoyer à L le chier que ce dernier n’a pas le droit de lire, bitpar bit.

HiStar

HiStar est un système d’exploitation inspiré directement d’Asbestos mais mettant l’accent sur des inventions diérentes [109]. HiStar réutilise les tags d’Asbestos mais requiert que tous les ux soient explicitement demandés. C’est-à-dire que contrairement à Asbestos qui utilise un modèle de label ottants, où ce sont les flux d’information qui causent automatiquement un changement des labels des processus concernés, HiStar utilise un modèle d’élévation explicite des labels. Le processus désireux d’être la destination d’un certain flux d’information doit auparavant élever son label à un niveau susant pour dominer le label de la source de ce flux. Ce parti-pris ferme un canal caché. Tout comme Asbestos, HiStar applique un contrôle de flux d’information décentralisé, le processus qui crée un tag étant libre de l’ajouter et de l’enlever de tous les objets lui appartenant. Grâce à ce mécanisme, HiStar peut se passer de superutilisateur. Toutefois, étant donné que le modèle de labels est très abstrait et général, l’administration d’un tel système est compliquée. HiStar donne plusieurs exemples de politiques à appliquer à des logiciels particuliers mais la composition des politiques appliquées à diérents composants au sein d’un même système n’est pas discutée. Il semble difficile en particulier de démontrer la cohérence d’une politique de sécurité, surtout si l’on considère le dé de sa maintenance dans le temps.
Un autre point de ressemblance avec Asbestos est le fait qu’HiStar dénit de nouvelles primitives de communications, certaines présentant des ressemblances avec celles de certains systèmes UNIX mais demeurant uniques dans leur fonctionnement.
En premier lieu, HiStar généralise le concept de répertoire des systèmes traditionnels en celui de conteneur. Un conteneur est donc une sorte d’annuaire référençant l’existence d’autres objets, pouvant eux-mêmes être des conteneurs. Les conteneurs portent un label et cela permet donc de cacher l’existence de certains objets à des processus nonautorisés. Les processus autorisés peuvent, eux, consulter le conteneur pour connaître les labels des objets qui y sont référencés et savoir à quel point ils doivent élever leur label pour y accéder. Les segments et espaces d’adressage sont aussi des objets géréspar HiStar. Tout processus possède un certain espace d’adressage qui représente sa mémoire virtuelle, composée d’un ensemble de segments, chacun avec un label. Cesystème permet à un thread d’écrire dans la mémoire d’un autre de manière sûre.
Cependant, il n’est pas clair que ce mécanisme ne puisse pas être contourné. En eet, si un processus possède deux segments en lecture–écriture, si l’un des deux a un label de condentialité plus fort que l’autre, le processus peut tout de même écrire du premier dans le deuxième sans faire d’appel système (les lectures ou écritures dans la mémoire se font entièrement en espace utilisateur, dès lors que les segments sont chargés en mémoire), et donc sans qu’HiStar ne puisse voir cette déclassication illégale. Ce point n’est pas discuté dans l’article « Making Information Flow Explicit in HiStar » [109]. Enn, HiStar dénit les portes qui sont des fonctions appelables dans un espace d’adressage par un thread même s’il ne possède pas cet espace d’adressage, pourvu qu’il en ait connaissance via un conteneur. Lorsqu’un processus passe une porte — ce qui revient à eectuer un appel de fonction appartenant à un autre processus — il peut déléguer certains de ses labels à celle-ci jusqu’au retour de la fonction. Ce mécanisme permet par exemple d’implémenter une déclassication contrôlée.

Le système des Linux Security Modules

Le framework Linux Security Modules (LSM) [105] est comme son nom l’indique une interface pour implémenter des modules de sécurité en sus du mécanisme de contrôle d’accès discrétionnaire existant par défaut pour le noyau Linux. Il a été introduit en 2001. Il se présente sous deux aspects. D’une part, des attributs supplémentaires ont été ajoutés aux structures de données du noyau dont l’accès doit être restreint. Ces attributs ne sont pas utilisés par le code standard du noyau et les modules de sécurité sont donc libres de les utiliser pour stocker leur état, et dans le cas des mécanismes de propagation de teintes, les labels des conteneurs d’information correspondant aux structures. D’autre part, des fonctions particulières ont été ajoutées et elles sont appelées à des endroits stratégiques du code du noyau, avant des opérations caractérisées comme sensibles du point de vue de la sécurité par les mainteneurs du noyau. Ces opérations peuvent être par exemple la lecture d’un chier ou l’envoi d’une donnée sur le réseau. Ces fonctions particulières, appelées crochets (hooks en anglais) dans la terminologie LSM peuvent être redénies par un module de sécurité pour appliquer des contrôles supplémentaires et éventuellement retourner un code d’erreur pour empêcher la réalisation de l’opération sensible. Nous détaillons plus avant la conception de LSM dans le chapitre 5.
Le framework LSM ne constitue donc pas stricto sensu une interface pour l’interception des appels système car en réalité les crochets sont implémentés profondément dans les appels système. Il y a plusieurs avantages clairs à cela : d’une part, cela permet de factoriser des crochets dans les appels systèmes qui manipulent les mêmes structures de données internes du noyau, et d’autre part, cela permet aux modules de sécurité de proter du prétraitement des arguments de l’appel système par le noyau.
Par exemple, les adresses mémoires ou descripteurs de chiers invalides sont détectés avant l’interposition, ce qui facilite le travail des développeurs du module. La conception intelligente de LSM permet également de couvrir une partie des risques exposés dans la section 2.4.1 : il n’y pas de risques de conditions de concurrence concernant les arguments des appels système, et comme les LSM font partie de la conception des appels, les valeurs d’erreur qu’ils peuvent retourner sont documentées, ce qui évite toute mauvaise surprise. Les modules bénécient de toutes les interfaces de programmation du noyau, et peuvent donc consulter l’état du noyau, ce qui peut permettre de limiter le problème de désynchronisation. Le problème de protection partielle des ressources est déporté quant à lui des modules au framework LSM. En eet, ce sont les seuls points où le mécanisme de sécurité peut non seulement agir (c’est-à-dire prévenir une opération incorrecte) mais aussi plus simplement observer l’état du système.
On conçoit donc que la position des crochets dans le code est critique pour assurer de bonnes garanties de sécurité. Si un crochet manque avant une opération sensible, alors le mécanisme de sécurité sera impuissant à la détecter, et a fortiori l’empêcher.
À l’inverse, trop de crochets nuiraient aux performances du noyau et rendraient très complexe et dicile la maintenance des mécanismes de sécurité. La bonne position des crochets LSM peut être vériée de plusieurs manières : par du test, des analyses statiques, dynamiques, du model-checking, etc. Dans la section suivante, nous détaillons l’état de l’art concernant l’analyse du code du noyau, pour donner le cadre général dans lequel s’inscrivent les approches spéciquement dédiées à l’analyse de la position des crochets LSM.

ANALYSE DU CODE DU NOYAU LINUX 

Outils dédiés à l’analyse

Dans cette section, nous décrivons les outils qui ont déjà été utilisés pour la vérication du noyau Linux, et en particulier les outils intégrés dans la chaîne de compilation et de tests du noyau. Pour un état de l’art plus complet de toute la théorie et les outils relatifs aux analyses statiques ou dynamiques de code tel que le noyau Linux, on consultera avec prot la thèse de doctorat de Slabý [83].

Approches statiques

De nombreux types d’outils ont été utilisés pour la vérication du noyau Linux. La méthode la plus basique et la plus rapide pour trouver des erreurs consiste à chercher des motifs dans le code connus pour être symptomatiques de certaines classes de problèmes. Par exemple, cela peut permettre de détecter l’oubli d’une désallocation de mémoire dans une fonction ou la comparaison directe entre un pointeur et un entier. À l’origine, ces recherches de motifs étaient faites par de simples expressions régulières mais naturellement, la grammaire du langage C n’étant pas régulière, cette méthode n’est ni correcte, ni sûre : il n’y a aucune garantie de trouver tous les problèmes, ni de ne trouver que des problèmes dans la sortie de l’outil. C’est pour répondre à ce problème qu’a été développé Coccinelle [69]. Coccinelle est un moteur de patchs sémantiques, c’est-à-dire qu’au lieu de travailler sur de simples expressions régulières, il comprend la grammaire du C et peut s’appuyer sur quelques connaissances de la sémantique du langage tels que la commutativité de l’addition et la multiplication, les conversions de type, etc. Cela lui permet de reconnaître des motifs et d’appliquer des transformations complexes. Coccinelle est intégré dans les sources du noyau Linux depuis 2010 [97, commit 74425eee71eb44c9f370bd922f72282b69bb0eab]. Linus Torvalds, créateur et mainteneur-en-chef de Linux, a également développé un analyseur sémantique pour le C appelé Sparse [7, 98]. L’objectif initial de Sparse n’est pas de constituer un compilateur mais uniquement un analyseur capable d’extraire des caractéristiques du code étudié, voire d’en proposer des visualisations (sous forme de graphes de ot de contrôle, typiquement). Certaines vérications statiques sont également facilitées par cet outil. Par exemple, en annotant les fonctions avec l’information des verrous qu’elles prennent et qu’elles libèrent, il est possible de véri-er qu’en tout point d’une fonction, le nombre de verrous occupés ne dépend pas du chemin suivi pour arriver à ce point (ce qui pourrait être le signe que le long de certains chemins d’exécution, tous les verrous pris ne sont pas libérés comme il faut) [96]. MECA [107] et CQUAL [30] ont été utilisés pour vérier la bonne utilisation des pointeurs venant de l’espace utilisateur dans le noyau [47, 107]. En eet, pour des raisons de sécurité, il est critique que le noyau soit parfaitement isolé des processus utilisateurs.
Par conséquent, il faut prendre garde, dans le noyau, de ne pas déréférencer de pointeur fourni par les processus utilisateur (par exemple, en tant qu’argument d’appel système) sans vérier qu’il pointe eectivement vers de la mémoire à laquelle le processus a légitimement accès. Des fonctions particulières, copy_from_user, copy_to_user, etc. sont disponibles pour déréférencer correctement ces pointeurs. Les travaux de Yang et al. [107] d’une part et Johnson et Wagner [47] d’autre part visent à garantir qu’aucun pointeur de l’espace utilisateur n’est déréférencé autrement que par ces fonctions. MECA s’appuie sur de la propagation de teintes : les pointeurs provenant des processus sont automatiquement marqués comme teintés à l’entrée des appels systèmes et seules les fonctions citées plus haut peuvent retirer la teinte. Déréférencer un pointeur teinté est signalé comme une erreur. L’approche CQUAL, pour sa part,s’appuie sur la théorie des types. Chaque type pointeur est rané en deux catégories : le type pointeur utilisateur et le type pointeur noyau. Les conversions ne sont autorisées que par les fonctions données plus haut. La principale diérence entre ces deux approches est que celle de CQUAL est correcte : toutes les manipulations
potentiellement mauvaises de pointeurs sont détectées, au prix de nombreux faux positifs (c’est-à dire de signalements d’erreurs qui n’en sont pas). À l’inverse, MECA ne prétend pas à la correction, il est possible de le tromper avec du code un peu compliqué et donc des erreurs peuvent lui échapper, mais il rapporte beaucoup moins de faux positifs.

Table des matières

1 Introduction 
2 État de l’art 
2.1 Contrôle d’accès et contrôle de flux d’information
2.2 Modèles de politiques et de traçage de flux
2.2.1 Plusieurs niveaux d’application du traçage
2.2.2 Contrôle de flux d’information décentralisé
2.3 Implémentations de contrôle de flux d’information dans les systèmes d’exploitation par propagation de teinte
2.3.1 Implémentations de systèmes d’exploitation sur mesure
2.3.2 Implémentations dans le cadre de systèmes d’exploitation préexistants
2.3.3 Implémentations dans le noyau Linux
2.3.4 Autres usages du traçage de flux d’information
2.3.5 Conclusion sur les implémentations de contrôle de flux d’information dans les systèmes d’exploitation
2.4 Interposition dans les appels système
2.4.1 Risques inhérents à l’interposition de contrôles de sécurité dans les appels système
2.4.2 Le système des Linux Security Modules
2.5 Analyse du code du noyau Linux
2.5.1 Analyses statiques
2.5.2 Analyses dynamiques
2.5.3 Outils dédiés à l’analyse
2.5.4 Application au problème du positionnement des crochets LSM
2.6 Conclusion
3 Conteneurs d’information du noyau Linux 
3.1 Généralités
3.2 Correspondances entre abstractions du système d’exploitation et structures de données internes du noyau
3.2.1 Système de fichiers virtuel
3.2.2 Structures de données relatives aux processus
3.2.3 Structures de données relatives à la mémoire
3.2.4 Structures correspondant aux canaux de communication entre processus
3.3 Conclusion
4 Analyse du noyau Linux assistée par GCC 
4.1 Utilisation du compilateur pour produire des modèles du code du noyau Linux
4.1.1 Particularités du code du noyau Linux
4.1.2 Utilité du compilateur pour construire des modèles
4.2 Extraction et visualisation de graphes de flot de contrôle avec Kayrebt
4.2.1 Kayrebt::Extractor : un greffon d’extraction de graphes de flot de contrôle pour GCC
4.2.2 Kayrebt::Viewer : une interface de visualisation des graphes produits par Extractor
4.2.3 Kayrebt::Callgraphs : un greffon pour produire des graphes d’appel
4.3 Conclusion
5 Vérification du placement des crochets LSM pour le contrôle de flux d’information 
5.1 LSM et les moniteurs de flux d’information
5.1.1 Appels systèmes provoquant des flux d’information
5.1.2 LSM pour le contrôle de flux d’information
5.2 Décider du bon positionnement des crochets
5.2.1 Conception d’un appel système
5.2.2 Problèmes spécifiques au contrôle de flux d’information
5.3 Analyse statique vérifiant la bonne position des crochets
5.3.1 Position des crochets LSM et des instructions causant les flux
5.3.2 Graphes de flot de contrôle
5.3.3 Propriété de médiation complète
5.4 Formalisation
5.4.1 Syntaxe des graphes
5.4.2 Configurations et exécutions abstraites et concrètes
5.4.3 Sémantiques abstraite et concrète
5.4.4 Conclure qu’un chemin est impossible
5.4.5 Gestion des boucles
5.5 Implémentation
5.6 Résultats
5.6.1 mq_timedsend et mq_timedreceive
5.6.2 tee, splice et vmsplice
5.6.3 process_vm_readv, process_vm_writev, ptrace
5.7 Conclusion
6 Rfblare : une implémentation de Blare à même de gérer la concurrence entre appels système et les projections en mémoire 
6.1 Attaques sur des moniteurs de flux d’information implémentés avec LSM
6.1.1 Exploitation d’une condition de concurrence entre read et write
6.1.2 Exploitation de flux d’information continus
6.2 Algorithme de propagation de teinte
6.2.1 Tags, flux et exécutions
6.2.2 Interprétation des exécutions en termes de flux d’information
6.2.3 Propagation idéale
6.2.4 Propagation de teintes effectuée par les moniteurs implémentés avec LSM
6.2.5 Plus petite surapproximation correcte des teintes à propager
6.3 Implémentation et expérimentations
6.4 Conception
6.5 Tests
6.6 Conclusion
7 Conclusion 
A Liste des crochets LSM dans la version 4.7 du noyau
A.1 Crochets présents dans le noyau ociel
A.2 Crochets ajoutés pour Rfblare
B Définition de la sémantique abstraite pour notre analyse statique et preuve de correction
C Description formelle de la propagation de teintes de Rfblare et preuve de correction
Bibliographie 
Liste des publications de l’auteur 
Table des figures 
Liste des tableaux 
Liste des extraits de code
Glossaire 

Lire le rapport complet