L4 (mikrokernel)

L4
Typ mikrokernel
Autor Jochen Liedtke
Vývojář Jochen Liedtke
Zapsáno v jazyk symbolických instrukcí
webová stránka l4hq.org

L4  je mikrojádro druhé generace vyvinuté Jochenem Liedtkem v roce 1993 [1] .

Architektura mikrokernelu L4 se osvědčila. Bylo vytvořeno mnoho implementací L4 microkernel ABI a API . Všechny implementace se staly známými jako rodina mikrojádrů L4. Liedtkeho implementace byla neformálně pojmenována „L4/x86“ [2] .

Historie

L1

V roce 1977 obhájil Jochen Liedtke svůj diplomový projekt z matematiky na univerzitě v Bielefeldu (Německo). V rámci projektu Liedtke napsal kompilátor pro jazyk ELAN ( angl. ). Jazyk ELAN vznikl v roce 1974 na základě jazyka Algol 68 pro výuku programování [3] . Liedtke nazval své dílo „L1“: písmeno „L“ je prvním písmenem autorova příjmení ( L iedtke ); číslo "1" je pořadové číslo díla.

L2

V roce 1977 Liedtke promoval jako matematik, zůstal na univerzitě v Bielefeldu a pustil se do vytváření běhového prostředí pro jazyk ELAN.

8bitové mikrokontroléry se staly široce dostupnými. Byl vyžadován operační systém, který by mohl běžet na malých pracovních stanicích na středních a vysokých školách. CP/M se nevešlo. Německé národní výzkumné centrum pro informatiku a technologii GMD a Univerzita v Bielefeldu se rozhodly vyvinout nový operační systém od nuly [4] .

V roce 1979 začal Jochen Liedtke vyvíjet nový operační systém a pojmenoval jej „ Eumel “ ( anglicky ) z angličtiny.  rozšiřitelný víceuživatelský mikroprocesorový systém EL AN . _ _ Operační systém "Eumel" byl také nazýván "L2", což znamená " L iedtkeho 2. dílo ". Nový operační systém podporoval 8bitové procesory Zilog Z80 , byl víceuživatelský a multitaskingový byl postaven na mikrojádru podporoval ortogonální persistenci Podpora ortogonální persistence byla následující: OS periodicky ukládal svůj stav na disk (obsah paměti , registry procesoru atd.); po výpadcích napájení byl OS obnoven z uloženého stavu; programy pokračovaly v práci, jako by k selhání nedošlo; byly ztraceny pouze změny provedené od posledního uložení. Eumel OS byl inspirován Multics OS a sdílel mnoho podobností s jádry Accent a Mach 4

Operační systém Eumel byl později portován na procesory Zilog Z8000 , Motorola 68000 a Intel 8086 . Tyto procesory byly 8bitové a 16bitové, neobsahovaly MMU a nepodporovaly mechanismus ochrany paměti . Eumel OS emuloval virtuální stroj s 32bitovým adresováním a MMU [4] . I přes použití emulace bylo možné k jedné pracovní stanici se systémem Eumel OS připojit až pět terminálů [4] .

Nejprve bylo možné psát programy pro Eumel OS pouze v jazyce ELAN. Kompilátory pro CDLPascal Basic a DYNAMO byly přidány později ale nebyly široce používány 4

Od roku 1980 se začalo používat Eumel OS, nejprve pro výuku programování a zpracování textu a poté pro komerční účely. Takže v polovině 80. let již Eumel OS běžel na více než 2000 počítačích v advokátních a dalších firmách [4] .

L3

S příchodem procesorů podporujících virtuální paměť (kvůli MMU) a mechanismů pro její ochranu zmizela nutnost emulovat virtuální stroj.

V roce 1984 [5] začal Jochen Liedtke pracovat ve výzkumném centru GMD, aby vytvořil operační systém podobný Eumelovu, ale bez emulace. GMD je v současnosti součástí Fraunhoferovy společnosti .

Od roku 1987 [4] Jochen Liedtke a jeho tým v SET Institute , součást GMD, začali vyvíjet nové mikrokernel nazvané "L3" ("L3" z " L iedtkeho 3. práce ").

Jochen Liedtke chtěl zjistit, zda je možné dosáhnout vysokého výkonu komponenty IPC výběrem správné architektury pro jádro a využitím vlastností hardwarové platformy při implementaci . Implementace mechanismu IPC se ukázala jako úspěšná (ve srovnání s komplexní implementací IPC v mikrokernelu Mach). Později byl implementován mechanismus pro izolaci oblastí paměti pro procesy běžící v uživatelském prostoru .

