L4 (mikromag)

L4
Típusú mikrokernel
Szerző Jochen Liedtke
Fejlesztő Jochen Liedtke
Beírva Assembly nyelv
Weboldal l4hq.org

Az L4  egy második generációs mikrokernel , amelyet Jochen Liedtke fejlesztett ki 1993 -ban [1] .

Az L4 mikrokernel architektúra sikeresnek bizonyult. Az L4 mikrokernel ABI és API számos implementációja készült. Az összes implementáció a mikrokernelek L4 családjaként vált ismertté. A Liedtke megvalósításának hivatalos neve "L4/x86" [2] .

Történelem

L1

1977 -ben Jochen Liedtke a Bielefeldi Egyetemen (Németország) védte meg matematika diplomáját . A projekt részeként Liedtke írt egy fordítót az ELAN nyelvhez ( eng. ). Az ELAN nyelvet 1974 -ben hozták létre az Algol 68 programozási nyelv alapján [3] . Liedtke "L1"-nek nevezte művét: az "L" betű a szerző vezetéknevének első betűje ( L iedtke ); az „1” szám a mű sorszáma.

L2

1977-ben Liedtke matematikus diplomát szerzett, a Bielefeldi Egyetemen maradt, és hozzálátott egy futási környezet létrehozásához az ELAN nyelv számára.

A 8 bites mikrokontrollerek széles körben elérhetővé váltak. Olyan operációs rendszerre volt szükség, amely a középiskolák és egyetemek kis munkaállomásain is futhat. A CP/M nem illett. A Német Nemzeti Számítástudományi és Technológiai Kutatóközpont, a GMD és a Bielefeldi Egyetem úgy döntött, hogy a semmiből új operációs rendszert fejlesztenek ki [4] .

1979 -ben Jochen Liedtke új operációs rendszert kezdett fejleszteni, és angolul " Eumel "-nek ( angolul ) nevezte el .  Bővíthető több u ser m mikroprocesszoros EL AN-rendszer . Az "Eumel" operációs rendszert "L2-nek" is hívták, ami azt jelenti, hogy " L iedtke 2. munkája ". Az új operációs rendszer a 8 bites Zilog Z80 processzorokat támogatta , többfelhasználós és többfeladatos volt mikrokernelre épült és támogatta az ortogonális perzisztenciát Az ortogonális perzisztencia támogatása a következő volt: az operációs rendszer időszakonként lemezre mentette állapotát ( memória tartalma , processzorregiszterek stb.); áramkimaradások után az operációs rendszert visszaállították a mentett állapotból; a programok továbbra is úgy működtek, mintha a hiba meg sem történt volna; csak az utolsó mentés óta végrehajtott módosítások vesztek el. Az Eumel operációs rendszert a Multics OS ihlette, és sok hasonlóságot mutatott az Accent és a Mach 4kernelekkel

Az Eumel operációs rendszert később a Zilog Z8000 , Motorola 68000 és Intel 8086 processzorokra portolták át . Ezek a processzorok 8 és 16 bitesek voltak, nem tartalmaztak MMU -t , és nem támogattak memóriavédelmi mechanizmust . Az Eumel OS egy virtuális gépet emulált 32 bites címzéssel és MMU-val [4] . Az emuláció használata ellenére egy Eumel OS-t futtató munkaállomáshoz akár öt terminál is csatlakoztatható [4] .

Eleinte csak ELAN nyelven lehetett programokat írni az Eumel OS-hez. A CDLPascal Basic és DYNAMO fordítóprogramokat később adták hozzá de ezeket nem használták széles körben 4

1980 óta kezdték használni az Eumel OS-t, először programozás és szövegszerkesztés oktatására, majd kereskedelmi célokra. Így az 1980-as évek közepén az Eumel OS már több mint 2000 számítógépen futott ügyvédi irodákban és más cégeknél [4] .

L3

A virtuális memóriát támogató processzorok (az MMU-nak köszönhetően) és a védelmi mechanizmusok megjelenésével megszűnt a virtuális gép emulációjának szükségessége.

1984- ben [5] Jochen Liedtke a GMD kutatóközpontba ment, hogy létrehozzon egy, az Eumeléhez hasonló operációs rendszert, de emuláció nélkül. A GMD jelenleg a Fraunhofer Társaság tagja .

1987 óta [4] Jochen Liedtke és csapata a SET Institute -ban, amely a GMD része, egy új mikrokernel fejlesztésébe kezdett, az "L3"-nak ("L3" a " L iedtke 3. művéből ").

Jochen Liedtke azt akarta látni, hogy lehetséges-e az IPC komponens nagy teljesítménye a kernelhez megfelelő architektúra kiválasztásával és a hardverplatform jellemzőinek felhasználásával a megvalósításban . Az IPC mechanizmus megvalósítása sikeresnek bizonyult (az IPC Mach mikrokernelben való komplex megvalósításához képest). Később egy mechanizmust vezettek be a memóriaterületek elkülönítésére a felhasználói térben futó folyamatok számára .

