L4 (mikrokerne)

L4  er en anden generations mikrokerne udviklet af Jochen Liedtke i 1993 [1] .

L4-mikrokernearkitekturen viste sig at være vellykket. Mange implementeringer af L4 mikrokerne ABI og API er blevet oprettet. Alle implementeringer blev kendt som L4-familien af ​​mikrokerner. Liedtkes implementering har uformelt fået navnet "L4/x86" [2] .

Historie

L1

I 1977 forsvarede Jochen Liedtke sit diplomprojekt i matematik ved universitetet i Bielefeld (Tyskland). Som en del af projektet skrev Liedtke en compiler til ELAN -sproget ( eng. ). ELAN-sproget blev skabt i 1974 på basis af sproget Algol 68 til undervisning i programmering [3] . Liedtke kaldte sit værk "L1": bogstavet "L" er det første bogstav i forfatterens efternavn ( L iedtke ); tallet "1" er værkets serienummer.

L2

I 1977 blev Liedtke færdig som matematiker, blev på universitetet i Bielefeld og gik i gang med at skabe et runtime-miljø for ELAN-sproget.

8-bit mikrocontrollere blev bredt tilgængelige. Der krævedes et styresystem, der kunne køre på små arbejdsstationer i gymnasier og universiteter. CP/M passede ikke. Det tyske nationale forskningscenter for datalogi og teknologi GMD og universitetet i Bielefeld besluttede at udvikle et nyt styresystem fra bunden [4] .

I 1979 begyndte Jochen Liedtke at udvikle et nyt styresystem og kaldte det " Eumel " ( engelsk ) fra engelsk.  Udvidbar flerbruger mikroprocessor EL AN - system . _ Operativsystemet "Eumel" blev også kaldt "L2", hvilket betyder " Liedtkes 2. værk " . Det nye OS understøttede 8-bit Zilog Z80-processorer , var multi-user og multitasking var bygget på en mikrokerne og ortogonal persistens Understøttelse af ortogonal persistens var som følger: OS gemte med jævne mellemrum sin tilstand på disk (indholdet af hukommelsen , processorregistre osv.); efter strømafbrydelser blev operativsystemet gendannet fra en gemt tilstand; programmer fortsatte med at arbejde, som om fejlen ikke var opstået; kun ændringer foretaget siden sidste lagring gik tabt. Eumel OS var inspireret af Multics OS og delte mange ligheder med Accent og Mach 4kernerne

Eumel OS blev senere overført til Zilog Z8000 , Motorola 68000 og Intel 8086 processorer . Disse processorer var 8-bit og 16-bit, indeholdt ikke en MMU og understøttede ikke en hukommelsesbeskyttelsesmekanisme . Eumel OS emulerede en virtuel maskine med 32-bit adressering og en MMU [4] . På trods af brugen af ​​emulering kunne op til fem terminaler forbindes til én arbejdsstation, der kører Eumel OS [4] .

I starten var det kun muligt at skrive programmer til Eumel OS på ELAN-sproget. Kompilere til CDLPascal Basic og DYNAMO blev tilføjet senere men de blev ikke brugt meget 4

Siden 1980 begyndte brugen af ​​Eumel OS, først til undervisning i programmering og tekstbehandling, og derefter til kommercielle formål. Så i midten af ​​1980'erne kørte Eumel OS allerede på mere end 2000 computere i advokatfirmaer og andre firmaer [4] .

L3

Med fremkomsten af ​​processorer, der understøtter virtuel hukommelse (på grund af MMU) og mekanismer til dens beskyttelse, er behovet for at efterligne en virtuel maskine forsvundet.

I 1984 [5] gik Jochen Liedtke på arbejde på GMD forskningscenter for at skabe et OS svarende til Eumels, men uden emulering. GMD er i øjeblikket en del af Fraunhofer Society .

Siden 1987 [4] er Jochen Liedtke og hans team på SET Institute , en del af GMD, begyndt at udvikle en ny mikrokerne, kaldet "L3" ("L3" fra " L iedtkes 3. værk ").

Jochen Liedtke ville se, om det var muligt at opnå høj ydeevne af IPC -komponenten ved at vælge den rigtige arkitektur til kernen og bruge hardwareplatformens funktioner i implementeringen . Implementeringen af ​​IPC-mekanismen viste sig at være vellykket (sammenlignet med den komplekse implementering af IPC i Mach-mikrokernen). Senere blev en mekanisme implementeret til at isolere hukommelsesområder for processer, der kører i brugerrummet .

I 1988 blev udviklingen afsluttet, og operativsystemet af samme navn blev frigivet. L3-mikrokernen blev skrevet i assemblersprog , brugte funktionerne fra Intel x86 -arkitekturprocessorerne , understøttede ikke andre platforme og overgik Mach-mikrokernen i ydeevne. L3 OS var kompatibelt med Eumel OS: programmer oprettet til Eumel OS kørte under L3 OS, men ikke omvendt [4] .

L3 mikrokerne komponenter:

• IPC-komponent (implementeret en mekanisme til synkron messaging );
• en komponent, der giver arbejde med hukommelsessider og fungerer i brugerrummet [6] ;
• en komponent, der implementerer en sikkerhedsmekanisme, kaldet den engelske.  sikre domæner ("opgaver", "klaner" og "chefer").

Siden 1989 [4] har OS været brugt:

• i skoler (erstattede sin forgænger - OS Eumel) [4] ;
• af TÜV SÜD (Tyskland) ;
• på cirka 3.000 computere installeret i advokatfirmaer i Tyskland [5] .

L4

Mens han arbejdede på L3-mikrokernen, opdagede Jochen Liedtke fejl i Mach-mikrokernen. Liedtke ønskede at forbedre ydeevnen og begyndte at kode den nye mikrokerne i assemblersprog ved hjælp af funktionerne i Intel i386 -processorarkitekturen . Den nye mikrokerne hed "L4" (fra " L iedtkes 4. værk ").

I 1993 blev implementeringen af ​​L4 mikrokernen afsluttet. IPC-komponenten viste sig at være 20 gange hurtigere end IPC'en fra Mach-mikrokernen [1] .

OS bygget på første generations mikrokerner (især på Mach mikrokernen) var karakteriseret ved lav ydeevne. På grund af dette begyndte udviklere i midten af ​​1990'erne at genoverveje begrebet mikronuklear arkitektur. Især den dårlige ydeevne af Mach-mikrokernen blev forklaret ved at flytte den komponent, der er ansvarlig for IPC, til brugerrummet.

Nogle komponenter i Mach-mikrokernen blev returneret tilbage - inde i mikrokernen . Dette krænkede selve ideen om mikrokerner (minimumsstørrelse, isolering af komponenter), men tillod at øge operativsystemets ydeevne.

Forskerne søgte efter årsagerne til Mach-mikrokernens dårlige ydeevne og analyserede omhyggeligt de komponenter, der er vigtige for god ydeevne. Analysen viste, at kernen allokerede et for stort arbejdssæt (meget hukommelse) til processerne, hvilket resulterede i , at der konstant opstod cache - misser , når kernen fik adgang til hukommelsen [ 6 ] . Analysen gjorde det muligt at formulere en ny regel for mikrokerneudviklere - mikrokernen bør designes således, at de komponenter, der er vigtige for at sikre høj ydeevne, placeres i processorens cache (helst det første niveau ( engelsk niveau 1 , L1) og det er ønskeligt at der stadig er lidt plads tilbage i cachen ).   

På grund af stigningen i IPC-komponentens ydeevne var eksisterende operativsystemer ikke i stand til at håndtere den øgede tilstrømning af IPC-meddelelser. Adskillige universiteter (f.eks. Technical University Dresden , University of New South Wales ), institutioner og organisationer (f.eks. IBM ) er begyndt at skabe implementeringer af L4 og bygge nye operativsystemer omkring dem.

I 1996 forsvarede Liedtke sin ph.d.- afhandling [7] ved det tekniske universitet i Berlin om emnet "beskyttede sidetabeller" [8] .

Siden 1996, ved Research Center, har og hans kolleger fortsat forskning i L4-mikrokernen, mikrokerner generelt og Sawmill OS -operativsystemet i særdeleshed [9] . På grund af den manglende kommercielle succes, " IBM Workspace OS "-operativsystemet, bygget på den tredje version af Mach-mikrokernen fra CMU og udviklet af IBM fra januar 1991 til 1996 [10] , i stedet for konceptet " L4 mikrokerne" brugte konceptet "Lava Nucleus" eller "LN" for kort.

Med tiden blev L4-mikrokernekoden frigivet fra at være bundet til platformen, sikkerheds- og isolationsmekanismerne blev forbedret.

I 1999 begyndte Liedtke at arbejde som professor i operativsystemer ved Karlsruhe Institute of Technology (Tyskland) [7] .

Mikrokerne L4Ka::Hasselnød

I 1999 blev Jochen Liedtke optaget i Systems Architecture Group (SAG), der arbejder ved Karlsruhe Institute of Technology (Tyskland), og fortsatte forskning i mikronukleare operativsystemer. SAG-gruppen er også kendt som "L4Ka"-gruppen.

For at bevise, at en mikrokerne kunne implementeres i et sprog på højt niveau , udviklede SAG -gruppen "L4Ka::Hazelnut" mikrokernen. Arbejdet blev udført på Karlsruhe Institute of Technology med støtte fra DFG [11] . Implementeringen blev skrevet i C++ og understøttede IA-32- og ARM-arkitekturprocessorer . Ydeevnen af ​​den nye mikrokerne viste sig at være acceptabel, og udviklingen af ​​assembly-sprog kerner blev afbrudt.

Microkernel L4/Fiasco

I 1998 begyndte Dresden Technical University Operating Systems Group at udvikle sin egen implementering af L4-mikrokernen, kaldet "L4/Fiasco". Udviklingen blev udført i C++ parallelt med udviklingen af ​​L4Ka::Hazelnut mikrokernen.