V roce 1988 byl vývoj dokončen a vydán stejnojmenný operační systém. Mikrojádro L3 bylo napsáno v jazyce symbolických instrukcí , využívalo vlastnosti procesorů architektury Intel x86 , nepodporovalo jiné platformy a výkonem překonalo Mach mikrokernel. L3 OS byl kompatibilní s Eumel OS: programy vytvořené pro Eumel OS běžely pod L3 OS, ale ne naopak [4] .

Komponenty mikrojádra L3:

Od roku 1989 [4] se OS používá:

L4

Při práci na mikrojádru L3 objevil Jochen Liedtke nedostatky v mikrojádru Mach. Ve snaze zlepšit výkon začal Liedtke kódovat nové mikrojádro v jazyce symbolických instrukcí pomocí funkcí architektury procesoru Intel i386 . Nové mikrojádro bylo nazváno „L4“ (z „ L iedtkeho 4. práce “).

V roce 1993 byla dokončena implementace mikrokernelu L4. Složka IPC se ukázala být 20krát rychlejší než IPC z mikrokernelu Mach [1] .

OS postavené na mikrojádrech první generace (zejména na mikrojádru Mach) se vyznačovaly nízkým výkonem. Kvůli tomu začali v polovině 90. let vývojáři přehodnocovat koncept mikrojaderné architektury. Zejména špatný výkon mikrojádra Mach byl vysvětlen přesunem komponenty zodpovědné za IPC do uživatelského prostoru.

Některé součásti Machova mikrojádra byly vráceny zpět - uvnitř mikrojádra . To porušilo samotnou myšlenku mikrokernelu (minimální velikost, izolace komponent), ale umožnilo zvýšit výkon operačního systému.

Výzkumníci hledali důvody špatného výkonu mikrojádra Mach a pečlivě analyzovali komponenty, které jsou důležité pro dobrý výkon. Analýza ukázala, že jádro přidělilo procesům příliš velkou pracovní sadu (hodně paměti), v důsledku čehož při přístupu jádra k paměti neustále docházelo k chybám mezipaměti [ 6 ] . Analýza umožnila formulovat nové pravidlo pro vývojáře mikrojádra - mikrokernel by měl být navržen tak, aby komponenty důležité pro zajištění vysokého výkonu byly umístěny v cache procesoru (nejlépe první úrovně ( English level 1 , L1 ) a je žádoucí že v mezipaměti ještě zbývá nějaké místo ).   

Kvůli prudkému nárůstu výkonu komponenty IPC nebyly stávající operační systémy schopny zvládnout zvýšený příliv zpráv IPC. Několik univerzit (např. Technical University Dresden , University of New South Wales ), institucí a organizací (např. IBM ) začalo vytvářet implementace L4 a kolem nich budovat nové operační systémy.

V roce 1996 Liedtke obhájil svou doktorandskou práci [7] na Technické univerzitě v Berlíně na téma „tabulky chráněných stránek“ [8] .

Od roku 1996 ve Výzkumném Watsona a jeho kolegové pokračovali ve výzkumu mikrojádra L4, mikrokernelu obecně a operačního systému Sawmill OS konkrétně [9] . Kvůli nedostatku komerčního úspěchu byl operační systém " IBM Workspace OS ", postavený na třetí verzi mikrojádra Mach od CMU a vyvíjený IBM od ledna 1991 do roku 1996 [10] , namísto konceptu " L4 microkernel" používal koncept "Lava Nucleus" nebo zkráceně "LN".

Postupem času byl kód mikrokernelu L4 uvolněn z vazby na platformu, zlepšily se bezpečnostní a izolační mechanismy.

V roce 1999 začal Liedtke pracovat jako profesor operačních systémů na Karlsruhe Institute of Technology (Německo) [7] .

Microkernel L4Ka::Lískový ořech

V roce 1999 byl Jochen Liedtke přijat do Systems Architecture Group (SAG), pracující v Karlsruhe Institute of Technology (Německo), a pokračoval ve výzkumu mikrojaderných operačních systémů. Skupina SAG je známá také jako skupina „L4Ka“.

