L4 (mikrokärna)

L4
Sorts mikrokärna
Författare Jochen Liedtke
Utvecklaren Jochen Liedtke
Skrivet i assembleringsspråk
Hemsida l4hq.org

L4  är en andra generationens mikrokärna utvecklad av Jochen Liedtke 1993 [ 1] .

L4-mikrokärnarkitekturen visade sig vara framgångsrik. Många implementeringar av L4-mikrokärnans ABI och API har skapats. Alla implementeringar blev kända som L4-familjen av mikrokärnor. Liedtkes implementering har informellt fått namnet "L4/x86" [2] .

Historik

L1

1977 försvarade Jochen Liedtke sitt diplomprojekt i matematik vid universitetet i Bielefeld (Tyskland). Som en del av projektet skrev Liedtke en kompilator för ELAN- språket ( eng. ). ELAN-språket skapades 1974 på basis av språket Algol 68 för undervisning i programmering [3] . Liedtke kallade sitt verk "L1": bokstaven "L" är den första bokstaven i författarens efternamn ( L iedtke ); siffran "1" är verkets serienummer.

L2

1977 tog Liedtke examen som matematiker, stannade vid universitetet i Bielefeld och började skapa en runtime-miljö för ELAN-språket.

8-bitars mikrokontroller blev allmänt tillgängliga. Det krävdes ett operativsystem som kunde köras på små arbetsstationer på gymnasier och universitet. CP/M passade inte. Det tyska nationella forskningscentret för datavetenskap och teknologi GMD och universitetet i Bielefeld beslutade att utveckla ett nytt operativsystem från grunden [4] .

1979 började Jochen Liedtke utveckla ett nytt operativsystem och döpte det till " Eumel " ( engelska ) från engelska.  Utökningsbar fleranvändarmikroprocessor EL AN - system . _ _ Operativsystemet "Eumel" kallades också "L2", vilket betyder " Liedtkes andra verk " . Det nya operativsystemet stödde 8-bitars Zilog Z80-processorer , var multi-användare och multitasking byggdes på en mikrokärna och ortogonal persistens Stöd för ortogonal beständighet var följande: OS sparade med jämna mellanrum sitt tillstånd på disk (innehållet i minnet , processorregister , etc.); efter strömavbrott återställdes operativsystemet från ett sparat tillstånd; programmen fortsatte att fungera som om felet inte hade inträffat; endast ändringar gjorda sedan den senaste lagringen gick förlorade. Eumel OS var inspirerat av Multics OS och delade många likheter med Accent och Mach 4kärnorna

Eumel OS portades senare till Zilog Z8000 , Motorola 68000 och Intel 8086 processorer . Dessa processorer var 8-bitars och 16-bitars, innehöll ingen MMU och stödde inte en minnesskyddsmekanism . Eumel OS emulerade en virtuell maskin med 32-bitars adressering och en MMU [4] . Trots användningen av emulering kunde upp till fem terminaler anslutas till en arbetsstation som kör Eumel OS [4] .

Till en början var det möjligt att skriva program för Eumel OS endast på ELAN-språket. Kompilatorer för CDLPascal Basic och DYNAMO lades till senare men de användes inte i stor utsträckning 4

Sedan 1980 började användningen av Eumel OS, först för undervisning i programmering och ordbehandling, och sedan för kommersiella ändamål. Så i mitten av 1980-talet kördes Eumel OS redan på mer än 2000 datorer på advokatbyråer och andra företag [4] .

L3

Med tillkomsten av processorer som stöder virtuellt minne (på grund av MMU) och mekanismer för dess skydd, har behovet av att emulera en virtuell maskin försvunnit.

1984 [ 5] gick Jochen Liedtke till jobbet vid GMD forskningscenter för att skapa ett OS som liknar Eumels, men utan emulering. GMD är för närvarande en del av Fraunhofer Society .

Sedan 1987 [4] har Jochen Liedtke och hans team vid SET Institute , en del av GMD, börjat utveckla en ny mikrokärna, kallad "L3" ("L3" från " L iedtkes 3: e verk ").

Jochen Liedtke ville se om det var möjligt att uppnå hög prestanda för IPC- komponenten genom att välja rätt arkitektur för kärnan och använda funktionerna i hårdvaruplattformen i implementeringen . Implementeringen av IPC-mekanismen visade sig vara framgångsrik (jämfört med den komplexa implementeringen av IPC i Mach-mikrokärnan). Senare implementerades en mekanism för att isolera minnesområden för processer som körs i användarutrymmet .