1988- ban a fejlesztés befejeződött, és megjelent az azonos nevű operációs rendszer. Az L3 mikrokernel assembly nyelven íródott, az Intel x86 architektúrájú processzorainak szolgáltatásait használta , nem támogatott más platformokat, teljesítményben pedig felülmúlta a Mach mikrokernelt. Az L3 OS kompatibilis volt az Eumel OS-szel: az Eumel OS-hez készített programok futottak L3 OS alatt, de fordítva nem [4] .

L3 mikrokernel összetevők:

1989 óta [4] az operációs rendszert használják:

L4

Miközben az L3 mikrokernelen dolgozott, Jochen Liedtke hibákat fedezett fel a Mach mikrokernelben. A teljesítmény javítása érdekében a Liedtke elkezdte az új mikrokernelt assembly nyelven kódolni az Intel i386 processzorarchitektúra szolgáltatásaival . Az új mikrokernelt "L4"-nek hívták (" L iedtke 4. művéből ").

1993-ban befejeződött az L4 mikrokernel megvalósítása. Az IPC komponens 20-szor gyorsabbnak bizonyult, mint a Mach mikrokernelből származó IPC [1] .

Az első generációs mikrokernelekre (különösen a Mach mikrokernelekre) épülő operációs rendszereket alacsony teljesítmény jellemezte. Emiatt az 1990-es évek közepén a fejlesztők elkezdték újragondolni a mikronukleáris architektúra koncepcióját. A Mach mikrokernel gyenge teljesítményét különösen azzal magyarázták, hogy az IPC-ért felelős komponenst a felhasználói térbe helyezték át.

A Mach mikrokernel egyes komponensei visszakerültek – a mikrokernel belsejébe . Ez megsértette a mikrokernelek gondolatát (minimális méret, az összetevők elkülönítése), de lehetővé tette az operációs rendszer teljesítményének növelését.

A kutatók keresték a Mach mikrokernel gyenge teljesítményének okait, és alaposan elemezték a jó teljesítményhez fontos összetevőket. Az elemzés kimutatta, hogy a kernel túl nagy munkahalmazt (sok memóriát) foglalt le a folyamatokhoz, aminek következtében a kernel memóriához való hozzáférése során folyamatosan gyorsítótár - kihagyások léptek fel [ 6 ] . Az elemzés lehetővé tette egy új szabály megfogalmazását a mikrokernel fejlesztők számára - a mikrokernelt úgy kell megtervezni, hogy a nagy teljesítmény biztosításához fontos komponensek a processzor gyorsítótárában (lehetőleg az első szint ( angol nyelv 1 , L1) kerüljenek, és ez kívánatos. hogy van még szabad hely a gyorsítótárban ).   

Az IPC komponens teljesítményének kiugrása miatt a meglévő operációs rendszerek nem tudták kezelni az IPC üzenetek megnövekedett beáramlását. Számos egyetem (pl. Dresdeni Műszaki Egyetem , Új-Dél-Walesi Egyetem ), intézmény és szervezet (pl. IBM ) megkezdte az L4 implementációinak létrehozását és új operációs rendszerek kiépítését köréjük.

Liedtke 1996- ban védte meg PhD disszertációját [7] a Berlini Műszaki Egyetemen "védett oldaltáblázatok" [8] témában .

1996 óta Watson Research Centerben és munkatársai folytatják az L4 mikrokernel, általában a mikrokernelek és különösen a Sawmill OS operációs rendszer kutatását [9] . A kereskedelmi siker hiánya miatt az " IBM Workspace OS " operációs rendszer, amely a CMU Mach mikrokernelének harmadik verziójára épült, és amelyet az IBM fejlesztett ki 1991 januárja és 1996 között [10] , a " koncepció helyett " Az L4 mikrokernel a "lávamag" vagy röviden "LN" fogalmát használta.

Idővel az L4 mikrokernel kódot felszabadították a platformhoz való kötődés alól, a biztonsági és elkülönítési mechanizmusok javultak.

1999 -ben Liedtke az operációs rendszerek professzoraként kezdett dolgozni a Karlsruhei Technológiai Intézetben (Németország) [7] .

Mikrokernel L4Ka::Mogyoró