Ve snaze dokázat, že mikrojádro lze implementovat v jazyce na vysoké úrovni , skupina SAG vyvinula mikrokernel „L4Ka::Lískový ořech“. Práce byly provedeny na Technologickém institutu v Karlsruhe za podpory DFG [11] . Implementace byla napsána v C++ a podporovala procesory architektury IA-32 a ARM . Výkon nového mikrojádra se ukázal jako přijatelný a vývoj jader v assembleru byl ukončen.

Microkernel L4/Fiasko

V roce 1998 začala skupina operačních systémů Technické univerzity v Drážďanech vyvíjet vlastní implementaci mikrojádra L4 s názvem „L4/Fiasco“. Vývoj probíhal v C++ souběžně s vývojem mikrojádra L4Ka::Lískový ořech.

V té době mikrojádro L4Ka::Hazelnut nepodporovalo souběžnost v kernel-space a mikrokernel "L4Ka::Pistachio" podporovalo pouze přerušení kernel-space ve specifických preempčních bodech. Vývojáři mikrokernelu „L4/Fiasco“ implementovali plný preemptivní multitasking (s výjimkou některých atomových operací). Díky tomu byla architektura jádra složitější, ale snížily se latence přerušení, což je důležité pro operační systém pracující v reálném čase.

Mikrokernel "L4/Fiasco" byl použit v OS "DROPS" [12]  - OS "tvrdého" reálného času (kdy je extrémně důležité, aby se na událost reagovalo v přísných časových rámcích), také vyvinutém na Technické univerzitě Drážďany.

Kvůli složitosti architektury mikrojádra v pozdějších verzích OS Fiasco se vývojáři vrátili k tradičnímu přístupu – spouštění jádra s vypnutými přerušeními (s výjimkou pár bodů preempce).

Nezávislost na platformě

Microkernel L4Ka::Pistácie

Implementace mikrojádra L4, vytvořené před vydáním mikrojádra L4Ka::Pistachio a pozdějších verzí mikrokernelu „Fiasco“, využívaly vlastnosti počítačové architektury (byly „svázány“ s architekturou procesoru). Bylo vyvinuto API nezávislé na architektuře. Navzdory přidání přenositelnosti poskytovalo API vysoký výkon. Myšlenky, které jsou základem architektury mikrokernelu, se nezměnily.

Počátkem roku 2001 bylo publikováno nové L4 API, velmi odlišné od předchozí verze L4 API s číslem verze 4 ("verze 4", také známé jako "verze X.2") a odlišné:

Po vydání nové verze API začal tým SAG vytvářet nové mikrokernel s názvem „L4Ka::Pistachio“ [13] [14] . Kód byl zkompilován od nuly v C++ s využitím zkušeností z projektu L4Ka::Hazelnut. Pozornost byla věnována vysokému výkonu a přenosnosti.

10. června 2001 zemřel Dr. Jochen Liedtke [7] při autonehodě. Poté se tempo vývoje projektu výrazně snížilo.

V roce 2003 [15] bylo dílo dokončeno díky úsilí Liedtkeho studentů: Volkmara Uhliga, Uwe Dannowského a Espena Skoglunda. Zdrojový kód byl vydán pod licencí 2-klauzule BSD .

Nové verze Fiaska

Souběžně s tím pokračoval vývoj mikrojádra L4/Fiasco. Byla přidána podpora pro více hardwarových platforem ( x86 , AMD64 , ARM ). Je pozoruhodné, že verze Fiasco s názvem „FiascoUX“ by mohla běžet v uživatelském prostoru s operačním systémem Linux .

Vývojáři mikrojádra L4/Fiasco implementovali několik rozšíření L4v2 API.

Mikrokernel „Fiasko“ navíc poskytoval mechanismy správy komunikačních práv. Stejné mechanismy existovaly pro správu zdrojů spotřebovaných jádrem.

Byl vyvinut "L4Env", sada komponent běžících na mikrokernelu "Fiasco" v uživatelském prostoru. "L4Env" byl použit v "L4Linux", implementaci paravirtualizace (virtualizace ABI) pro linuxová jádra verze 2.6.x.

University of New South Wales a NICTA

Vývojáři z University of New South Wales vytvořili mikrojádra L4/MIPS a L4/Alpha, implementace L4 pro 64bitové procesory MIPS a DEC Alpha . Původní mikrokernel L4 podporoval pouze procesory architektury x86 a stal se neformálně známým jako „L4/x86“. Implementace byly napsány od nuly v jazyce C a assembleru a nebyly přenosné. Po vydání mikrojádra L4Ka::Pistachio nezávislého na platformě skupina UNSW přestala vyvíjet svá mikrojádra a začala portovat mikrokernel L4Ka::Pistachio. Implementace mechanismu předávání zpráv se ukázala být rychlejší než jiné implementace (36 cyklů na procesorech architektury Itanium ) [16] .