1988 slutfördes utvecklingen och operativsystemet med samma namn släpptes. L3-mikrokärnan skrevs i assemblerspråk , använde funktionerna hos Intel x86 -arkitekturprocessorerna , stödde inte andra plattformar och överträffade Mach-mikrokärnan i prestanda. L3 OS var kompatibelt med Eumel OS: program skapade för Eumel OS kördes under L3 OS, men inte vice versa [4] .

L3 mikrokärnkomponenter:

Sedan 1989 [4] har operativsystemet använts:

L4

Under arbetet med L3-mikrokärnan upptäckte Jochen Liedtke brister i Mach-mikrokärnan. Liedtke ville förbättra prestandan och började koda den nya mikrokärnan i assemblerspråk med funktionerna i Intel i386- processorarkitekturen . Den nya mikrokärnan kallades "L4" (från " L iedtkes 4 :e verk ").

1993 slutfördes implementeringen av L4-mikrokärnan. IPC-komponenten visade sig vara 20 gånger snabbare än IPC från Mach-mikrokärnan [1] .

OS byggt på första generationens mikrokärnor (i synnerhet på Mach-mikrokärnan) kännetecknades av låg prestanda. På grund av detta började utvecklare i mitten av 1990 - talet ompröva konceptet med mikronukleär arkitektur. I synnerhet förklarades den dåliga prestandan för Mach-mikrokärnan genom att flytta den komponent som ansvarar för IPC till användarutrymmet.

Vissa komponenter i Mach-mikrokärnan returnerades tillbaka - inuti mikrokärnan . Detta kränkte själva idén om mikrokärnor (minsta storlek, isolering av komponenter), men tillät att öka prestanda hos operativsystemet.

Forskarna sökte efter orsakerna till Mach-mikrokärnans dåliga prestanda och analyserade noggrant de komponenter som är viktiga för god prestanda. Analysen visade att kärnan allokerade en för stor arbetsuppsättning (mycket minne) till processerna, vilket resulterade i att cachemissar hela tiden inträffade när kärnan fick åtkomst till minnet [ 6 ] . Analysen gjorde det möjligt att formulera en ny regel för mikrokärnutvecklare - mikrokärnan ska utformas så att de komponenter som är viktiga för att säkerställa hög prestanda placeras i processorns cache (helst den första nivån ( engelska nivå 1 , L1) och det är önskvärt att det fortfarande finns lite utrymme kvar i cachen ).   

På grund av ökningen i prestanda hos IPC-komponenten kunde befintliga operativsystem inte hantera det ökade inflödet av IPC-meddelanden. Flera universitet (t.ex. Technical University Dresden , University of New South Wales ), institutioner och organisationer (t.ex. IBM ) har börjat skapa implementeringar av L4 och bygga nya operativsystem runt dem.

1996 försvarade Liedtke sin doktorsavhandling [7] vid Tekniska universitetet i Berlin på ämnet "skyddade sidtabeller" [8] .

Sedan 1996, vid Research Center, har och hans kollegor fortsatt forskning om L4-mikrokärnan, mikrokärnor i allmänhet och Sawmill OS operativsystem i synnerhet [9] . På grund av bristen på kommersiell framgång, operativsystemet " IBM Workspace OS ", byggt på den tredje versionen av Mach-mikrokärnan från CMU och utvecklat av IBM från januari 1991 till 1996 [10] istället för konceptet " L4 microkernel" använde konceptet "Lava Nucleus" eller "LN" för kort.

Med tiden släpptes L4-mikrokärnkoden från att vara bunden till plattformen, säkerhets- och isoleringsmekanismerna förbättrades.

1999 började Liedtke arbeta som professor i operativsystem vid Karlsruhe Institute of Technology (Tyskland) [7] .

Microkernel L4Ka::Hasselnöt

1999 antogs Jochen Liedtke i Systems Architecture Group (SAG), som arbetar vid Karlsruhe Institute of Technology (Tyskland), och fortsatte forskning om mikronukleära operativsystem. SAG-gruppen är också känd som "L4Ka"-gruppen.

