Noyau de séparation

Un noyau de séparation est un type de noyau de sécurité utilisé pour simuler un environnement distribué. Le concept a été introduit par John Rushby dans un article de 1981. Rushby a proposé le noyau de séparation comme solution aux difficultés et aux problèmes qui sont apparus lors du développement et de la vérification de noyaux de sécurité complexes et volumineux destinés à « fournir un fonctionnement sécurisé à plusieurs niveaux sur des systèmes multi-utilisateurs à usage général ». Selon Rushby, « la tâche d'un noyau de séparation est de créer un environnement qui ne se distingue pas de celui fourni par un système physiquement distribué : il doit apparaître comme si chaque régime était une machine séparée et isolée et que les informations ne pouvaient circuler d'une machine à une autre que par des lignes de communication externes connues. L'une des propriétés que nous devons prouver d'un noyau de séparation est donc qu'il n'existe aucun canal de circulation d'informations entre les régimes autres que ceux explicitement fournis ».

Une variante du noyau de séparation, le noyau de partitionnement, a été acceptée dans la communauté de l'aviation commerciale comme moyen de consolider plusieurs fonctions sur un seul processeur, peut-être de criticité mixte . Les produits de systèmes d'exploitation en temps réel commerciaux de ce genre ont été utilisés par les constructeurs aéronautiques pour des applications avioniques critiques pour la sécurité.

En 2007, la Direction de l'assurance de l'information de l' Agence nationale de sécurité américaine (NSA) a publié le profil de protection du noyau de séparation (SKPP) , une spécification des exigences de sécurité pour les noyaux de séparation adaptés à une utilisation dans les environnements de menaces les plus hostiles. Le SKPP décrit, dans le jargon des critères communs , une classe de produits modernes qui fournissent les propriétés fondamentales du noyau de séparation conceptuel de Rushby. Il définit les exigences fonctionnelles et d'assurance de sécurité pour la construction et l'évaluation des noyaux de séparation tout en offrant une certaine latitude dans les choix disponibles pour les développeurs.

Le SKPP définit le noyau de séparation comme « des mécanismes matériels et/ou micrologiciels et/ou logiciels dont la fonction principale est d'établir, d'isoler et de séparer plusieurs partitions et de contrôler le flux d'informations entre les sujets et les ressources exportées allouées à ces partitions ». De plus, les exigences fonctionnelles de base du noyau de séparation incluent :

• Protection de toutes les ressources (y compris le processeur , la mémoire et les périphériques) contre tout accès non autorisé.
• Séparation des ressources internes utilisées par la Cible des Fonctions de Sécurité d'Evaluation (TSF) des ressources exportées mises à disposition des sujets.
• Partitionnement et isolement des ressources exportées.
• Médiation des flux d'informations entre les partitions et entre les ressources exportées.
• Services d'audit.

Le noyau de séparation alloue toutes les ressources exportées sous son contrôle dans des partitions. Les partitions sont isolées, à l'exception des flux d'informations explicitement autorisés. Les actions d'un sujet dans une partition sont isolées des sujets d'une autre partition (c'est-à-dire qu'elles ne peuvent pas être détectées ou communiquées à ceux-ci), à moins que ce flux n'ait été autorisé. Les partitions et les flux sont définis dans les données de configuration. Notez que « partition » et « sujet » sont des abstractions orthogonales. « Partition », comme l'indique sa genèse mathématique, fournit un regroupement théorique des entités système, tandis que « sujet » nous permet de raisonner sur les entités actives individuelles d'un système. Ainsi, une partition (une collection contenant zéro ou plusieurs éléments) n'est pas un sujet (un élément actif), mais peut contenir zéro ou plusieurs sujets. Le noyau de séparation fournit à ses programmes logiciels hébergés des propriétés de partitionnement et de contrôle des flux d'informations de haute assurance qui sont à la fois inviolables et non contournables. Ces capacités fournissent une base de confiance configurable pour une variété d'architectures système.

• PikeOS combine la technologie d'hyperviseur à noyau séparé avec des capacités en temps réel.
• INTEGRITY-178B de Green Hills Software En septembre 2008, il est devenu le premier noyau de séparation certifié contre le SKPP.
• Wind River Systems dispose d'une technologie de noyau de séparation qui était en cours de certification en 2009.
• Lynx Software Technologies dispose d'un noyau de séparation, LynxSecure .

En 2011, la Direction de l'assurance de l'information a mis fin au SKPP. La NSA ne certifiera plus de systèmes d'exploitation spécifiques, y compris les noyaux de séparation, par rapport au SKPP, notant que « la conformité à ce profil de protection, en soi, n'offre pas suffisamment de confiance dans le fait que les informations de sécurité nationale sont correctement protégées dans le contexte d'un système plus vaste dans lequel le produit conforme est intégré ».

Le micro-noyau seL4 a une preuve formelle de concept selon laquelle il peut être configuré comme un noyau de séparation. La continuité forcée des informations implique également qu'il s'agit d'un exemple de niveau élevé d'assurance. Le noyau de séparation Muen est également un noyau de séparation open source formellement vérifié pour les machines x86.