Skupina UNSW ukázala, že ovladač v uživatelském prostoru lze spustit stejným způsobem jako ovladač v prostoru jádra [17] .

Vyvinula komponenty pro paravirtualizaci linuxových jader. Komponenty běžely na vrcholu mikrojádra L4. Výsledek byl nazván " Wombat OS ". Wombat OS mohl běžet na architekturách x86, ARM a MIPS. Na procesorech Intel XScale prováděl Wombat OS přepínání kontextu 30krát pomaleji než monolitické jádro Linuxu [18] .

Skupina UNSW se poté přestěhovala do NICTA, vytvořila vidlici mikrojádra L4Ka::Pistachio a pojmenovala ji „NICTA::L4-embedded“. Nové mikrokernel bylo napsáno pro komerční vestavěné systémy , vyžadovalo málo paměti a implementovalo zjednodušené L4 API. Se zjednodušeným API byla systémová volání prováděna tak „krátká“, že nevyžadovala body preemptivního multitaskingu a umožňovala implementaci OS v reálném čase [19] .

Komerční využití

Qualcomm provozoval implementaci mikrokernelu L4 od NICTA na čipové sadě zvané „Mobilní stanice Modem“ (MSM) Toto bylo hlášeno v listopadu 2005 [20] zástupci NICTA a na konci roku 2006 se začaly prodávat čipové sady MSM. Implementace mikrokernelu L4 tedy skončila v mobilních telefonech .

V srpnu 2006 Heiser Open Kernel Labs V té době Heiser sloužil jako vedoucí programu ERTOS organizovaného NICTA [21] a byl profesorem na UNSW. OK Labs byl vytvořen pro

V dubnu 2008 byla vydána verze 2.1 mikrokernelu „OKL4“, první veřejná implementace L4, která má zabezpečení založené na schopnostech . V říjnu 2008 byla vydána verze 3.0 [22] - nejnovější open source  verze "OKL4" . Zdrojový kód pro následující verze byl uzavřen. Vrstva mikrojádra, která pohání hypervizor , byla přepsána tak, aby přidala podporu pro nativní hypervizor nazvaný "OKL4 mikrovizor" [23] .

Společnost OK Labs distribuovala paravirtualizovaný operační systém Linux s  názvem OK :Linux [24] . OK : Linux byl potomkem Wombat OS . OK Labs také distribuovala paravirtualizované verze operačních systémů Symbian a Android .

OK Labs získala práva na mikrokernel seL4 od NICTA.

Na začátku roku 2012 bylo prodáno více než 1,5 miliardy zařízení vybavených implementací mikrojádra L4 [25] . Většina těchto zařízení obsahovala čipy, které implementují bezdrátové modemy a byly vydány společností Qualcomm .

Implementace L4 byla také použita v automobilových zábavních systémech [26] .

OS, postavený na bázi implementace L4, byl provozován bezpečným enklávovým procesorem, který je součástí elektronického obvodu Apple A7 umístěného na čipu [27] . Stejná implementace L4 byla použita v projektu Darbat společnosti NICTA [28] . Zařízení obsahující Apple A7 dodávaná s iOS . V roce 2015 existovalo přibližně 310 milionů iOS zařízení [29] .

Ověření

seL4

V roce 2006 začal vývoj třetí generace mikrojádra , nazvaného „seL4“ [30] . Vývoj začal od nuly skupinou programátorů z NICTA. Účel: vytvořit základ pro budování bezpečných a spolehlivých systémů, které dokážou splnit moderní bezpečnostní požadavky, jak je psáno např. v dokumentu „Obecná kritéria pro hodnocení bezpečnosti informačních technologií“. Kód mikrokernelu byl od samého počátku psán tak, aby jej bylo možné ověřit (kontrola správnosti). Ověření bylo provedeno pomocí jazyka Haskell : požadavky na mikrokernel (specifikace) byly napsány v jazyce Haskell; objekty mikrojádra byly reprezentovány jako objekty Haskell; práce se zařízením byla emulována [31] . Aby bylo možné získat informace o dostupnosti objektu provedením formálního uvažování, použil seL4 řízení přístupu založené na zabezpečení založeném na schopnostech.