SAG -gruppen ville bevisa att en mikrokärna kunde implementeras på ett högnivåspråk och utvecklade mikrokärnan "L4Ka::Hazelnut". Arbetet utfördes vid Karlsruhes tekniska högskola med stöd av DFG [11] . Implementeringen skrevs i C++ och stödde IA-32- och ARM-arkitekturprocessorer . Prestandan för den nya mikrokärnan visade sig vara acceptabel och utvecklingen av assembly-språkkärnor avbröts.

Microkernel L4/Fiasco

1998 började Dresden Technical University Operating Systems Group utveckla sin egen implementering av L4-mikrokärnan, kallad "L4/Fiasco". Utvecklingen genomfördes i C++ parallellt med utvecklingen av mikrokärnan L4Ka::Hazelnut.

Vid den tiden stödde inte L4Ka::Hazelnut-mikrokärnan samtidighet mellan kärna och rymden, och "L4Ka::Pistachio"-mikrokärnan stödde endast kärn-space- avbrott vid specifika preemption-punkter. Utvecklarna av mikrokärnan "L4/Fiasco" har implementerat fullständig förebyggande multitasking (med undantag för vissa atomoperationer). Detta gjorde kärnarkitekturen mer komplex, men minskade avbrottslatenser, vilket är viktigt för ett realtidsoperativsystem.

Mikrokärnan "L4/Fiasco" användes i OS "DROPS" [12]  - OS för "hård" realtid (när det är extremt viktigt att händelsen besvaras inom strikta tidsramar), även utvecklat vid Tekniska universitetet i Dresden.

På grund av komplexiteten i mikrokärnarkitekturen i senare versioner av Fiasco OS, återgick utvecklarna till det traditionella tillvägagångssättet - att starta kärnan med avstängda avbrott (med undantag för några få företrädespunkter).

Plattformsoberoende

Microkernel L4Ka::Pistachio

Implementeringar av L4-mikrokärnan, skapade före lanseringen av L4Ka::Pistachio-mikrokärnan och senare versioner av "Fiasco"-mikrokärnan, använde funktionerna i datorarkitekturen (de var "bundna" till processorarkitekturen). Ett arkitekturoberoende API utvecklades. Trots tillägget av portabilitet gav API:et hög prestanda. Idéerna bakom mikrokärnarkitekturen har inte förändrats.

I början av 2001 publicerades ett nytt L4 API, mycket annorlunda än den tidigare versionens L4 API, med versionsnummer 4 ("version 4", även känd som "version X.2"), och annorlunda:

Efter lanseringen av den nya versionen av API:t började SAG-teamet skapa en ny mikrokärna, kallad "L4Ka::Pistachio" [13] [14] . Koden kompilerades från grunden i C++ med hjälp av erfarenheten från L4Ka::Hazelnut-projektet. Uppmärksamhet ägnades åt hög prestanda och portabilitet.

Den 10 juni 2001 dog Dr Jochen Liedtke [7] i en bilolycka. Därefter minskade utvecklingstakten av projektet markant.

År 2003 [15] slutfördes arbetet tack vare insatser från Liedtkes elever: Volkmar Uhlig, Uwe Dannowski och Espen Skoglund. Källkoden har släppts under BSD-licensen med 2 klausuler .

Nya versioner av Fiasco

Parallellt fortsatte utvecklingen av L4/Fiasco-mikrokärnan. Stöd för flera hårdvaruplattformar ( x86 , AMD64 , ARM ) har lagts till. Noterbart är att en version av Fiasco kallad "FiascoUX" skulle kunna köras i användarutrymme som kör Linux OS .

Utvecklarna av L4/Fiasco-mikrokärnan har implementerat flera tillägg till L4v2 API.

Dessutom tillhandahöll mikrokärnan "Fiasco" mekanismer för hantering av kommunikationsrättigheter. Samma mekanismer fanns för att hantera resurserna som förbrukades av kärnan.

"L4Env" utvecklades, en uppsättning komponenter som körs ovanpå "Fiasco"-mikrokärnan i användarutrymmet. "L4Env" användes i "L4Linux", en implementering av paravirtualisering (virtualisering ABI) för Linux-kärnor version 2.6.x.

University of New South Wales och NICTA