På det tidspunkt understøttede L4Ka::Hazelnut-mikrokernen ikke kerne-rum-samtidighed, og "L4Ka::Pistachio"-mikrokernen understøttede kun kernel-space- afbrydelser ved specifikke præemptionspunkter. Udviklerne af "L4/Fiasco" mikrokernen har implementeret fuld forebyggende multitasking (med undtagelse af nogle atomoperationer). Dette gjorde kernearkitekturen mere kompleks, men reducerede interrupt latenser, hvilket er vigtigt for et real-time operativsystem.

Mikrokernen "L4/Fiasco" blev brugt i OS "DROPS" [12]  - OS af "hård" realtid (når det er ekstremt vigtigt, at hændelsen reageres på i strenge tidsrammer), også udviklet på Technical University of Dresden.

På grund af kompleksiteten af ​​mikrokerne-arkitekturen i senere versioner af Fiasco OS, vendte udviklere tilbage til den traditionelle tilgang - at starte kernen med afbrydelser slået fra (med undtagelse af nogle få præemptionspunkter).

Platformuafhængighed

Microkernel L4Ka::Pistachio

Implementeringer af L4 mikrokernen, skabt før udgivelsen af ​​L4Ka::Pistachio mikrokernen og senere versioner af "Fiasco" mikrokernen, brugte funktionerne i computerarkitekturen (de var "bundet" til processorarkitekturen). En arkitekturuafhængig API blev udviklet. På trods af tilføjelsen af ​​portabilitet leverede API'en høj ydeevne. De ideer, der ligger til grund for mikrokernearkitekturen, har ikke ændret sig.

I begyndelsen af ​​2001 blev en ny L4 API udgivet, meget forskellig fra den tidligere versions L4 API, givet versionsnummer 4 ("version 4", også kendt som "version X.2"), og anderledes:

• bedre understøttelse af multiprocessorsystemer ;
• "løsere bånd" mellem tråde og adresserum;
• tilføjelse af UTCB'er (trådkontrolblokke på brugerniveau ) til tråde, der kører i brugerrummet ; 
• tilføjelse af virtuelle registre .

Efter udgivelsen af ​​den nye version af API'et begyndte SAG-teamet at skabe en ny mikrokerne, kaldet "L4Ka::Pistachio" [13] [14] . Koden blev kompileret fra bunden i C++ ved hjælp af erfaringerne fra L4Ka::Hazelnut-projektet. Der blev lagt vægt på høj ydeevne og bærbarhed.

Den 10. juni 2001 døde læge Jochen Liedtke [7] i en bilulykke. Herefter faldt udviklingshastigheden af ​​projektet markant.

I 2003 [15] blev arbejdet afsluttet takket være indsatsen fra Liedtkes elever: Volkmar Uhlig, Uwe Dannowski og Espen Skoglund. Kildekoden er blevet frigivet under BSD-licensen med 2 klausuler .

Nye versioner af Fiasco

Sideløbende fortsatte udviklingen af ​​L4/Fiasco-mikrokernen. Understøttelse af flere hardwareplatforme ( x86 , AMD64 , ARM ) er blevet tilføjet. Især kunne en version af Fiasco kaldet "FiascoUX" køre i brugerrum, der kører Linux OS .

Udviklerne af L4/Fiasco mikrokernen har implementeret flere udvidelser til L4v2 API.

• IPC - undtagelsen tillod kernen at overlade håndtering af processorundtagelser til brugerpladsen.
• Tilføjelsen af ​​Alien-tråd (en tråd udført af én processorkerne på vegne af en proces, der kører på en anden processorkerne) gav mulighed for finkornet kontrol af systemopkald .
• Tilføjelse af UTCB (samme som i L4 API version X.2).

Derudover leverede "Fiasco"-mikrokernen mekanismer til administration af kommunikationsrettigheder. De samme mekanismer eksisterede til at styre de ressourcer, der forbruges af kernen.

"L4Env" blev udviklet, et sæt komponenter, der kører oven på "Fiasco" mikrokernen i brugerrummet. "L4Env" blev brugt i "L4Linux", en implementering af paravirtualisering (virtualisering ABI) til Linux-kerner version 2.6.x.

University of New South Wales og NICTA

Udviklere ved University of New South Wales har skabt L4/MIPS- og L4/Alpha-mikrokernerne, implementeringer af L4 til 64-bit MIPS- og DEC Alpha -seriens processorer . Den originale L4-mikrokerne understøttede kun x86-arkitekturprocessorer og blev uformelt kendt som "L4/x86". Implementeringerne blev skrevet fra bunden i C og assemblersprog og var ikke bærbare. Efter udgivelsen af ​​den platformsuafhængige mikrokerne L4Ka::Pistachio, stoppede UNSW-gruppen med at udvikle deres mikrokerner og begyndte at portere L4Ka::Pistachio-mikrokernen. Implementeringen af ​​meddelelsesoverførselsmekanismen viste sig at være hurtigere end andre implementeringer (36 cyklusser på Itanium- arkitekturprocessorer ) [16] .

