Separationskerne - Separation kernel

En adskillelse kerne er en form for sikkerhed kerne anvendes til at simulere et distribueret miljø. Konceptet blev introduceret af John Rushby i et papir fra 1981. Rushby foreslog separeringskernen som en løsning på de vanskeligheder og problemer, der var opstået i udviklingen og verifikationen af ​​store, komplekse sikkerhedskerner, der havde til formål "at levere sikker drift på flere niveauer på flerbrugersystemer til generelle formål." Ifølge Rushby, "er en adskillelseskerns opgave at skabe et miljø, der ikke kan skelnes fra det, der leveres af et fysisk distribueret system: det skal se ud som om hvert regime er en separat, isoleret maskine, og at information kun kan strømme fra en maskine til en anden langs kendte eksterne kommunikationslinjer. En af de egenskaber, vi skal bevise for en adskillelseskerne, er derfor, at der ikke er andre kanaler for informationsstrøm mellem andre regimer end dem, der udtrykkeligt er givet. "

En variant af adskillelseskernen, partitioneringskernen, har opnået accept i det kommercielle luftfartssamfund som en måde at konsolidere flere funktioner på en enkelt processor, måske af blandet kritik . Kommercielle realtids-operativsystemprodukter i denne genre er blevet brugt af flyproducenter til sikkerhedskritiske avionikapplikationer.

I 2007 offentliggjorde Information Assurance Directorate i US National Security Agency (NSA) Separation Kernel Protection Profile (SKPP), en sikkerhedskravspecifikation for adskillelseskerner, der er egnet til brug i de mest fjendtlige trusselsmiljøer. SKPP beskriver i Common Criteria -sprogbrug en klasse af moderne produkter, der giver grundlæggende egenskaber ved Rushbys konceptuelle adskillelseskerne. Det definerer sikkerhedsfunktionelle og sikkerhedskrav til konstruktion og evaluering af adskillelseskerner, samtidig med at det giver en vis spillerum i de valg, der er tilgængelige for udviklere.

SKPP definerer adskillelseskernen som "hardware og/eller firmware og/eller softwaremekanismer, hvis primære funktion er at etablere, isolere og adskille flere partitioner og kontrollere informationsstrømmen mellem emnerne og eksporterede ressourcer, der er allokeret til disse partitioner." Endvidere omfatter separeringskernens kernefunktionelle krav:

  • Beskyttelse af alle ressourcer (herunder CPU , hukommelse og enheder) mod uautoriseret adgang.
  • Adskillelse af interne ressourcer, der bruges af Target of Evaluation Security Functions (TSF) fra eksporterede ressourcer, der stilles til rådighed for emner.
  • Opdeling og isolering af eksporterede ressourcer.
  • Formidling af informationsstrømme mellem partitioner og mellem eksporterede ressourcer.
  • Revisionstjenester.

Separationskernen allokerer alle eksporterede ressourcer under dens kontrol til partitioner. Partitionerne er isoleret bortset fra eksplicit tilladte informationsstrømme. Et emns handlinger i en partition er isoleret fra (dvs. kan ikke påvises af eller kommunikeres til) emner i en anden partition, medmindre denne strøm er tilladt. Partitionerne og flowene er defineret i konfigurationsdata. Bemærk, at 'partition' og 'subjekt' er ortogonale abstraktioner. 'Partition', som angivet ved dets matematiske genese, giver mulighed for en sætteoretisk gruppering af systemenheder, hvorimod 'subjekt' giver os mulighed for at ræsonnere om de enkelte aktive enheder i et system. En partition (en samling, der indeholder nul eller flere elementer) er således ikke et emne (et aktivt element), men kan indeholde nul eller flere emner. Adskillelseskernen leverer til sine hostede softwareprogrammer høj-partitionerings- og informationsflowkontrolegenskaber, der er både manipuleringssikre og ikke-omgåelige. Disse muligheder giver et konfigurerbart, pålideligt fundament for en række forskellige systemarkitekturer.

Løsninger

I 2011 nedlagde Information Assurance Directorate SKPP. NSA vil ikke længere certificere specifikke operativsystemer, herunder adskillelseskerner mod SKPP, idet det bemærker, at "overensstemmelse med denne beskyttelsesprofil i sig selv ikke giver tilstrækkelig tillid til, at nationale sikkerhedsoplysninger er passende beskyttet i forbindelse med et større system, hvor konformen produktet er integreret ".

Den seL4 mikrokernen har et formelt bevis for konceptet, at det kan konfigureres som en adskillelse kerne. Den håndhævede fortsættelse af information sammen med dette indebærer, at det er et forhøjet niveau af sikkerhed. Muen -adskillelseskernen er også en formelt verificeret open source -adskillelseskerne til x86 -maskiner.

Se også

Referencer