Utvecklare vid University of New South Wales har skapat mikrokärnorna L4/MIPS och L4/Alpha, implementeringar av L4 för 64-bitars MIPS- och DEC Alpha -seriens processorer . Den ursprungliga L4-mikrokärnan stödde endast x86-arkitekturprocessorer och blev informellt känd som "L4/x86". Implementeringarna skrevs från grunden i C och assemblerspråk och var inte bärbara. Efter lanseringen av den plattformsoberoende mikrokärnan L4Ka::Pistachio, slutade UNSW-gruppen att utveckla sina mikrokärnor och började porta L4Ka::Pistachio-mikrokärnan. Implementeringen av meddelandeöverföringsmekanismen visade sig vara snabbare än andra implementeringar (36 cykler på Itanium- arkitekturprocessorer ) [16] .

UNSW-gruppen har visat att en drivrutin för användarutrymme kan köras på samma sätt som en drivrutin för kärnutrymme [17] .

Hon utvecklade komponenter för paravirtualisering av Linux-kärnor. Komponenterna kördes ovanpå L4-mikrokärnan. Resultatet har kallats " Wombat OS ". Wombat OS kunde köras på x86, ARM och MIPS arkitekturer. På Intel XScale-processorer utförde Wombat OS en kontextväxling 30 gånger långsammare än en monolitisk Linuxkärna [18] .

UNSW-gruppen flyttade sedan till NICTA, skapade en gaffel av L4Ka::Pistachio-mikrokärnan och döpte den till "NICTA::L4-inbäddad". Den nya mikrokärnan skrevs för kommersiella inbäddade system , krävde lite minne och implementerade ett förenklat L4 API. Med ett förenklat API gjordes systemanrop så "korta" att de inte krävde förebyggande multitasking-punkter och tillät realtidsimplementering av OS [19] .

Kommersiell användning

Qualcomm körde NICTA :s implementering av L4-mikrokärnan på en chipset kallad "Mobile Station Modem" (MSM) Detta rapporterades i november 2005 [20] av NICTA-representanter, och i slutet av 2006 började MSM-chipset säljas. Så implementeringen av L4-mikrokärnan hamnade i mobiltelefoner .

I augusti 2006 grundade Open Kernel Labs Vid den tiden tjänstgjorde Heiser som chef för ERTOS-programmet organiserat av NICTA [21] och var professor vid UNSW. OK Labs skapades för att

I april 2008 släpptes version 2.1 av "OKL4"-mikrokärnan, den första offentliga implementeringen av L4 som har kapacitetsbaserad säkerhet . I oktober 2008 släpptes version 3.0 [22] - den senaste versionen med öppen källkod  av "OKL4" . Källkoden för följande versioner har stängts. Mikrokärnlagret som driver hypervisorn har skrivits om för att lägga till stöd för en inbyggd hypervisor som kallas "OKL4 microvisor" [23] .

OK Labs distribuerade ett paravirtualiserat Linux -  operativsystem som heter OK :Linux [24] . OK : Linux var en ättling till Wombat OS . OK Labs distribuerade också paravirtualiserade versioner av operativsystemen Symbian och Android .

OK Labs har förvärvat rättigheterna till seL4 mikrokärnan från NICTA.

I början av 2012 såldes mer än 1,5 miljarder enheter utrustade med en implementering av L4-mikrokärnan [25] . De flesta av dessa enheter innehöll chips som implementerar trådlösa modem och släpptes av Qualcomm .

En implementering av L4 har också använts i underhållningssystem i bilen [26] .

OS, byggt på basis av L4-implementationen, exekverades av den säkra enklavprocessorn, som är en del av Apple A7 elektroniska krets som finns på chipet [27] . Samma L4-implementering användes i NICTA:s Darbat-projekt [28] . Enheter som innehåller Apple A7 levereras med iOS . Från och med 2015 fanns det cirka 310 miljoner iOS-enheter [29] .

Verifiering

seL4

2006 började utvecklingen av tredje generationens mikrokärna , kallad "seL4" [30] . Utvecklingen startade från början av en grupp programmerare från NICTA. Syfte: att skapa underlag för att bygga säkra och tillförlitliga system som kan uppfylla moderna säkerhetskrav, som t ex skrivits i dokumentet "Allmänna kriterier för bedömning av informationsteknologisäkerhet". Redan från början var mikrokärnkoden skriven på ett sådant sätt att det gick att verifiera den (korrekthetskontroll). Verifieringen utfördes med hjälp av Haskell-språket : kraven för mikrokärnan (specifikationen) skrevs på Haskell-språket; mikrokärnobjekt representerades som Haskell-objekt; arbete med utrustningen emulerades [31] . För att kunna få information om ett objekts tillgänglighet genom att utföra formella resonemang använde seL4 åtkomstkontroll baserad på förmågasbaserad säkerhet.