UNSW-gruppen har vist, at en user-space- driver kan køre på samme måde som en kernel-space-driver [17] .

Hun udviklede komponenter til paravirtualisering af Linux-kerner. Komponenterne kørte oven på L4 mikrokernen. Resultatet er blevet kaldt " Wombat OS ". Wombat OS kunne køre på x86, ARM og MIPS arkitekturer. På Intel XScale-processorer udførte Wombat OS et kontekstskift 30 gange langsommere end en monolitisk Linux-kerne [18] .

UNSW-gruppen flyttede derefter til NICTA, skabte en gaffel af L4Ka::Pistachio-mikrokernen og kaldte den "NICTA::L4-indlejret". Den nye mikrokerne blev skrevet til kommercielle indlejrede systemer , krævede lidt hukommelse og implementerede en forenklet L4 API. Med en forenklet API blev systemkald lavet så "korte", at de ikke krævede forebyggende multitasking-punkter og tillod real-time OS- implementering [19] .

Kommerciel brug

Qualcomm kørte NICTAs implementering af L4-mikrokernen på et chipset kaldet "Mobile Station Modem" (MSM) Dette blev rapporteret i november 2005 [20] af NICTA-repræsentanter, og i slutningen af ​​2006 kom MSM-chipsæt til salg. Så implementeringen af ​​L4 mikrokernen endte i mobiltelefoner .

I august 2006 Heiser Open Kernel Labs På det tidspunkt fungerede Heiser som leder af ERTOS-programmet organiseret af NICTA [21] og var professor ved UNSW. OK Labs blev oprettet til

• yde teknisk support til L4 kommercielle brugere;
• fortsat udvikling af L4 sammen med NICTA for at fortsætte den kommercielle brug af implementeringen af ​​L4, men under OKL4- mærket .

I april 2008 blev version 2.1 af "OKL4"-mikrokernen frigivet, den første offentlige implementering af L4 med kapacitetsbaseret sikkerhed . I oktober 2008 blev version 3.0 [22] frigivet - den seneste open source-  version af "OKL4" . Kildekoden til følgende versioner er blevet lukket. Mikrokernelaget, der driver hypervisoren , er blevet omskrevet for at tilføje understøttelse af en native hypervisor kaldet "OKL4 microvisor" [23] .

OK Labs distribuerede et paravirtualiseret Linux  - operativsystem kaldet OK :Linux [24] . OK : Linux var en efterkommer af Wombat OS . OK Labs distribuerede også paravirtualiserede versioner af Symbian- og Android -operativsystemerne .

OK Labs har erhvervet rettighederne til seL4-mikrokernen fra NICTA.

I begyndelsen af ​​2012 blev der solgt mere end 1,5 milliarder enheder udstyret med en implementering af L4-mikrokernen [25] . De fleste af disse enheder indeholdt chips, der implementerer trådløse modemer og blev udgivet af Qualcomm .

En implementering af L4 er også blevet brugt i underholdningssystemer i bilen [26] .

OS, bygget på basis af L4-implementeringen, blev udført af den sikre enklave-processor, som er en del af Apple A7 elektroniske kredsløb placeret på chippen [27] . Den samme L4-implementering blev brugt i NICTAs Darbat-projekt [28] . Enheder, der indeholder Apple A7, leveret med iOS . Fra 2015 var der cirka 310 millioner iOS-enheder [29] .

Bekræftelse

seL4

I 2006 begyndte udviklingen af ​​tredje generations mikrokerne , kaldet "seL4" [30] . Udviklingen startede fra bunden af ​​en gruppe programmører fra NICTA. Formål: at skabe grundlag for at opbygge sikre og pålidelige systemer, der kan opfylde moderne sikkerhedskrav, som f.eks. er skrevet i dokumentet "Generelle kriterier for vurdering af informationsteknologisikkerhed". Helt fra begyndelsen var mikrokernekoden skrevet på en sådan måde, at det var muligt at verificere den (korrekthedstjek). Verifikation blev udført ved hjælp af Haskell-sproget : kravene til mikrokernen (specifikationen) blev skrevet på Haskell-sproget; mikrokerneobjekter blev repræsenteret som Haskell-objekter; arbejdet med udstyret blev emuleret [31] . For at kunne få information om tilgængeligheden af ​​et objekt ved at udføre formelle ræsonnementer, brugte seL4 adgangskontrol baseret på kapacitetsbaseret sikkerhed.

I 2009 blev beviset for rigtigheden af ​​seL4-mikrokernekoden [32] afsluttet . Eksistensen af ​​et bevis sikrede overensstemmelse mellem implementeringen og specifikationen, bekræftede fraværet af nogle fejl i implementeringen (for eksempel fraværet af deadlocks , livelocks, bufferoverløb , aritmetiske undtagelser og tilfælde af brug af uinitialiserede variabler). seL4-mikrokernen var den første mikrokerne designet til et generelt OS og verificeret [32] .

seL4-mikrokernen implementerede ikke-standard kerneressourcestyring [33] :