V roce 2009 byl dokončen důkaz správnosti kódu mikrokernelu seL4 [32] . Existence důkazu zajistila shodu mezi implementací a specifikací, potvrdila nepřítomnost některých chyb v implementaci (například absence uváznutí , livelock , přetečení bufferu , aritmetické výjimky a případy použití neinicializovaných proměnných). Mikrojádro seL4 bylo první mikrojádro navržené pro obecný operační systém a ověřené [32] .

Mikrokernel seL4 implementoval nestandardní správu zdrojů jádra [33] :

Něco podobného bylo implementováno v experimentálním OS Barrelfish . Díky tomuto přístupu ke správě zdrojů jádra bylo možné provádět úvahy o izolaci vlastností a později bylo prokázáno, že mikrokernel seL4 zajišťuje integritu a důvěrnost vlastností [34] . Důkaz byl proveden pro původní kód.

Tým výzkumníků z firmy NICTA prokázal správnost překladu textu z jazyka C do strojového kódu. To umožnilo vyloučit kompilátor ze seznamu důvěryhodného softwaru a považovat důkaz provedený pro zdrojový kód mikrojádra za platný i pro spustitelný soubor mikrojádra.

Mikrojádro seL4 se stalo prvním jádrem s chráněným režimem, u kterého byla v plném rozsahu provedena analýza doby provádění v nejhorším případě a výsledky této analýzy byly publikovány. Výsledky analýzy jsou nezbytné pro použití mikrokernelu v hard real-time OS [34] .

29. července 2014 NICTA a General Dynamics C4 Systemsoznámila vydání mikrojádra seL4 (včetně všech důkazů o jejich správnosti) pod otevřenými licencemi [35] . Zdrojový kód mikrojádra a důkazy byly vydány pod licencí GPL v2. Většina knihoven a nástrojů byla distribuována pod licencí 2-klauzule BSD.

Zajímavým tvrzením výzkumníků [36] je, že náklady na provedení softwarové verifikace jsou nižší než náklady na tradiční softwarový výzkum, a to i přes to, že při ověřování lze získat mnohem spolehlivější informace.

V srpnu 2012 NICTA, Rockwell Collins, Galois Inc , Boeing a University of Minnesota v rámci programu vývoje vysoce spolehlivých vojenských kybernetických systémů [37] organizovaného agenturou DARPA zahájily vývoj bezpilotního vzdušného prostředku [38] . Hlavním požadavkem pro vývoj je zajištění vysoké spolehlivosti zařízení. Každá z uvedených firem měla v programu svou roli. NICTA byla zodpovědná za vývoj operačního systému a postavila jej kolem mikrojádra seL4. Odpovědné úlohy byly implementovány jako komponenty mikrojádra, zatímco nezodpovědné úlohy byly provozovány pod paravirtualizovaným OS Linux. Vývoj programu byl plánován pro použití ve vrtulníku NICTA Unmanned Little Bird, který vyvinula společnost Boeing. Vrtulník musel podporovat jak pilotní řízení, tak bezpilotní režim. V listopadu 2015 byla hlášena úspěšná implementace [39] .

Ostatní výzkum a vývoj

Hurd/L4 . V listopadu 2000 byl vytvořen e-mailový seznam „l4-hurd“, aby diskutoval o myšlence portovat jádro „ GNU Hurd “ na mikrokernel L4. Portování bylo provedeno v letech 2002-2004, výsledek byl nazván "Hurd / L4". Implementace "Hurd/L4" nebyla dokončena. V roce 2005 byl projekt zastaven [40] .

Osker  je operační systém , který implementuje L4 a byl napsán v Haskell v roce 2005 . Účel projektu: otestovat možnost implementace OS ve funkcionálním jazyce (a ne studovat mikrokernel) [41] .

Codezero  je implementace mikrokernelu L4 pro vestavěné systémy, který se stal veřejně dostupným v létě 2009 [42] . Vytvořeno vývojáři britské společnosti "B Labs" od nuly. Kód byl napsán v C. Implementace podporuje procesory architektury ARM , implementuje hypervizor prvního řádu a podporuje virtualizaci OS Linux a Android [43] [44] . Přes prohlášení o dodání kódu pod licencí GPL v3 není možné stáhnout kód z oficiálních stránek.

F9  je implementace mikrokernelu L4, který se stal veřejně dostupným v červenci 2013 [45] . Napsáno od začátku v C. Navrženo pro vestavěné systémy. Podporuje architekturu ARM řady procesorů Cortex-M . Kód je dodáván pod licencí BSD.