Under 2009 slutfördes beviset för att seL4-mikrokärnkoden [32] var korrekt . Förekomsten av ett bevis som säkerställde överensstämmelse mellan implementeringen och specifikationen bekräftade frånvaron av några buggar i implementeringen (till exempel frånvaron av dödlägen , livelås, buffertspill , aritmetiska undantag och fall av användning av oinitierade variabler). seL4-mikrokärnan var den första mikrokärnan som designats för ett generellt operativsystem och verifierad [32] .

seL4-mikrokärnan implementerade icke-standardiserad kärnresurshantering [33] :

Något liknande implementerades i det experimentella OS Barrelfish . Tack vare detta tillvägagångssätt för att hantera kärnresurser blev det möjligt att föra resonemang om isolering av egenskaper, och senare bevisades det att mikrokärnan seL4 säkerställer integriteten och konfidentialitet för egenskaper [34] . Beviset gjordes för den ursprungliga koden.

Ett team av forskare från NICTA-företaget bevisade riktigheten av att översätta text från C-språk till maskinkod. Detta gjorde det möjligt att utesluta kompilatorn från listan över tillförlitlig programvara och betrakta beviset som utförts för mikrokärnans källkod som giltigt även för den körbara mikrokärnfilen.

seL4-mikrokärnan blev den första kärnan i skyddat läge för vilken den värsta exekveringstidsanalysen utfördes i sin helhet, och resultaten av denna analys publicerades. Resultaten av analysen är nödvändiga för att använda mikrokärnan i ett hårt realtidsoperativsystem [34] .

29 juli 2014 NICTA och General Dynamics C4 Systemstillkännagav lanseringen av seL4-mikrokärnan (inklusive alla bevis på deras riktighet) under öppna licenser [35] . Mikrokärnans källkod och bevis släpptes under GPL v2-licensen. De flesta av biblioteken och verktygen distribuerades under BSD-licensen med 2 klausuler.

Ett intressant påstående från forskare [36] är att kostnaden för att utföra programvaruverifiering är lägre än kostnaden för traditionell programvaruforskning, trots att mycket mer tillförlitlig information kan erhållas under verifiering.

I augusti 2012 NICTA, Rockwell Collins, Galois Inc , Boeing och University of Minnesota , som en del av ett program för att utveckla högst pålitliga militära cybersystem [37] organiserat av DARPA- byrån , har börjat utveckla ett obemannat flygfarkost [38] . Huvudkravet för utvecklingen är att säkerställa enhetens höga tillförlitlighet. Var och en av de listade företagen hade en roll att spela i programmet. NICTA ansvarade för utvecklingen av operativsystemet och byggde upp det kring seL4-mikrokärnan. Ansvarsfulla uppgifter implementerades som mikrokärnkomponenter, medan icke-ansvariga kördes under ett paravirtualiserat Linux OS. Utvecklingen av programmet var planerad att användas i NICTA Unmanned Little Bird-helikoptern, som utvecklades av Boeing. Helikoptern var tvungen att stödja både pilotkontroll och obemannat läge. I november 2015 rapporterades ett framgångsrikt genomförande [39] .

Annan forskning och utveckling

Hurd/L4 . I november 2000 skapades e-postlistan "l4-hurd" för att diskutera idén om att portera " GNU Hurd "-kärnan till L4-mikrokärnan. Portering genomfördes under 2002-2004, resultatet kallades "Hurd / L4". Implementeringen av "Hurd/L4" slutfördes inte. 2005 stoppades projektet [40] .

Osker  är ett operativsystem som implementerar L4 och skrevs i Haskell 2005 . Syftet med projektet: att testa möjligheten att implementera OS på ett funktionellt språk (och inte att studera mikrokärnan) [41] .

Codezero  är en implementering av L4-mikrokärnan för inbäddade system som blev allmänt tillgänglig sommaren 2009 [42] . Skapad av utvecklarna av det brittiska företaget "B Labs" från grunden. Koden skrevs i C. Implementeringen stöder ARM -arkitekturprocessorer , implementerar en första ordningens hypervisor och stöder Linux- och Android OS-virtualisering [43] [44] . Trots uttalandet om leverans av koden under GPL v3-licensen är det omöjligt att ladda ner koden från den officiella webbplatsen.