1999-ben Jochen Liedtke felvételt nyert a Systems Architecture Groupba (SAG, a Karlsruhe Institute of Technology (Németország) munkatársa, és folytatta a mikronukleáris operációs rendszerek kutatását. A SAG csoportot "L4Ka" csoportnak is nevezik.

Az SAG csoport kifejlesztette az "L4Ka::Hazelnut" mikrokernelt , hogy be akarja bizonyítani, hogy egy mikrokernel megvalósítható magas szintű nyelven . A munkát a Karlsruhei Technológiai Intézetben végezték a DFG [11] támogatásával . A megvalósítás C++ nyelven íródott, és támogatott IA-32 és ARM architektúra processzorokat . Az új mikrokernel teljesítménye elfogadhatónak bizonyult, az assembly nyelvű kernelek fejlesztése leállt.

Microkernel L4/Fiasco

1998- ban a Drezdai Műszaki Egyetem Operációs Rendszerek Csoportja megkezdte az L4 mikrokernel saját megvalósításának fejlesztését, amelyet "L4/Fiasco"-nak neveztek el. A fejlesztés C++ nyelven az L4Ka::Mogyoró mikromag fejlesztésével párhuzamosan történt.

Abban az időben az L4Ka::Hazelnut mikrokernel nem támogatta a kernel-space párhuzamosságot, az "L4Ka::Pistachio" mikrokernel pedig csak bizonyos elővételi pontokon támogatta a kernel-space megszakításokat . Az "L4/Fiasco" mikrokernel fejlesztői teljes preemptív multitaskingot valósítottak meg (néhány atomi művelet kivételével). Ez bonyolultabbá tette a kernel architektúrát, de csökkentette a megszakítási késéseket, ami fontos egy valós idejű operációs rendszer számára.

Az „L4/Fiasco” mikrokernelt a „DROPS” [12] operációs rendszerben használták  – a „kemény” valós idejű operációs rendszerben (amikor rendkívül fontos, hogy az eseményre szigorú időkeretekben reagáljanak), szintén a Műszaki Egyetemen fejlesztették ki. Drezda.

A Fiasco OS későbbi verzióiban a mikrokernel architektúra bonyolultsága miatt a fejlesztők visszatértek a hagyományos megközelítéshez - a kernel elindításához kikapcsolt megszakításokkal (néhány elővételi pont kivételével).

Platformfüggetlenség

Mikrokernel L4Ka::Pistachio

Az L4 mikrokernel implementációi, amelyeket az L4Ka::Pistachio mikrokernel megjelenése előtt készítettek, és a "Fiasco" mikrokernel későbbi verziói, a számítógép-architektúra jellemzőit használták (a processzor architektúrához "kötöttek"). Egy architektúrától független API-t fejlesztettek ki. A hordozhatóság kiegészítése ellenére az API nagy teljesítményt nyújtott. A mikrokernel architektúra mögött meghúzódó ötletek nem változtak.

2001 elején egy új L4 API-t tettek közzé, amely nagyon különbözik az előző verzió L4 API-jától, a 4-es verziószámmal ("4-es verzió", más néven "X.2-es verzió"), és más:

Az API új verziójának megjelenése után az SAG csapata elkezdett létrehozni egy új mikrokernelt "L4Ka::Pistachio" néven [13] [14] . A kódot az L4Ka::Hazelnut projekt tapasztalatait felhasználva a semmiből fordították le C++ nyelven. Figyelmet fordítottak a nagy teljesítményre és a hordozhatóságra.

2001. június 10-én Dr. Jochen Liedtke meghalt [7] egy autóbalesetben. Ezt követően a projekt fejlesztési üteme jelentősen csökkent.

2003- ban [15] a munka Liedtke tanítványai: Volkmar Uhlig, Uwe Dannowski és Espen Skoglund erőfeszítéseinek köszönhetően elkészült. A forráskód a 2 tagú BSD licenc alatt jelent meg .

A Fiasco új verziói

Ezzel párhuzamosan folytatódott az L4/Fiasco mikrokernel fejlesztése. Több hardverplatform támogatása ( x86 , AMD64 , ARM ) került hozzáadásra. Nevezetesen, a Fiasco "FiascoUX" nevű verziója futhat Linux operációs rendszert futtató felhasználói területen .

Az L4/Fiasco mikrokernel fejlesztői számos bővítést implementáltak az L4v2 API-hoz.

Ezenkívül a "Fiasco" mikrokernel kommunikációs jogkezelési mechanizmusokat biztosított. Ugyanezek a mechanizmusok léteztek a kernel által fogyasztott erőforrások kezelésére is.

Az "L4Env"-t fejlesztették ki, a felhasználói térben a "Fiasco" mikrokernel tetején futó komponensek készletét. Az "L4Env"-t az "L4Linux"-ban használták, amely a paravirtualizáció (virtualizációs ABI) megvalósítása a Linux kernelek 2.6.x verzióihoz.

University of New South Wales és a NICTA

A University of New South Wales fejlesztői létrehozták az L4/MIPS és L4/Alpha mikrokernelt, az L4 implementációit a 64 bites MIPS és DEC Alpha sorozatú processzorokhoz . Az eredeti L4 mikrokernel csak az x86 architektúrájú processzorokat támogatta, és informálisan "L4/x86" néven vált ismertté. Az implementációkat a semmiből írták C és assembly nyelven, és nem voltak hordozhatóak. A platformfüggetlen L4Ka::Pistachio mikrokernel megjelenése után az UNSW csoport abbahagyta a mikrokernelek fejlesztését, és megkezdte az L4Ka::Pistachio mikrokernel portolását. Az üzenettovábbítási mechanizmus megvalósítása gyorsabbnak bizonyult, mint más implementációk (36 ciklus Itanium architektúra processzorokon ) [16] .

Az UNSW csoport kimutatta, hogy a user-space illesztőprogram ugyanúgy futhat, mint a kernel-space illesztőprogram [17] .

Összetevőket fejlesztett ki a Linux kernelek paravirtualizálásához. A komponensek az L4 mikrokernel tetején futottak. Az eredmény a " Wombat OS " nevet kapta. A Wombat OS futhat x86, ARM és MIPS architektúrán. Intel XScale processzorokon a Wombat OS 30-szor lassabban hajtott végre környezetváltást, mint egy monolitikus Linux kernel [18] .

Az UNSW csoport ezután a NICTA-hoz költözött, létrehozta az L4Ka::Pistachio mikrokernel villát, és elnevezte "NICTA::L4-beágyazottnak". Az új mikrokernel kereskedelmi beágyazott rendszerekhez készült , kevés memóriát igényelt, és egy egyszerűsített L4 API-t valósított meg. Az egyszerűsített API-val a rendszerhívások olyan "rövidek" lettek, hogy nem igényeltek megelőző többfeladatos pontot, és lehetővé tették a valós idejű operációs rendszer megvalósítását [19] .

Kereskedelmi felhasználás

A Qualcomm az L4 mikrokernel NICTA implementációját futtatta a " Mobile Station Modem" (MSM) nevű lapkakészleten Erről 2005 novemberében számoltak be [20] a NICTA képviselői, és 2006 végén az MSM lapkakészletek eladásra kerültek. Így az L4 mikrokernel megvalósítása a mobiltelefonokban kötött ki .

2006 augusztusában Heiser az Open Kernel Labs -t Ekkor Heiser a NICTA [21] által szervezett ERTOS program vezetője volt, és az UNSW professzora volt. Az OK Labs azért jött létre

2008 áprilisában megjelent az "OKL4" mikrokernel 2.1-es verziója, az L4 első nyilvános megvalósítása, amely képességalapú biztonsággal rendelkezik . 2008 októberében megjelent a 3.0 [22] verzió –  az "OKL4" legújabb nyílt forráskódú verziója . A következő verziók forráskódja le van zárva. A hipervizort működtető mikrokernel réteget átírták, hogy támogatást adjon az „OKL4 mikrovizornak” nevezett natív hipervizorhoz [23] .

Az OK Labs az OK :Linux nevű paravirtualizált Linux  operációs rendszert [24] terjesztette . OK : A Linux a Wombat OS leszármazottja volt . Az OK Labs a Symbian és Android operációs rendszerek paravirtualizált verzióit is terjesztette .

Az OK Labs megszerezte a seL4 mikrokernel jogait a NICTA-tól.

2012 elején több mint 1,5 milliárd olyan eszközt adtak el , amelyek az L4 mikrokernel implementációjával voltak felszerelve [25] . Ezen eszközök többsége vezeték nélküli modemeket megvalósító chipeket tartalmazott, és a Qualcomm adta ki őket .

Az L4 megvalósítását az autós szórakoztató rendszerekben is alkalmazták [26] .

Az L4 implementációra épülő operációs rendszert a biztonságos enclave processzor hajtotta végre, amely a chipen található Apple A7 elektronikus áramkör része [27] . Ugyanezt az L4-es implementációt használták a NICTA Darbat projektjében [28] . Az iOS rendszerrel szállított Apple A7-et tartalmazó eszközök . 2015-ben körülbelül 310 millió iOS-eszköz volt [29] .

Ellenőrzés

seL4

2006- ban megkezdődött a harmadik generációs mikrokernel , a "seL4" [30] fejlesztése . A fejlesztést a nulláról kezdte a NICTA programozóinak egy csoportja. Cél: alapot teremteni a biztonságos és megbízható rendszerek kiépítéséhez, amelyek megfelelnek a modern biztonsági követelményeknek, ahogyan például az "Informatikai biztonság értékelésének általános kritériumai" című dokumentumban is szerepel. A mikrokernel kódja kezdettől fogva úgy volt megírva, hogy ellenőrizhető legyen (helyességellenőrzés). Az ellenőrzés a Haskell nyelven történt : a mikrokernel követelményei (specifikáció) Haskell nyelven lettek megírva; a mikrokernel objektumok Haskell objektumként voltak ábrázolva; a berendezéssel végzett munkát emulálták [31] . Ahhoz, hogy egy objektum elérhetőségéről formális érveléssel tudjon információt szerezni, a seL4 képességalapú biztonságon alapuló hozzáférés-vezérlést használt.

2009 - ben befejeződött a seL4 mikrokernel kód [32] helyességének bizonyítása . A bizonyíték megléte biztosította az implementáció és a specifikáció közötti összhangot, megerősítette néhány hiba hiányát a megvalósításban (például a holtpontok hiánya , az élőzárak, a puffertúlcsordulás , az aritmetikai kivételek és az inicializálatlan változók használatának esetei). A seL4 mikrokernel volt az első mikrokernel, amelyet általános célú operációs rendszerhez terveztek, és ellenőrizték [32] .

A seL4 mikrokernel nem szabványos kernel erőforrás-kezelést valósított meg [33] :

Valami hasonlót valósítottak meg a kísérleti Barrelfish OS-ben . A kernel erőforrások kezelésének ezen megközelítése révén lehetővé vált a tulajdonságok elkülönítésével kapcsolatos érvelés, majd később bebizonyosodott, hogy a seL4 mikrokernel biztosítja a tulajdonságok integritását és titkosságát [34] . A bizonyítást az eredeti kódra végezték el.

A NICTA cég kutatóiból álló csapat bebizonyította a szöveg C nyelvről gépi kódra történő fordításának helyességét. Ez lehetővé tette a fordító kizárását a megbízható szoftverek listájáról, és a mikrokernel forráskódjára elvégzett bizonyítást a mikrokernel futtatható fájljára is érvényesnek tekintette.

A seL4 mikrokernel lett az első védett módú kernel , amelyre a legrosszabb eset végrehajtási idő elemzését teljes egészében elvégezték, és ennek az elemzésnek az eredményeit publikálták. Az elemzés eredményei szükségesek a mikrokernel kemény valós idejű operációs rendszerben való használatához [34] .

2014. július 29. NICTA és General Dynamics C4 Systemsbejelentette a seL4 mikrokernel (beleértve a helyességük minden bizonyítékát) nyílt licenc alatti kiadását [35] . A mikrokernel forráskódja és a próbaverziók a GPL v2 licenc alatt jelentek meg. A legtöbb könyvtár és eszköz a 2-clauses BSD licenc alatt került terjesztésre.

A kutatók érdekes megállapítása [36] , hogy a szoftverellenőrzés elvégzésének költsége alacsonyabb, mint a hagyományos szoftverkutatás költségei, annak ellenére, hogy a hitelesítés során sokkal megbízhatóbb információ nyerhető.

2012 augusztusában a NICTA, Rockwell Collins, a Galois Inc , a Boeing és a University of Minnesota a DARPA ügynökség által szervezett, rendkívül megbízható katonai kiberrendszerek fejlesztésére irányuló program [37] részeként pilóta nélküli légi jármű fejlesztésébe kezdett [38] . A fejlesztés fő követelménye a készülék magas megbízhatóságának biztosítása. A felsorolt ​​cégek mindegyike szerepet játszott a programban. A NICTA volt felelős az operációs rendszer fejlesztéséért, és a seL4 mikrokernel köré építette. A felelős feladatokat mikrokernel-komponensekként valósították meg, míg a nem felelős feladatokat paravirtualizált Linux operációs rendszer alatt futtatták. A program fejlesztéseit a Boeing által fejlesztett NICTA Unmanned Little Bird helikopterben tervezték felhasználni. A helikopternek támogatnia kellett a pilótavezérlést és a pilóta nélküli üzemmódot is. 2015 novemberében sikeres megvalósításról számoltak be [39] .

Egyéb kutatás és fejlesztés

Hurd/L4 . 2000 novemberében létrehozták az "l4-hurd" levelezőlistát, hogy megvitassák a " GNU Hurd " kernelnek az L4 mikrokernelre történő portolását . A portolás 2002-2004 között történt, az eredmény a "Hurd / L4" nevet kapta. A "Hurd/L4" megvalósítása nem fejeződött be. 2005-ben a projektet leállították [40] .

Az Osker egy L4-et megvalósító operációs rendszer, és 2005  -ben Haskellben írták . A projekt célja: az OS funkcionális nyelven való megvalósításának lehetőségének tesztelése (és nem a mikrokernel vizsgálata) [41] .

A Codezero a beágyazott rendszerekhez készült L4 mikrokernel megvalósítása, amely 2009  nyarán vált nyilvánosan elérhetővé [42] . A brit "B Labs" cég fejlesztői készítette a semmiből. A kód C nyelven íródott. Az implementáció támogatja az ARM architektúra processzorokat , elsőrendű hypervisort valósít meg , valamint támogatja a Linux és az Android OS virtualizációját [43] [44] . A kód GPL v3 licenc alatti kézbesítésére vonatkozó nyilatkozat ellenére lehetetlen letölteni a kódot a hivatalos webhelyről.

Az F9  az L4 mikrokernel implementációja, amely 2013 júliusában vált nyilvánosan elérhetővé [45] . A semmiből írva C nyelven. Beágyazott rendszerekhez tervezve. Támogatja az ARM architektúra Cortex-M processzorsorozatát . A kódot BSD licenc alatt szállítjuk.

A Fiasco.OC  egy harmadik generációs mikrokernel, amely az "L4/Fiasco" mikrokernelen alapul. Megvalósítja a képesség alapú biztonsági mechanizmust, támogatja a többmagos processzorokat és a hardveres virtualizációt [46] .

Az L4 Runtime Environment (röviden L4Re) egy olyan keretrendszer, amely a "Fiasco.OC" mikrokernelen fut, és a felhasználói tér összetevőinek létrehozására szolgál. Az L4Re funkciókat biztosít kliens/szerver alkalmazások építéséhez, fájlrendszerek megvalósításához, népszerű könyvtárak megvalósításához, mint például a C standard könyvtár ("libc"), a C++ szabványos könyvtár ("libstdc++") és a pthreads könyvtár .

Az L4Re keretrendszer és a "Fiasco.OC" mikrokernel támogatta az x86 (IA-32 és AMD64), ARM és PowerPC (WiP) architektúrákat.

Az L4Linux  egy alrendszer Linux operációs rendszer futtatására a "Fiasco.OC" mikrokernel tetején, paravirtualizáció segítségével [47] . Korábban a "Fiasco.OC" - L4Re pár helyett az "L4 / Fiasco" - L4Env párost használták.

A NOVA ( a  N OVA O S v irtualization a rchitecture ) egy kutatási projekt, amely egy biztonságos és hatékony virtualizációs környezet létrehozására jött létre [48] [49] [50] a megbízható szoftverek kis listájával ( megbízható számítási bázis ) .  A NOVA a következőket tartalmazza:

A NOVA projekt többmagos x86 processzorokat támogatott. Ahhoz, hogy a NOVA mikro-hipervizor (mikrokernelre épített hipervizor) irányítása alatt futhasson, a vendég operációs rendszernek támogatnia kell az Intel VT-x- et vagy az AMD-V-t . A forráskódot a GPL v2 licenc alatt biztosítottuk.

A Xameleon  egy L4 mikrokernelen alapuló operációs rendszer [52] . A projektet 2001 -ben alapította az egyetlen fejlesztő, Alekszej Mandrikin (született : 1973. január 19. ). Az operációs rendszer eredetileg az „ L4/Fiasco ” mikrokernelre épült. Később a szerző áttelepítette az operációs rendszert az " L4Ka::Pistachio " mikrokernelre. Az operációs rendszer forráskódja le van zárva.

A WrmOS egy nyílt forráskódú valós idejű operációs rendszer (RTOS), amely az L4 mikrokernelen alapul. A WrmOS saját megvalósítással rendelkezik a kernelhez, a szabványos könyvtárakhoz és a hálózati veremhez. A támogatott processzorarchitektúrák a SPARC, ARM, x86, x86_64. A WrmOS kernel az L4 Kernel Reference Manual Version X.2 dokumentumon alapul . A WrmOS tetején egy paravirtualizált Linux kernel ( w4linux ) fut.

Jegyzetek

  1. 1 2 Liedtke, Jochen ( 1993. december ). „Az IPC javítása kernel tervezéssel” (PDF) . 14. ACM szimpózium az operációs rendszer elveiről . Asheville , NC , USA . pp. 175-88. Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2016. március 4. a Wayback Machine -nál
  2. L4 mikrokernel család. Áttekintés Archivált 2015. május 14-én a Wayback Machine -nél  (angol nyelven) // A Drezdai Műszaki Egyetem ( Németország ) webhelye.
  3. Az ELAN nyelv archiválva : 2015. május 12. a Wayback Machine -nél  // A Dresdeni Műszaki Egyetem weboldala .
  4. 1 2 3 4 5 6 7 8 9 10 Liedtke, Jochen ( 1993. december ). „Kitartó rendszer valós használatban – az első 13 év tapasztalatai” (PDF) . Az operációs rendszerek objektumorientációjával foglalkozó 3. nemzetközi műhely (IWOOOS) anyaga . Asheville , NC , USA . pp. 2-11. Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2015. július 10. a Wayback Machine -nál
  5. 1 2 In Memoriam Jochen Liedtke (1953-2001) Archiválva : 2012. március 5. a Wayback Machine -nél .
  6. 1 2 Liedtke, Jochen ( 1995. december ). „A µ-Kernel felépítéséről” . Proc. 15. ACM szimpózium az operációs rendszerek alapelveiről (SOSP) . pp. 237-250. Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archivált : 2009. március 18. a Wayback Machine -nél
  7. 1 2 3 Rendszerarchitektúra csoport. rólunk. emberek. Liedtke . Archivált másolat .
  8. Jochen Liedtke. Oldaltábla-struktúrák finomszemcsés virtuális memóriához Archiválva : 2007. november 12., a Wayback Machine -en . Technikai jelentés 872. Német Nemzeti Számítástechnikai Kutatóközpont (GMD). 1994. október .
  9. Gefflaut, Alain; Jaeger, Trent; Park, Yoonho; Liedtke, Jochen ; Elphinstone, Kevin; Uhlig, Volkmar; Tidswell, Jonathon; Deller, Luke; Reuther, Lars ( 2000 ). "The Sawmill multiserver megközelítés" . ACM SIGOPS Európai Műhely . Kolding , Dánia . pp. 109-114. Ellenőrizze a dátumot itt: |date=( súgó angolul )
  10. Fleisch, Brett D; Allan, Mark. Munkahelyi mikrokernel és operációs rendszer:  esettanulmány . — John Wiley & Sons, Ltd. Archiválva az eredetiből 2007. augusztus 24-én.
  11. "L4Ka" csoportoldal // archive.org .
  12. ↑ A Drops áttekintése Archiválva : 2011. augusztus 7. a Wayback Machine -nél .
  13. Mikrokernel "L4Ka::Pistachio" Archiválva : 2007. január 9. a Wayback Machine -nél  .
  14. "L4Ka" fejlesztőcsapat Archiválva : 2007. január 22. a Wayback Machine -nél  .
  15. Az L4Ka::Pistachio Microkernel . (angol) Fehér könyv . PDF . 2003. május 1. // archive.org .
  16. Gray, Charles; Chapman, Matthew; Chubb, Péter; Mosberger-Tang, David; Heiser, Gernot (2005. április). Itanium - rendszermegvalósító meséje . USENIX éves műszaki konferencia . Annaheim , CA , USA . pp. 264-278. Elavult használt paraméter |coauthors=( help );Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2007. február 17. a Wayback Machine -nél
  17. Leslie, Ben; Chubb, Péter; FitzRoy-Dale, Nicholas; Gotz, Stefan; Grey, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting; Elphinstone, Kevin; Heiser, Gernot . Felhasználói szintű eszközmeghajtók: elért teljesítmény  (neopr.)  // Journal of Computer Science and Technology. - T. 20 , 5. sz . — S. 654-664 . - doi : 10.1007/s11390-005-0654-4 .
  18. van Schaik, Carl; Heiser, Gernot (2007. január). „Nagy teljesítményű mikrokernelek és virtualizáció ARM-en és szegmentált architektúrákon” . 1. nemzetközi műhely a beágyazott rendszerek mikrokerneleiről . Sydney , Ausztrália : NICTA . pp. 11-21 . Letöltve: 2007-04-01 . Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2007. április 26. a Wayback Machine -nél
  19. Ruocco, Sergio. Valós idejű programozói körút az általános célú L4 mikrokernelekről //  EURASIP  Journal on Embedded Systems, Special Issue on Operating System Support for Embedded Real-Time Applications : Journal. - 2008. - október ( 2008. évf. ). - 1-14 . o . - doi : 10.1155/2008/234710 .  (nem elérhető link)
  20. [1] Archiválva : 2006. augusztus 25. a Wayback Machine -nél .
  21. Az ERTOS program oldala a NICTA honlapján // archive.org .
  22. OKL4 3.0 (lefelé irányuló kapcsolat) . Letöltve: 2011. május 21. Az eredetiből archiválva : 2011. május 16.. 
  23. OKL4 mikrovizor Archiválva : 2014. március 13. a Wayback Machine -nál .
  24. OK:Linux (downlink) . Letöltve: 2015. július 8. Az eredetiből archiválva : 2015. április 10. 
  25. A Kernel Labs megnyitása (2012. január 19.). Az Open Kernel Labs szoftver túllépi az 1,5 milliárd mobileszköz-szállítmány mérföldkövét . Sajtóközlemény . Letöltve 2015-11-10 .
  26. Open Kernel Labs ( 2012. március 27. ). A Bosch által az Infotainment Systems számára kiválasztott Kernel Labs Automotive Virtualization megnyitása . Sajtóközlemény . Archiválva az eredetiből 2012. július 2-án.
  27. iOS biztonság . Letöltve: 2017. szeptember 28. Az eredetiből archiválva : 2014. szeptember 23..
  28. Darbat projekt archiválva : 2013. december 19. a Wayback Machine -nél .
  29. [2] Archiválva : 2015. július 15. a Wayback Machine -nél .
  30. [3] Archiválva : 2022. május 3. a Wayback Machine -nél .
  31. Derrin, Fülöp; Elphinstone, Kevin; Klein, Gerwin; kakas; Dávid; Chakravarty, Manuel MT ( 2006. szeptember ). „A kézikönyv futtatása: megközelítés a magas szintű mikrokernel-fejlesztéshez” (PDF) . ACM SIGPLAN Haskell Workshop . Portland , Oregon , USA . pp. 60-71. Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2016. március 3. a Wayback Machine -nél
  32. 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronick, június; Kakas, Dávid; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Érintse meg, Harvey; Winwood, Simon ( 2009. október ). “seL4: Egy operációs rendszer kernel formális ellenőrzése” (PDF) . 22. ACM szimpózium az operációs rendszer elveiről . Big Sky , MT , USA . Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2011. július 28. a Wayback Machine -nél
  33. Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin ( 2008. április ). „Kernel tervezése a fizikai memória elkülönítésére és biztosítására” . 1. Workshop a beágyazott rendszerek elkülönítéséről és integrációjáról . Glasgow , Egyesült Királyság . DOI : 10.1145/1435458 . Letöltve: 2015-07-08 . Elavult használt paraméter |coauthors=( help );Ellenőrizze a dátumot itt: |date=( súgó angolul ) Archiválva : 2010. április 24. a Wayback Machine -nél
  34. 1 2 Klein, Gerwin; Andronick, június; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Az operációs rendszer mikrokernelének átfogó formális ellenőrzése  (angol)  // ACM Transactions on Computer Systems: napló. — Vol. 32 , sz. 1 . — P. 2:1-2:70 . - doi : 10.1145/2560537 .
  35. NICTA ( 2014. július 29. ). A NICTA által fejlesztett biztonságos operációs rendszer nyílt forráskódú . Sajtóközlemény . Az eredetiből archiválva : 2014. augusztus 10. Letöltve: 2015-07-08 .
  36. Klein, Gerwin; Andronick, június; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot. Az operációs rendszer mikrokernelének átfogó formális ellenőrzése  (angol)  // ACM Transactions on Computer Systems: napló. - 2014. - Kt. 32 . — 64. o . - doi : 10.1145/2560537 .
  37. Nagy biztonságú kiber katonai rendszerek Archivált 2014. augusztus 8. (HACM-ek).
  38. SMACCM projekt archiválva 2015. július 10-én a Wayback Machine -nél // NICTA webhely. A SMACCM az angol rövidítése .  a vezérlési modellek matematikailag biztos összetétele .
  39. Az új generációs drónokat nem lehet feltörni Archivált : 2015. november 18., a Wayback Machine // Popular Mechanics Magazine. 2015. november 12.
  40. A GNU Hurd története. Portolás másik mikrokernelre Archiválva : 2017. március 8. a Wayback Machine -nél  .
  41. Hallgren, T.; Jones, képviselő; Leslie, R.; Tolmach, A. Elvi megközelítés az operációs rendszer felépítéséhez in Haskell  //  Proceedings of the tized ACM SIGPLAN international Conference onfunctional programing : Journal. - 2005. - 20. évf. 40 , sz. 9 . - 116-128 . o . — ISSN 0362-1340 . - doi : 10.1145/1090189.1086380 .
  42. Codezero archiválva : 2015. július 9. a Wayback Machine -nél a genode.org webhelyen.
  43. dev.b-labs.com // archive.org .
  44. A Codezero projekt hivatalos weboldala Archivált 2015. július 9-én a Wayback Machine -nél .
  45. F9 projekttár archiválva : 2017. március 5. a Wayback Machine -en // github.com .
  46. Péter, Mihály; Schild, Henning; Lackorzynski, Adam; Warg, Alexander ( 2009. március ). „Bezárt virtuális gépek – Virtualizáció kis megbízható számítási bázisokkal rendelkező rendszerekben” . VTDS'09: Workshop a virtualizációs technológiáról megbízható rendszerek számára . Nürnberg , Németország . Elavult használt paraméter |coauthors=( help );Ellenőrizze a dátumot itt: |date=( súgó angolul )
  47. L4Linux archiválva : 2015. július 7. a Wayback Machine -nél .
  48. Steinberg, Udo; Bernhard, Kauer ( 2010. április ). "NOVA: Mikrohipervizor-alapú biztonságos virtualizációs architektúra". EuroSys '10: Az 5. Számítógépes Rendszerek Európai Konferenciájának anyaga . Párizs , Franciaország . Ellenőrizze a dátumot itt: |date=( súgó angolul )
  49. Steinberg, Udo; Bernhard, Kauer ( 2010. április ). "A skálázható többprocesszoros felhasználói szintű környezet felé". IIDS'10: Műhely a megbízható rendszerek elkülönítéséről és integrációjáról . Párizs , Franciaország . Ellenőrizze a dátumot itt: |date=( súgó angolul )
  50. Project Nova archiválva 2015. június 24-én a Wayback Machine -nél . Hivatalos oldal.
  51. VMM Seoul archiválva 2018. június 11-én a Wayback Machine -nél // github.com
  52. l4os.ru Archiválva : 2011. február 9. a Wayback Machine -nél . A Xameleon projekt hivatalos weboldala.

Irodalom

Linkek