Fiasco.OC  je mikrokernel třetí generace založený na mikrojádru „L4/Fiasco“. Implementuje bezpečnostní mechanismus založený na schopnostech, podporuje vícejádrové procesory a hardwarovou virtualizaci [46] .

L4 Runtime Environment (zkráceně L4Re) je framework, který běží nad mikrokernelem „Fiasco.OC“ a je navržen tak, aby vytvářel komponenty uživatelského prostoru. L4Re poskytuje funkce pro vytváření aplikací klient/server, implementaci souborových systémů, implementaci populárních knihoven, jako je standardní knihovna C ("libc"), standardní knihovna C++ ("libstdc++") a knihovna pthreads .

Rámec L4Re a mikrokernel „Fiasco.OC“ podporovaly architektury x86 (IA-32 a AMD64), ARM a PowerPC (WiP).

L4Linux  je subsystém pro provoz operačního systému Linux nad mikrokernelem "Fiasco.OC" pomocí paravirtualizace [47] . Dříve se místo dvojice "Fiasco.OC" - L4Re používala dvojice "L4 / Fiasco" - L4Env.

NOVA ( N OVA O S virtualization a rchitecture ) je výzkumný  projekt vytvořený za účelem vytvoření bezpečného a efektivního virtualizačního prostředí [48] [49] [50] s malým seznamem důvěryhodného softwaru ( trusted computing base ) . NOVA zahrnuje:  

Projekt NOVA podporoval vícejádrové x86 procesory. Aby hostující OS běžel pod kontrolou mikro-hypervizoru (hypervizoru postaveného na mikrojádru) NOVA, musí podporovat Intel VT-x nebo AMD-V . Zdrojový kód byl dodán pod licencí GPL v2.

Xameleon  je operační systém založený na mikrojádru L4 [52] . Projekt byl založen v roce 2001 jediným vývojářem Alexejem Mandrykinem (narozen 19. ledna 1973 ). OS byl původně postaven na mikrokernelu „ L4/Fiasco “. Později autor migroval OS na mikrokernel " L4Ka::Pistachio ". Zdrojový kód OS je uzavřen.

WrmOS je open source operační systém pracující v reálném čase (RTOS) založený na mikrojádru L4. WrmOS má vlastní implementaci jádra, standardní knihovny a síťový zásobník. Podporované architektury procesorů jsou SPARC, ARM, x86, x86_64. Jádro WrmOS je založeno na dokumentu L4 Kernel Reference Manual verze X.2 . Nad WrmOS běží paravirtualizované linuxové jádro ( w4linux ).