F9  är en implementering av L4-mikrokärnan som blev allmänt tillgänglig i juli 2013 [45] . Skrivet från grunden i C. Designad för inbyggda system. Stöder ARM-arkitektur Cortex-M- processorserien . Koden tillhandahålls under en BSD-licens.

Fiasco.OC  är en tredje generationens mikrokärna baserad på mikrokärnan "L4/Fiasco". Implementerar den kapacitetsbaserade säkerhetsmekanismen, stöder flerkärniga processorer och hårdvaruvirtualisering [46] .

L4 Runtime Environment (L4Re för kort) är ett ramverk som körs ovanpå mikrokärnan "Fiasco.OC" och är designat för att skapa komponenter för användarutrymme. L4Re tillhandahåller funktionalitet för att bygga klient-/serverapplikationer, implementera filsystem, implementera populära bibliotek som C-standardbiblioteket ("libc"), C++-standardbiblioteket ("libstdc++") och pthreads- biblioteket .

L4Re-ramverket och mikrokärnan "Fiasco.OC" stödde x86 (IA-32 och AMD64), ARM och PowerPC (WiP) arkitekturer.

L4Linux  är ett undersystem för att köra Linux OS ovanpå mikrokärnan "Fiasco.OC" med hjälp av paravirtualisering [47] . Tidigare användes istället för paret "Fiasco.OC" - L4Re, paret "L4 / Fiasco" - L4Env.

NOVA ( N  OVA O S v irtualiseringsarkitekturen ) är ett forskningsprojekt skapat för att skapa en säker och effektiv virtualiseringsmiljö [ 48 ] [49] [50] med en liten lista över betrodd programvara ( trusted computing base ) .  NOVA inkluderar:

NOVA-projektet stödde x86-processorer med flera kärnor. För att köras under kontroll av en mikrohypervisor (en hypervisor byggd på en mikrokärna) NOVA måste gästoperativsystemet stödja Intel VT-x eller AMD-V . Källkoden tillhandahölls under GPL v2-licensen.

Xameleon  är ett operativsystem baserat på L4-mikrokärnan [52] . Projektet grundades 2001 av den enda utvecklaren Alexei Mandrykin (född 19 januari 1973 ). OS byggdes ursprungligen ovanpå mikrokärnan " L4/Fiasco ". Senare migrerade författaren operativsystemet till " L4Ka::Pistachio " mikrokärnan. OS-källkoden är stängd.

WrmOS är ett realtidsoperativsystem med öppen källkod (RTOS) baserat på L4-mikrokärnan. WrmOS har sin egen implementering av kärnan, standardbibliotek och nätverksstacken. Processorarkitekturer som stöds är SPARC, ARM, x86, x86_64. WrmOS-kärnan är baserad på dokumentet L4 Kernel Reference Manual Version X.2 . Det finns en paravirtualiserad Linux-kärna ( w4linux ) som körs ovanpå WrmOS.