• kerneressourcer blev administreret af en brugerrumskomponent;
• den kapacitetsbaserede sikkerhedsmekanisme blev brugt ikke kun til at kontrollere adgang til brugerrumsressourcer, men også til at kontrollere adgang til kerneressourcer.

Noget lignende blev implementeret i det eksperimentelle Barrelfish OS . Takket være denne tilgang til styring af kerneressourcer blev det muligt at udføre ræsonnementer om isolering af egenskaber, og senere blev det bevist, at mikrokernen seL4 sikrer integriteten og fortroligheden af ​​egenskaber [34] . Beviset blev udført for den originale kode.

Et team af forskere fra NICTA-firmaet beviste rigtigheden af ​​at oversætte tekst fra C-sprog til maskinkode. Dette gjorde det muligt at udelukke compileren fra listen over betroet software og betragte beviset udført for mikrokernens kildekode for også at være gyldigt for mikrokernens eksekverbare fil.

seL4-mikrokernen blev den første kerne i beskyttet tilstand, for hvilken den værst tænkelige eksekveringstidsanalyse blev udført fuldt ud, og resultaterne af denne analyse blev offentliggjort. Resultaterne af analysen er nødvendige for at bruge mikrokernen i et hårdt real-time OS [34] .

29. juli 2014 NICTA og General Dynamics C4 Systemsannoncerede frigivelsen af ​​seL4-mikrokernen (inklusive alle beviser for deres rigtighed) under åbne licenser [35] . Mikrokernens kildekode og beviser blev frigivet under GPL v2-licensen. De fleste af bibliotekerne og værktøjerne blev distribueret under BSD-licensen med 2 klausuler.

En interessant udtalelse fra forskere [36] er, at omkostningerne ved at udføre softwareverifikation er lavere end omkostningerne ved traditionel softwareforskning, på trods af at meget mere pålidelig information kan opnås under verifikation.

I august 2012 NICTA, Rockwell Collins, Galois Inc , Boeing og University of Minnesota , som en del af et program til udvikling af yderst pålidelige militære cybersystemer [37] organiseret af DARPA- agenturet , er begyndt at udvikle et ubemandet luftfartøj [38] . Hovedkravet til udviklingen er at sikre enhedens høje pålidelighed. Hver af de opførte firmaer havde en rolle at spille i programmet. NICTA var ansvarlig for udviklingen af ​​operativsystemet og byggede det op omkring seL4-mikrokernen. Ansvarlige opgaver blev implementeret som mikrokernekomponenter, mens ikke-ansvarlige blev kørt under et paravirtualiseret Linux OS. Udviklingen af ​​programmet var planlagt til at blive brugt i NICTA Unmanned Little Bird-helikopteren, som blev udviklet af Boeing. Helikopteren skulle understøtte både pilotkontrol og ubemandet tilstand. I november 2015 blev der rapporteret om en vellykket implementering [39] .

Anden forskning og udvikling

Hurd/L4 . I november 2000 blev "l4-hurd"-mailinglisten oprettet for at diskutere ideen om at portere " GNU Hurd "-kernen til L4-mikrokernen. Portering blev udført i 2002-2004, resultatet blev kaldt "Hurd / L4". Implementering af "Hurd/L4" blev ikke afsluttet. I 2005 blev projektet stoppet [40] .

Osker  er et operativsystem, der implementerer L4 og blev skrevet i Haskell i 2005 . Formålet med projektet: at teste muligheden for at implementere OS i et funktionelt sprog (og ikke at studere mikrokernen) [41] .

Codezero  er en implementering af L4-mikrokernen til indlejrede systemer, der blev offentligt tilgængelig i sommeren 2009 [42] . Skabt af udviklerne af det britiske firma "B Labs" fra bunden. Koden blev skrevet i C. Implementeringen understøtter ARM -arkitekturprocessorer , implementerer en første-ordens hypervisor og understøtter Linux og Android OS virtualisering [43] [44] . På trods af erklæringen om levering af koden under GPL v3-licensen er det umuligt at downloade koden fra det officielle websted.

F9  er en implementering af L4-mikrokernen, der blev offentligt tilgængelig i juli 2013 [45] . Skrevet fra bunden i C. Designet til indlejrede systemer. Understøtter ARM-arkitektur Cortex-M- processorserien . Koden leveres under en BSD-licens.

Fiasco.OC  er en tredje generations mikrokerne baseret på "L4/Fiasco" mikrokernen. Implementerer den kapacitetsbaserede sikkerhedsmekanisme, understøtter multi-core processorer og hardware virtualisering [46] .

L4 Runtime Environment (L4Re for kort) er en ramme, der kører oven på "Fiasco.OC" mikrokernen og er designet til at skabe brugerrumskomponenter. L4Re leverer funktionalitet til opbygning af klient/server-applikationer, implementering af filsystemer, implementering af populære biblioteker såsom C-standardbiblioteket ("libc"), C++-standardbiblioteket ("libstdc++") og pthreads- biblioteket .

