Separační jádro - Separation kernel

Separace jádra je druh zabezpečení jádra slouží k simulaci distribuované prostředí. Tento koncept představil John Rushby v dokumentu z roku 1981. Rushby navrhl separační jádro jako řešení obtíží a problémů, které vyvstaly při vývoji a ověřování velkých, komplexních bezpečnostních jader, která měla „poskytovat víceúrovňovou bezpečnou operaci na univerzálních víceuživatelských systémech“. Podle Rushbyho „úkolem separačního jádra je vytvořit prostředí, které je k nerozeznání od prostředí poskytovaného fyzicky distribuovaným systémem: musí to vypadat, jako by každý režim byl samostatný izolovaný stroj a aby informace mohly proudit pouze z jednoho stroje. k dalšímu podél známých vnějších komunikačních linek. Jednou z vlastností, kterou musíme u separačního jádra prokázat, je, že mezi režimy neexistují žádné jiné kanály pro tok informací než ty, které jsou výslovně uvedeny. "

Varianta separačního jádra, dělícího jádra, získala v komerční letecké komunitě přijetí jako způsob konsolidace více funkcí do jednoho procesoru, snad smíšené kritičnosti . Komerční produkty operačních systémů v reálném čase v tomto žánru používali výrobci letadel pro aplikace letecké avioniky kritické z hlediska bezpečnosti.

V roce 2007 vydalo ředitelství Information Assurance Americké národní bezpečnostní agentury (NSA) profil Separation Kernel Protection Profile (SKPP), což je specifikace bezpečnostních požadavků pro separační jádra vhodná k použití v prostředí nejnepřátelštějších hrozeb. SKPP v jazyce Common Criteria popisuje třídu moderních produktů, které poskytují základní vlastnosti Rushbyho koncepčního separačního jádra. Definuje požadavky na funkční zabezpečení a zabezpečení pro konstrukci a vyhodnocování separačních jader a přitom poskytuje určitou volnost ve volbách, které mají vývojáři k dispozici.

SKPP definuje separační jádro jako „hardwarové a/nebo firmware a/nebo softwarové mechanismy, jejichž primární funkcí je vytvořit, izolovat a oddělit více oddílů a řídit tok informací mezi subjekty a exportovanými prostředky přidělenými těmto oddílům“. Mezi základní funkční požadavky separačního jádra dále patří:

  • Ochrana všech prostředků (včetně CPU , paměti a zařízení) před neoprávněným přístupem.
  • Oddělení interních zdrojů používaných nástrojem Target of Evaluation Security Functions (TSF) od exportovaných zdrojů zpřístupněných subjektům.
  • Rozdělení a izolace exportovaných zdrojů.
  • Zprostředkování toků informací mezi oddíly a mezi exportovanými prostředky.
  • Auditorské služby.

Separační jádro alokuje všechny exportované prostředky pod svou kontrolou do oddílů. Oddíly jsou izolované s výjimkou výslovně povolených toků informací. Akce subjektu v jednom oddílu jsou izolovány od (tj. Nemohou být detekovány nebo sděleny subjektům) subjektů v jiném oddílu, pokud tento tok nebyl povolen. Oddíly a toky jsou definovány v konfiguračních datech. Všimněte si, že 'oddíl' a 'předmět' jsou ortogonální abstrakce. „Oddíl“, jak naznačuje jeho matematická geneze, poskytuje set-teoretické seskupení systémových entit, zatímco „subjekt“ nám umožňuje uvažovat o jednotlivých aktivních entitách systému. Oddíl (kolekce obsahující nula nebo více prvků) tedy není subjektem (aktivním prvkem), ale může obsahovat nula nebo více subjektů. Oddělovací jádro poskytuje svým hostovaným softwarovým programům vysoce kvalitní dělení a vlastnosti řízení toku informací, které jsou odolné proti neoprávněné manipulaci a nelze je obejít. Tyto funkce poskytují konfigurovatelný důvěryhodný základ pro řadu systémových architektur.

Řešení

V roce 2011 ředitelství pro zajišťování informací ukončilo SKPP. NSA již nebude certifikovat konkrétní operační systémy, včetně separačních jader proti SKPP, přičemž konstatuje, že „shoda s tímto ochranným profilem sama o sobě nenabízí dostatečnou jistotu, že informace o národní bezpečnosti jsou vhodně chráněny v kontextu většího systému, v němž produkt je integrován “.

SeL4 microkernel má formální důkaz o koncept, který může být nakonfigurován jako separační jádra. Vynucené pokračování informací spolu s tím znamená, že jde o příklad jistoty na vyšší úrovni. Separační jádro Muen je také formálně ověřeným separačním jádrem s otevřeným zdrojovým kódem pro počítače x86.

Viz také

Reference