Poznámky

  1. ↑ 1 2 Liedtke, Jochen (prosinec 1993 ). „Zlepšení IPC pomocí návrhu jádra“ (PDF) . 14. sympozium ACM o principech operačního systému . Asheville , NC , USA . str. 175-88. Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 4. března 2016 na Wayback Machine
  2. ↑ Rodina mikrojader L4. Přehled Archivováno 14. května 2015 na Wayback Machine  (anglicky) // Webové stránky Technické univerzity v Drážďanech ( Německo ).
  3. ↑ Jazyk ELAN archivován 12. května 2015 na webu Wayback Machine  // webové stránky Technické univerzity v Drážďanech .
  4. ↑ 1 2 3 4 5 6 7 8 9 10 Liedtke, Jochen (prosinec 1993 ). „Trvalý systém v reálném provozu – zkušenosti z prvních 13 let“ (PDF) . Sborník příspěvků z 3. mezinárodního workshopu o objektové orientaci v operačních systémech (IWOOOS) . Asheville , NC , USA . str. 2-11. Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 10. července 2015 na Wayback Machine
  5. ↑ 1 2 In Memoriam Jochen Liedtke (1953-2001) Archivováno 5. března 2012 na Wayback Machine .
  6. ↑ 1 2 Liedtke, Jochen (prosinec 1995 ). „O konstrukci µ-kernelu“ . Proč. 15. sympozium ACM o principech operačních systémů (SOSP) . str. 237-250. Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 18. března 2009 na Wayback Machine
  7. ↑ 1 2 3 Skupina architektury systému. o nás. lidé. Liedtke . Archivovaná kopie .
  8. ↑ Jochen Liedtke. Struktury tabulek stránek pro jemnozrnnou virtuální paměť Archivováno 12. listopadu 2007 na Wayback Machine . Technická zpráva 872. Německé národní výzkumné centrum pro informatiku (GMD). října 1994 .
  9. ↑ Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars ( 2000 ). "Multiserverový přístup Sawmill" . Evropský workshop ACM SIGOPS . Kolding , Dánsko . str. 109-114. Zkontrolujte datum na |date=( nápověda v angličtině )
  10. ↑ Fleisch, Brett D; Allane, Marku. Workplace Microkernel and OS: Případová  studie . — John Wiley & Sons, Ltd. Archivováno z originálu 24. srpna 2007.
  11. ↑ Stránka skupiny "L4Ka" // archive.org .
  12. ↑ Přehled kapek Archivováno 7. srpna 2011 na Wayback Machine .
  13. ↑ Mikrokernel "L4Ka::Pistachio" Archivováno 9. ledna 2007 na Wayback Machine  .
  14. ↑ Vývojový tým "L4Ka" Archivováno 22. ledna 2007 na Wayback Machine  .
  15. ↑ Mikrojádro L4Ka::Pistácie . (anglicky) Bílá kniha . PDF . 1. května 2003 // archive.org .
  16. ↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (duben 2005). Itanium - příběh implementátora systému . Výroční technická konference USENIX . Annaheim , CA , USA . str. 264-278. Použitý zastaralý parametr |coauthors=( help );Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 17. února 2007 na Wayback Machine
  17. ↑ Leslie, Ben; Chubb, Peter; FitzRoy-Dale, Nicholas; Gotz, Stefan; Grey, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot . Ovladače zařízení na uživatelské úrovni: dosažený výkon  (neopr.)  // Journal of Computer Science and Technology. - T. 20 , č. 5 . — S. 654-664 . - doi : 10.1007/s11390-005-0654-4 .
  18. ↑ van Schaik, Carl; Heiser, Gernot (leden 2007). „Vysoce výkonná mikrojádra a virtualizace na ARM a segmentovaných architekturách“ . 1. mezinárodní seminář o mikrojádrech pro vestavěné systémy . Sydney , Austrálie : NICTA . str. 11-21 . Získáno 2007-04-01 . Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 26. dubna 2007 na Wayback Machine
  19. ↑ Ruocco, Sergio. Programátorská prohlídka v reálném čase po univerzálních mikrojádrech L4 //  EURASIP  Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications: journal. - 2008. - Říjen ( roč. 2008 ). - str. 1-14 . - doi : 10.1155/2008/234710 .  (nedostupný odkaz)
  20. ↑ [1] Archivováno 25. srpna 2006 na Wayback Machine .
  21. ↑ Stránka programu ERTOS na webu NICTA // archive.org .
  22. ↑ OKL4 3.0 (downlink) . Získáno 21. května 2011. Archivováno z originálu 16. května 2011. 
  23. ↑ Mikrovizor OKL4 Archivováno 13. března 2014 na Wayback Machine .
  24. ↑ OK:Linux (downlink) . Získáno 8. července 2015. Archivováno z originálu 10. dubna 2015. 
  25. ↑ Otevřete Kernel Labs (19. ledna 2012). Software Open Kernel Labs překonává milník 1,5 miliardy zásilek mobilních zařízení . Tisková zpráva . Staženo 2015-11-10 .
  26. ↑ Otevřete Kernel Labs ( 27. března 2012 ). Open Kernel Labs Automotive Virtualization Selected Bosch for Infotainment Systems . Tisková zpráva . Archivováno z originálu 2. července 2012.
  27. ↑ Zabezpečení iOS . Získáno 28. září 2017. Archivováno z originálu 23. září 2014.
  28. ↑ Projekt Darbat Archivováno 19. prosince 2013 na Wayback Machine .
  29. ↑ [2] Archivováno 15. července 2015 na Wayback Machine .
  30. ↑ [3] Archivováno 3. května 2022 na Wayback Machine .
  31. ↑ Derrin, Philip; Elphinstone, Kevin; Klein, Gerwin; kohout; David; Chakravarty, Manuel MT (září 2006 ). „Spuštění příručky: přístup k vývoji mikrokernelu s vysokou jistotou“ (PDF) . Workshop ACM SIGPLAN Haskell . Portland , Oregon , USA . str. 60-71. Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 3. března 2016 na Wayback Machine
  32. ↑ 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronick, červen; Kohout, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Dotkni se, Harvey; Winwood, Simon (říjen 2009 ). “seL4: Formální ověření jádra OS” (PDF) . 22. sympozium ACM o principech operačního systému . Big Sky , MT , USA . Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 28. července 2011 na Wayback Machine
  33. ↑ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (duben 2008 ). „Design jádra pro izolaci a zajištění fyzické paměti“ . 1. workshop o izolaci a integraci ve vestavěných systémech . Glasgow , Spojené království . DOI : 10.1145/1435458 . Staženo 2015-07-08 . Použitý zastaralý parametr |coauthors=( help );Zkontrolujte datum na |date=( nápověda v angličtině ) Archivováno 24. dubna 2010 na Wayback Machine
  34. ↑ 1 2 Klein, Gerwin; Andronick, červen; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Komplexní formální ověření mikrokernelu OS  (anglicky)  // ACM Transactions on Computer Systems: journal. — Sv. 32 , č. 1 . — P. 2:1–2:70 . - doi : 10.1145/2560537 .
  35. ↑ NICTA ( 29. července 2014 ). Bezpečný operační systém vyvinutý společností NICTA je otevřený . Tisková zpráva . Archivováno z originálu 10. srpna 2014. Staženo 2015-07-08 .
  36. ↑ Klein, Gerwin; Andronick, červen; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Komplexní formální ověření mikrokernelu OS  (anglicky)  // ACM Transactions on Computer Systems: journal. - 2014. - Sv. 32 . — S. 64 . - doi : 10.1145/2560537 .
  37. ↑ Kybernetické vojenské systémy s vysokým zabezpečením Archivováno 8. srpna 2014. (HACM).
  38. ↑ Projekt SMACCM archivován 10. července 2015 na webu Wayback Machine // NICTA. SMACCM je zkratka z angličtiny.  bezpečné matematicky zajištěné složení řídicích modelů .
  39. ↑ Drony nové generace nelze hacknout Archivováno 18. listopadu 2015 na Wayback Machine // Popular Mechanics Magazine. 12. listopadu 2015.
  40. ↑ Historie GNU Hurd. Portování na jiný mikrokernel Archivováno 8. března 2017 na Wayback Machine  .
  41. ↑ Hallgren, T.; Jones, poslanec; Leslie, R.; Tolmach, A. Principiální přístup ke konstrukci operačního systému v Haskellu  //  Sborník z desáté mezinárodní konference ACM SIGPLAN o funkcionálním programování: časopis. - 2005. - Sv. 40 , č. 9 . - str. 116-128 . — ISSN 0362-1340 . - doi : 10.1145/1090189.1086380 .
  42. ↑ Codezero Archivováno 9. července 2015 na Wayback Machine na genode.org.
  43. ↑ dev.b-labs.com // archive.org .
  44. ↑ Oficiální stránky projektu Codezero Archived 9. července 2015 na Wayback Machine .
  45. ↑ Repozitář projektu F9 Archivováno 5. března 2017 na Wayback Machine // github.com .
  46. ↑ Petr, Michael; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (březen 2009 ). „Virtuální stroje uvězněny – virtualizace v systémech s malými důvěryhodnými výpočetními základnami“ . VTDS'09: Workshop o virtualizační technologii pro spolehlivé systémy . Norimberk , Německo . Použitý zastaralý parametr |coauthors=( help );Zkontrolujte datum na |date=( nápověda v angličtině )
  47. ↑ L4Linux Archivováno 7. července 2015 na Wayback Machine .
  48. ↑ Steinberg, Udo; Bernhard, Kauer (duben 2010 ). „NOVA: Bezpečná virtualizační architektura založená na mikrohypervisoru“ . EuroSys '10: Sborník příspěvků z 5. evropské konference o počítačových systémech . Paříž , Francie . Zkontrolujte datum na |date=( nápověda v angličtině )
  49. ↑ Steinberg, Udo; Bernhard, Kauer (duben 2010 ). „Směrem ke škálovatelnému víceprocesorovému prostředí na uživatelské úrovni“. IIDS'10: Workshop o izolaci a integraci pro spolehlivé systémy . Paříž , Francie . Zkontrolujte datum na |date=( nápověda v angličtině )
  50. ↑ Projekt Nova archivován 24. června 2015 na Wayback Machine . Oficiální stránka.
  51. ↑ VMM Seoul archivováno 11. června 2018 na Wayback Machine // github.com
  52. ↑ l4os.ru Archivováno 9. února 2011 na Wayback Machine . Oficiální stránky projektu Xameleon.

Literatura

Odkazy