Trennkern - Separation kernel

Eine Separation Kernel ist eine Art von Sicherheits Kernel verwendet , um eine verteilte Umgebung zu simulieren. Das Konzept wurde von John Rushby in einem Papier von 1981 eingeführt. Rushby schlug den Separation Kernel als Lösung für die Schwierigkeiten und Probleme vor, die bei der Entwicklung und Verifikation großer, komplexer Sicherheitskerne aufgetreten waren, die "einen mehrstufigen sicheren Betrieb auf universellen Mehrbenutzersystemen bereitstellen" sollten. Laut Rushby besteht die Aufgabe eines Separation-Kernels darin, eine Umgebung zu schaffen, die sich nicht von der eines physisch verteilten Systems unterscheidet: Es muss so aussehen, als ob jedes Regime eine separate, isolierte Maschine ist und dass Informationen nur von einer Maschine fließen können zu einem anderen entlang bekannter externer Kommunikationswege. Eine der Eigenschaften, die wir eines Separation-Kernels beweisen müssen, ist daher, dass es keine anderen Kanäle für den Informationsfluss zwischen Regimen gibt, als die explizit vorgesehenen."

Eine Variante des Separation-Kernels, der Partitioning-Kernel, hat sich in der kommerziellen Luftfahrtgemeinschaft durchgesetzt, um auf einem einzigen Prozessor mehrere Funktionen zu konsolidieren, möglicherweise von unterschiedlicher Kritikalität . Kommerzielle Echtzeit-Betriebssystemprodukte dieses Genres wurden von Flugzeugherstellern für sicherheitskritische Avionikanwendungen verwendet.

2007 veröffentlichte das Information Assurance Directorate der US-amerikanischen National Security Agency (NSA) das Separation Kernel Protection Profile (SKPP), eine Spezifikation der Sicherheitsanforderungen für Separation-Kernel, die für den Einsatz in den feindlichsten Bedrohungsumgebungen geeignet sind. Das SKPP beschreibt im Common Criteria- Sprachgebrauch eine Klasse moderner Produkte, die die grundlegenden Eigenschaften von Rushbys konzeptionellem Separation Kernel bereitstellen. Es definiert die Sicherheitsfunktions- und Sicherheitsanforderungen für die Konstruktion und Bewertung von Separation-Kernels und bietet gleichzeitig einen gewissen Spielraum bei den Auswahlmöglichkeiten, die den Entwicklern zur Verfügung stehen.

Der SKPP definiert den Trennungskernel als "Hardware- und/oder Firmware- und/oder Softwaremechanismen, deren Hauptfunktion darin besteht, mehrere Partitionen einzurichten, zu isolieren und zu trennen und den Informationsfluss zwischen den Subjekten und den diesen Partitionen zugewiesenen exportierten Ressourcen zu steuern". Darüber hinaus umfassen die Kernfunktionsanforderungen des Separation Kernels:

  • Schutz aller Ressourcen (einschließlich CPU , Speicher und Geräte) vor unbefugtem Zugriff.
  • Trennung der internen Ressourcen, die vom Target of Evaluation Security Functions (TSF) verwendet werden, von den exportierten Ressourcen, die den Probanden zur Verfügung gestellt werden.
  • Partitionierung und Isolierung exportierter Ressourcen.
  • Vermittlung von Informationsflüssen zwischen Partitionen und zwischen exportierten Ressourcen.
  • Prüfungsleistungen.

Der Separation-Kernel ordnet alle exportierten Ressourcen unter seiner Kontrolle in Partitionen zu. Die Partitionen sind isoliert, mit Ausnahme von explizit erlaubten Informationsflüssen. Die Aktionen eines Subjekts in einer Partition sind von Subjekten in einer anderen Partition isoliert (d. h. können nicht von Subjekten in einer anderen Partition erkannt oder an sie kommuniziert werden), es sei denn, dieser Fluss wurde zugelassen. Die Partitionen und Flüsse werden in den Konfigurationsdaten definiert. Beachten Sie, dass 'Partition' und 'Subjekt' orthogonale Abstraktionen sind. 'Partition' ermöglicht, wie durch seine mathematische Genese angedeutet, eine mengentheoretische Gruppierung von Systementitäten, während 'Subjekt' uns erlaubt, über die einzelnen aktiven Entitäten eines Systems nachzudenken. Somit ist eine Partition (eine Sammlung, die null oder mehr Elemente enthält) kein Subjekt (ein aktives Element), kann aber null oder mehr Subjekte enthalten. Der Separation Kernel bietet seinen gehosteten Softwareprogrammen hochsichere Partitionierungs- und Informationsflusskontrolleigenschaften, die sowohl manipulationssicher als auch nicht umgangen werden können. Diese Funktionen bieten eine konfigurierbare vertrauenswürdige Grundlage für eine Vielzahl von Systemarchitekturen.

Lösungen

Im Jahr 2011 hat die Direktion für Informationssicherung das SKPP eingestellt. Die NSA wird bestimmte Betriebssysteme, einschließlich Separation-Kernels, nicht mehr gegen das SKPP zertifizieren Produkt integriert ist".

Der seL4-Mikrokernel verfügt über einen formalen Machbarkeitsnachweis, dass er als Separation-Kernel konfiguriert werden kann. Die erzwungene Fortführung von Informationen impliziert, dass dies ein Beispiel für Sicherheit auf hohem Niveau ist. Der Muen-Trennkernel ist auch ein offiziell verifizierter Open-Source-Trennkernel für x86-Maschinen.

Siehe auch

Verweise