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] .
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.
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] .
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:
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] .
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.
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).
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 .
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.
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] .
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] .
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] .
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.