L4Re-rammeværket og "Fiasco.OC" mikrokernen understøttede x86 (IA-32 og AMD64), ARM og PowerPC (WiP) arkitekturer.

L4Linux  er et undersystem til at køre Linux OS oven på "Fiasco.OC" mikrokernen ved hjælp af paravirtualisering [47] . Tidligere blev i stedet for parret "Fiasco.OC" - L4Re brugt parret "L4 / Fiasco" - L4Env.

NOVA ( N OVA O S v irtualiseringsarkitekturen ) er et forskningsprojekt skabt for at skabe et sikkert og effektivt virtualiseringsmiljø [ 48  ] [49] [50] med en lille liste over betroet software ( trusted computing base ) . NOVA inkluderer:  

• en mikrokerne, der implementerer L4 og en første-ordens hypervisor ( baremetal  hypervisor );
• VMM Vancouver er en mikrokernekomponent (proces), der kører i brugerrummet, der er involveret i servicering (hardwareemulering) af en virtuel maskine og frataget privilegier. Én VMM blev lanceret pr. virtuel maskine. VMM Vancouver er en del af NUL og kan erstattes af VMM Seoul. VMM Seoul [51] er baseret på VMM Vancouver;
• NUL ( N OVA u - ser - l evel  environment ) - nogle komponenter af mikrokernen, der fungerer i brugerrummet (VMM Vancouver, enhedsdrivere (for eksempel netværkskort); partitionsmanager; komponenter designet til at styre hukommelse, I/O; komponenter, implementering af stakke af TCP/IP , USB osv.). NUL kan erstattes med genode eller NRE. NRE ( N OVA r untime e nvironment ) er en efterkommer af NUL. 

NOVA-projektet understøttede x86-processorer med flere kerner. For at køre under kontrol af en mikro-hypervisor (en hypervisor bygget på en mikrokerne) NOVA, skal gæsteoperativsystemet understøtte Intel VT-x eller AMD-V . Kildekoden blev leveret under GPL v2-licensen.

Xameleon  er et operativsystem baseret på L4 mikrokernen [52] . Projektet blev grundlagt i 2001 af den eneste udvikler Alexei Mandrykin (født 19. januar 1973 ). OS blev oprindeligt bygget oven på " L4/Fiasco " mikrokernen. Senere migrerede forfatteren OS til " L4Ka::Pistachio " mikrokernen. OS-kildekoden er lukket.

WrmOS er et open source real-time operativsystem (RTOS) baseret på L4 mikrokernen. WrmOS har sin egen implementering af kernen, standardbiblioteker og netværksstakken. Understøttede processorarkitekturer er SPARC, ARM, x86, x86_64. WrmOS-kernen er baseret på L4 Kernel Reference Manual Version X.2- dokumentet . Der kører en paravirtualiseret Linux-kerne ( w4linux ) oven på WrmOS.

Noter