Anteckningar

  1. ↑ 1 2 Liedtke, Jochen (december 1993 ). "Förbättra IPC genom kärndesign" (PDF) . 14:e ACM- symposium om operativsystemsprinciper . Asheville , NC , USA . pp. 175-88. Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 4 mars 2016 på Wayback Machine
  2. ↑ L4 familj av mikrokärnor. Översikt Arkiverad 14 maj 2015 på Wayback Machine  (engelska) // Webbplats för Technical University of Dresden ( Tyskland ).
  3. ↑ ELAN Language Arkiverad 12 maj 2015 på Wayback Machine  // Technical University of Dresden webbplats .
  4. ↑ 1 2 3 4 5 6 7 8 9 10 Liedtke, Jochen (december 1993 ). "Ett beständigt system i verklig användning - upplevelser av de första 13 åren" (PDF) . Proceedings of the 3rd International Workshop on Object Orientation in Operating Systems (IWOOOS) . Asheville , NC , USA . pp. 2-11. Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 10 juli 2015 på Wayback Machine
  5. ↑ 1 2 In Memoriam Jochen Liedtke (1953-2001) Arkiverad 5 mars 2012 på Wayback Machine .
  6. ↑ 1 2 Liedtke, Jochen (december 1995 ). "Om µ-kärnkonstruktion" . Proc. 15:e ACM- symposium om operativsystemsprinciper (SOSP) . pp. 237-250. Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 18 mars 2009 på Wayback Machine
  7. ↑ 1 2 3 Systemarkitekturgrupp. om oss. människor. Liedtke . Arkiverad kopia .
  8. ↑ Jochen Liedtke. Sidtabellstrukturer för finkornigt virtuellt minne Arkiverad 12 november 2007 på Wayback Machine . Teknisk rapport 872. Tyska nationella forskningscentret för datavetenskap (GMD). oktober 1994 .
  9. ↑ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathan; Deller, Luke; Reuther, Lars ( 2000 ). "Sågverkets multiservermetod" . ACM SIGOPS European Workshop . Kolding , Danmark . pp. 109-114. Kontrollera datumet på |date=( hjälp på engelska )
  10. ↑ Fleisch, Brett D; Allan, Mark. Workplace Microkernel and OS: A Case  Study . — John Wiley & Sons, Ltd. Arkiverad från originalet den 24 augusti 2007.
  11. ↑ "L4Ka" gruppsida // archive.org .
  12. ↑ Drops översikt Arkiverad 7 augusti 2011 på Wayback Machine .
  13. ↑ Microkernel "L4Ka::Pistachio" Arkiverad 9 januari 2007 på Wayback Machine  .
  14. ↑ "L4Ka" utvecklingsteam Arkiverad 22 januari 2007 på Wayback Machine  .
  15. ↑ L4Ka::Pistachio-mikrokärnan . (engelska) Vitbok . PDF . 1 maj 2003 // archive.org .
  16. ↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (april 2005). Itanium-systemimplementatorns berättelse . USENIX årliga tekniska konferens . Annaheim , CA , USA . pp. 264-278. Föråldrad parameter använd |coauthors=( hjälp );Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 17 februari 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 . Drivrutiner på användarnivå: uppnådda prestanda  (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 (januari 2007). "Högpresterande mikrokärnor och virtualisering på ARM och segmenterade arkitekturer" . Första internationella workshop om mikrokärnor för inbyggda system . Sydney , Australien : NICTA . pp. 11-21 . Hämtad 2007-04-01 . Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 26 april 2007 på Wayback Machine
  19. ↑ Ruocco, Sergio. En realtidsprogrammerares rundtur i L4-mikrokärnor för allmänna ändamål //  EURASIP  Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications: journal. - 2008. - Oktober ( vol. 2008 ). - S. 1-14 . - doi : 10.1155/2008/234710 .  (inte tillgänglig länk)
  20. ↑ [1] Arkiverad 25 augusti 2006 på Wayback Machine .
  21. ↑ ERTOS- programsidan på NICTA-webbplatsen //archive.org .
  22. ↑ OKL4 3.0 (nedlänk) . Hämtad 21 maj 2011. Arkiverad från originalet 16 maj 2011. 
  23. ↑ OKL4 microvisor Arkiverad 13 mars 2014 på Wayback Machine .
  24. ↑ OK:Linux (nedlänk) . Hämtad 8 juli 2015. Arkiverad från originalet 10 april 2015. 
  25. ↑ Open Kernel Labs (19 januari 2012). Open Kernel Labs-programvaran överträffar milstolpen på 1,5 miljarder mobila enhetsförsändelser . Pressmeddelande . Hämtad 2015-11-10 .
  26. ↑ Öppna Kernel Labs ( 27 mars 2012 ). Open Kernel Labs Automotive Virtualization Vald av Bosch för infotainmentsystem . Pressmeddelande . Arkiverad från originalet den 2 juli 2012.
  27. ↑ iOS-säkerhet . Hämtad 28 september 2017. Arkiverad från originalet 23 september 2014.
  28. ↑ Darbat-projektet Arkiverat 19 december 2013 på Wayback Machine .
  29. ↑ [2] Arkiverad 15 juli 2015 på Wayback Machine .
  30. ↑ [3] Arkiverad 3 maj 2022 på Wayback Machine .
  31. ↑ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; kuk; David; Chakravarty, Manuel MT (september 2006 ). "Köra manualen: ett tillvägagångssätt för utveckling av mikrokärnor med hög säkerhet" (PDF) . ACM SIGPLAN Haskell Workshop . Portland , Oregon , USA . pp. 60-71. Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 3 mars 2016 på Wayback Machine
  32. ↑ 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronick, juni; kuk, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Touch, Harvey; Winwood, Simon (oktober 2009 ). "seL4: Formell verifiering av en OS-kärna" (PDF) . 22:a ACM- symposiet om operativsystemets principer . Big Sky , MT , USA . Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 28 juli 2011 på Wayback Machine
  33. ↑ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (april 2008 ). "Kärndesign för isolering och försäkran om fysiskt minne" . Första workshopen om isolering och integration i inbyggda system . Glasgow , Storbritannien . DOI : 10.1145/1435458 . Hämtad 2015-07-08 . Föråldrad parameter använd |coauthors=( hjälp );Kontrollera datumet på |date=( hjälp på engelska ) Arkiverad 24 april 2010 på Wayback Machine
  34. ↑ 1 2 Klein, Gerwin; Andronick, juni; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Omfattande formell verifiering av en OS-mikrokärna  (engelska)  // ACM Transactions on Computer Systems: journal. — Vol. 32 , nr. 1 . — S. 2:1-2:70 . - doi : 10.1145/2560537 .
  35. ↑ NICTA ( 29 juli 2014 ). Säkert operativsystem utvecklat av NICTA går med öppen källkod . Pressmeddelande . Arkiverad från originalet den 10 augusti 2014. Hämtad 2015-07-08 .
  36. ↑ Klein, Gerwin; Andronick, juni; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Omfattande formell verifiering av en OS-mikrokärna  (engelska)  // ACM Transactions on Computer Systems: journal. - 2014. - Vol. 32 . — S. 64 . - doi : 10.1145/2560537 .
  37. ↑ Militära cybersystem med hög säkerhet Arkiverad 8 augusti 2014. (HACM).
  38. ↑ SMACCM-projektet arkiverat 10 juli 2015 på Wayback Machine // NICTAs webbplats. SMACCM är en förkortning av engelskan.  säker matematiskt säkerställd sammansättning av styrmodeller .
  39. ↑ Ny generation drönare kan inte hackas Arkiverad 18 november 2015 på Wayback Machine // Popular Mechanics Magazine. 12 november 2015.
  40. ↑ Historia om GNU Hurd. Portering till en annan mikrokärna Arkiverad 8 mars 2017 på Wayback Machine  .
  41. ↑ Hallgren, T.; Jones, MP; Leslie, R.; Tolmach, A. Ett principiellt tillvägagångssätt för operativsystemkonstruktion i Haskell  //  Proceedings of the tenth ACM SIGPLAN international conference on functional programmering : journal. - 2005. - Vol. 40 , nej. 9 . - S. 116-128 . — ISSN 0362-1340 . - doi : 10.1145/1090189.1086380 .
  42. ↑ Codezero Arkiverad 9 juli 2015 på Wayback Machine på genode.org.
  43. ↑ dev.b-labs.com // archive.org .
  44. ↑ Officiell webbplats för Codezero-projektet Arkiverad 9 juli 2015 på Wayback Machine .
  45. ↑ F9-projektarkiv Arkiverad 5 mars 2017 på Wayback Machine // github.com .
  46. ↑ Peter, Michael; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (mars 2009 ). "Virtuella maskiner fängslade - Virtualisering i system med små betrodda datorbaser" . VTDS'09: Workshop om virtualiseringsteknik för pålitliga system . Nürnberg , Tyskland . Föråldrad parameter använd |coauthors=( hjälp );Kontrollera datumet på |date=( hjälp på engelska )
  47. ↑ L4Linux Arkiverad 7 juli 2015 på Wayback Machine .
  48. ↑ Steinberg, Udo; Bernhard, Kauer (april 2010 ). "NOVA: A Microhypervisor-Based Secure Virtualization Architecture". EuroSys '10: Proceedings of the 5th European Conference on Computer Systems . Paris , Frankrike . Kontrollera datumet på |date=( hjälp på engelska )
  49. ↑ Steinberg, Udo; Bernhard, Kauer (april 2010 ). "Mot en skalbar miljö med flera processorer på användarnivå". IIDS'10: Workshop om isolering och integration för pålitliga system . Paris , Frankrike . Kontrollera datumet på |date=( hjälp på engelska )
  50. ↑ Project Nova Arkiverad 24 juni 2015 på Wayback Machine . Officiell sida.
  51. ↑ VMM Seoul Arkiverad 11 juni 2018 på Wayback Machine // github.com
  52. ↑ l4os.ru Arkiverad 9 februari 2011 på Wayback Machine . Officiell webbplats för Xameleon-projektet.

Litteratur

Länkar