1. ↑ 1 2 Liedtke, Jochen (december 1993 ). "Forbedring af IPC ved kernedesign" (PDF) . 14. ACM -symposium om operativsystemets principper . Asheville , NC , USA . pp. 175-88. Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 4. marts 2016 på Wayback Machine
2. ↑ L4 familie af mikrokerner. Oversigt Arkiveret 14. maj 2015 på Wayback Machine  (engelsk) // Website for Technical University of Dresden ( Tyskland ).
3. ↑ ELAN Language Arkiveret 12. maj 2015 på Wayback Machine  // Technical University of Dresden hjemmeside .
4. ↑ 1 2 3 4 5 6 7 8 9 10 Liedtke, Jochen (december 1993 ). "Et vedvarende system i virkelig brug - erfaringer fra de første 13 år" (PDF) . Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS) . Asheville , NC , USA . pp. 2-11. Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 10. juli 2015 på Wayback Machine
5. ↑ 1 2 In Memoriam Jochen Liedtke (1953-2001) Arkiveret 5. marts 2012 på Wayback Machine .
6. ↑ 1 2 Liedtke, Jochen (december 1995 ). "Om µ-kernekonstruktion" . Proc. 15. ACM -symposium om operativsystemets principper (SOSP) . pp. 237-250. Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 18. marts 2009 på Wayback Machine
7. ↑ 1 2 3 Systemarkitekturgruppe. om os. mennesker. Liedtke . Arkiveret kopi .
8. ↑ Jochen Liedtke. Sidetabelstrukturer til finkornet virtuel hukommelse Arkiveret 12. november 2007 på Wayback Machine . Teknisk rapport 872. Tysk nationalt forskningscenter for datalogi (GMD). oktober 1994 .
9. ↑ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathan; Deller, Luke; Reuther, Lars ( 2000 ). "Savværkets multiservertilgang" . ACM SIGOPS European Workshop . Kolding , Danmark . pp. 109-114. Tjek datoen på |date=( hjælp på engelsk )
10. ↑ Fleisch, Brett D; Allan, Mark. Workplace Microkernel and OS: A Case  Study . — John Wiley & Sons, Ltd. Arkiveret fra originalen den 24. august 2007.
11. ↑ "L4Ka" gruppeside // archive.org .
12. ↑ Drops oversigt Arkiveret 7. august 2011 på Wayback Machine .
13. ↑ Mikrokernel "L4Ka::Pistachio" Arkiveret 9. januar 2007 på Wayback Machine  .
14. ↑ "L4Ka" udviklingsteam Arkiveret 22. januar 2007 på Wayback Machine  .
15. ↑ L4Ka::Pistachio-mikrokernen . (engelsk) Hvidbog . PDF . 1. maj 2003 // archive.org .
16. ↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (april 2005). Itanium-systemimplementeringsfortælling . USENIX årlige tekniske konference . Annaheim , CA , USA . pp. 264-278. Forældet parameter brugt |coauthors=( hjælp );Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 17. februar 2007 på Wayback Machine
17. ↑ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Gotz, Stefan; Grey, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot . Enhedsdrivere på brugerniveau : opnået ydeevne  (neopr.)  // Journal of Computer Science and Technology. - T. 20 , nr. 5 . — S. 654-664 . - doi : 10.1007/s11390-005-0654-4 .
18. ↑ van Schaik, Carl; Heiser, Gernot (januar 2007). "Højtydende mikrokerner og virtualisering på ARM og segmenterede arkitekturer" . 1. internationale workshop om mikrokerner til indlejrede systemer . Sydney , Australien : NICTA . pp. 11-21 . Hentet 2007-04-01 . Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 26. april 2007 på Wayback Machine
19. ↑ Ruocco, Sergio. En programmørs rundvisning i realtid af L4-mikrokerner til generelle formål //  EURASIP  Journal om indlejrede systemer, specialudgave om operativsystemstøtte til indlejrede realtidsapplikationer: journal. - 2008. - Oktober ( bind 2008 ). - S. 1-14 . - doi : 10.1155/2008/234710 .  (utilgængeligt link)
20. ↑ [1] Arkiveret 25. august 2006 på Wayback Machine .
21. ↑ ERTOS- programsiden på NICTA-webstedet // archive.org .
22. ↑ OKL4 3.0 (downlink) . Hentet 21. maj 2011. Arkiveret fra originalen 16. maj 2011. (ubestemt) 
23. ↑ OKL4 microvisor Arkiveret 13. marts 2014 på Wayback Machine .
24. ↑ OK:Linux (downlink) . Hentet 8. juli 2015. Arkiveret fra originalen 10. april 2015. (ubestemt) 
25. ↑ Åbne Kernel Labs (19. januar 2012). Open Kernel Labs-software overgår milepælen på 1,5 milliarder forsendelser af mobilenheder . Pressemeddelelse . Hentet 2015-11-10 .
26. ↑ Åbne Kernel Labs ( 27. marts 2012 ). Open Kernel Labs Automotive Virtualization valgt af Bosch til infotainmentsystemer . Pressemeddelelse . Arkiveret fra originalen den 2. juli 2012.
27. ↑ iOS-sikkerhed . Hentet 28. september 2017. Arkiveret fra originalen 23. september 2014. (ubestemt)
28. ↑ Darbat-projektet Arkiveret 19. december 2013 på Wayback Machine .
29. ↑ [2] Arkiveret 15. juli 2015 på Wayback Machine .
30. ↑ [3] Arkiveret 3. maj 2022 på Wayback Machine .
31. ↑ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; hane; David; Chakravarty, Manuel MT (september 2006 ). "Kørsel af manualen: en tilgang til udvikling af mikrokerner med høj sikkerhed" (PDF) . ACM SIGPLAN Haskell Workshop . Portland , Oregon , USA . pp. 60-71. Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 3. marts 2016 på Wayback Machine
32. ↑ 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronick, juni; Pik, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Berøring, Harvey; Winwood, Simon (oktober 2009 ). "seL4: Formel verifikation af en OS-kerne" (PDF) . 22. ACM -symposium om operativsystemets principper . Big Sky , MT , USA . Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 28. juli 2011 på Wayback Machine
33. ↑ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (april 2008 ). "Kernedesign til isolering og sikring af fysisk hukommelse" . 1. workshop om isolation og integration i indlejrede systemer . Glasgow , Storbritannien . DOI : 10.1145/1435458 . Hentet 2015-07-08 . Forældet parameter brugt |coauthors=( hjælp );Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 24. april 2010 på Wayback Machine
34. ↑ 1 2 Klein, Gerwin; Andronick, juni; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Omfattende formel verifikation af en OS-mikrokerne  (engelsk)  // ACM Transactions on Computer Systems: journal. — Bd. 32 , nr. 1 . — S. 2:1-2:70 . - doi : 10.1145/2560537 .
35. ↑ NICTA ( 29. juli 2014 ). Sikkert operativsystem udviklet af NICTA går i åben kildekode . Pressemeddelelse . Arkiveret fra originalen 10. august 2014. Hentet 2015-07-08 .
36. ↑ Klein, Gerwin; Andronick, juni; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Omfattende formel verifikation af en OS-mikrokerne  (engelsk)  // ACM Transactions on Computer Systems: journal. - 2014. - Bd. 32 . — S. 64 . - doi : 10.1145/2560537 .
37. ↑ Cybermilitære systemer med høj sikkerhed Arkiveret 8. august 2014. (HACM'er).
38. ↑ SMACCM-projektet arkiveret 10. juli 2015 på Wayback Machine // NICTA- webstedet. SMACCM er en forkortelse af engelsk.  sikker matematisk sikker sammensætning af kontrolmodeller .
39. ↑ Ny generations droner kan ikke hackes Arkiveret 18. november 2015 på Wayback Machine // Popular Mechanics Magazine. 12. november 2015.
40. ↑ Historien om GNU Hurd. Portering til en anden mikrokerne Arkiveret 8. marts 2017 på Wayback Machine  .
41. ↑ Hallgren, T.; Jones, MP; Leslie, R.; Tolmach, A. En principiel tilgang til operativsystemkonstruktion i Haskell  //  Proceedings of the tiende ACM SIGPLAN internationale konference om funktionel programmering: tidsskrift. - 2005. - Bd. 40 , nej. 9 . - S. 116-128 . — ISSN 0362-1340 . - doi : 10.1145/1090189.1086380 .
42. ↑ Codezero Arkiveret 9. juli 2015 på Wayback Machine på genode.org.
43. ↑ dev.b-labs.com // archive.org .
44. ↑ Officiel hjemmeside for Codezero-projektet Arkiveret 9. juli 2015 på Wayback Machine .
45. ↑ F9-projektlager Arkiveret 5. marts 2017 på Wayback Machine // github.com .
46. ↑ Peter, Michael; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (marts 2009 ). "Virtuelle maskiner fængslet - Virtualisering i systemer med små pålidelige computerbaser" . VTDS'09: Workshop om virtualiseringsteknologi til pålidelige systemer . Nürnberg , Tyskland . Forældet parameter brugt |coauthors=( hjælp );Tjek datoen på |date=( hjælp på engelsk )
47. ↑ L4Linux Arkiveret 7. juli 2015 på Wayback Machine .
48. ↑ Steinberg, Udo; Bernhard, Kauer (april 2010 ). "NOVA: En mikrohypervisor-baseret sikker virtualiseringsarkitektur". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems . Paris , Frankrig . Tjek datoen på |date=( hjælp på engelsk )
49. ↑ Steinberg, Udo; Bernhard, Kauer (april 2010 ). "Mod et skalerbart multiprocessormiljø på brugerniveau". IIDS'10: Workshop om isolation og integration for pålidelige systemer . Paris , Frankrig . Tjek datoen på |date=( hjælp på engelsk )
50. ↑ Project Nova Arkiveret 24. juni 2015 på Wayback Machine . Officiel side.
51. ↑ VMM Seoul Arkiveret 11. juni 2018 på Wayback Machine // github.com
52. ↑ l4os.ru Arkiveret 9. februar 2011 på Wayback Machine . Xameleon-projektets officielle hjemmeside.

Litteratur

• Jochen Liedtke , Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. To års erfaring med et μ-Kernel baseret OS . ACM Tryk. 1991
• Liedtke, Jochen ; Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar (2000-10-22). "Stub-Code Ydelse bliver vigtig" . I Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego , CA , oktober 2000 . Arkiveret fra originalen (PDF) 2006-09-05 . Hentet 2006-09-05 . Forældet parameter brugt |coauthors=( hjælp ) Arkiveret 5. september 2006 på Wayback Machine (på L4 mikrokernen og compileren).
• Cheng Guanghui, Nicholas McGuire. L4/Fiasco/L4Linux Kickstart , Distributed & Embedded Systems Lab - Lanzhou University .
• Elphinstone, Kevin; Heiser, Gernot (oktober 2014 ). "Fra L3 til seL4: Hvad har vi lært i 20 år med L4-mikrokerner?" . 24. ACM SIGOPS-symposium om operativsystemets principper . Farmington , PA , USA . pp. 133-150. Tjek datoen på |date=( hjælp på engelsk ) Arkiveret 12. august 2014 på Wayback Machine L4 arkitekturudvikling og implementeringstilgange.

Links

• L4Hq : L4-hovedkvarter, et fællesskabswebsted om L4-implementeringer.
• L4 mikrokernefamilien . Oversigt over L4 implementeringer, dokumentation og projekter.
• Den officielle wiki for TUD:OS-projektet .
• L4ka . L4 implementeringer "L4Ka::Pistachio" og "L4Ka::Hazelnut".
• UNSW . Implementering af L4 til DEC Alpha processorer og MIPS arkitektur processorer .
• OKL4 . Kommerciel implementering af L4 fra Open Kernel Labs .
• Implementering af L4 fra NICTA . Forskningsanmeldelser og publikationer.
• Genode operativsystemramme . Ramme til opbygning af operativsystemer, udviklet af L4-fællesskabet.
• Officiel side dedikeret til L3-kernen
• Microkernel L4 som grundlag for OS-kernen