| Vyvíjí | NICTA a další[1] |
|---|---|
| Rodina OS | Unix-like a další |
| Druh | Svobodný software |
| Aktuální verze | 13.0.0 /1. července2024[2] |
| Podporované platformy | 32bitové: ARM: ARMv6 (ARM11) ARMv7 (Cortex A8, A9, A15) Intel: x86 64bitové: ARM: ARMv8 (Cortex A53 (Raspberry Pi 3)[3] (Cortex A72Raspberry Pi 4)[4]) Intel: x86-64 RISC-V:RV64[5][6] |
| Typ jádra | mikrojádro třetí generace |
| Programovací jazyk | Haskell (model),C,assembler |
| Licence | Svobodný software, převážněGNU GPLv2[7] aBSDv2. |
| Stav | Aktivní |
| Oficiální web | seL4 (anglicky) seL4 Home L4.verified Home |
seL4 (Secure Embedded L4) jesvobodnéjádro operačního systému, přesnějimikrojádro třetí generace, zaměřené na vysokoubezpečnost aspolehlivost.[1]
MikrojádroseL4 bylo vytvořeno jako pokračovatel revolučního mikrojádra druhé generaceL4 německého počítačového vědce jménemJochen Liedtke.
MikrojádroL4 bylo vytvořeno zejména s důrazem na co nejvyšší výkon. Také mikrojádroseL4 bylo vytvořeno s důrazem na vysoký výkon, avšak zároveň s přihlédnutím k otázkám bezpečnosti a formální bezchybnosti. Důležité zlepšení také spočívá v lepší přenositelnosti, a to nejen uživatelskýchserverů (poskytovatelů služeb mikrojádra běžících vuživatelském prostoru), ale též vlastního mikrojádra.[8]
Operační systém typu mikrojádro vznikl jako reakce na neustálé zvětšování klasickýchmonolitických operačních systémů, u kterých tak začal být obtížný další vývoj a údržba. Návrh mikrojádra proto odpovídá teoriistrukturovaného programování. Výhoda mikrojádra spočívá v rozdělení systému na menší části (uživatelskéservery a vlastní mikrojádro), což přináší vyšší přehlednost kódu.
Nevýhodou mikrojádra je nutnost častější změny kontextu při systémovém volání mezi uživatelským procesem, mikrojádrem a obsluhujícími servery a s tím související ztráty výkonu.
Špatný výkon první generace mikrokernelů, jako byl zejménaMach 3, vedl v polovině devadesátých let 20. století množství vývojářů k redefinici celého konceptu mikrokernelu.
Asynchronní vnitro-kernelový konceptmeziprocesové komunikace (IPC) mikrokernelu Mach 3, používající velkouvyrovnávací paměť (buffer), se ukázal být jedním z hlavních důvodů pro jeho špatný výkon. Toto přimělo vývojáře na Machu založených operačních systémů k přenesení některých časově kritických komponent, jako jsou ovladače (systémGNU Hurd)[9] a souborové systémy, zpět do jádra, často až k přechodu khybridnímu jádru (systémymacOS,NT).[10] I když to poněkud zmírnilo problémy s výkonem, je to jasné porušení minimalistického konceptu opravdových mikrokernelů (a plýtvá jejich hlavními výhodami).
Detailní analýzaúzkého hrdla operačního systému Mach indikuje, že (jakékoliv další) požadavky na mikrokernel, dělají problém příliš složitým: kódmeziprocesové komunikace (IPC), jehož většina je v jádře, představuje špatnou lokalizaci; což ve výsledku znamená příliš mnoho neúspěšných čtenícacheCPU (musí se číst z mnohem pomalejší paměti). Tato analýza vedla k závěru, že efektivní mikrokernel musí být dostatečně malý, aby většina výkonu kritického kódu byla k dispozici v cache první úrovně (pokud možno malý zlomek zmíněné cache).
Po zkušenosti s použitím svého mikrokernelu L3, dospěl Liedtke k závěru, že i několik dalších konceptů Machu bylo špatných (vizte též). Prostřednictvím zjednodušení konceptu mikrokernelu ještě vynalezl první mikrokernelyL4 (první vlna mikrojader druhé generace), které byly od počátku primárně navrženy pro vysoký výkon. Za účelem vyždímat každý kousek výkonu jádra, byly celé napsány vassembleru a jejichmeziprocesová komunikace (IPC) tak byla 20krát rychlejší než v případě Machu.
První vlna mikrojader druhé generace, je reprezentována zejména originálním systémemL4, který byl velice pečlivě vytvořen Jochenem Liedtkem vassembleru, což bylo důležité zejména pro vysoký výkon a rychlost tohoto systému. Ale brzy se ukázalo, že by bylo vhodné, aby nejen uživatelskéservery, ale též vlastní mikrojádro, bylo co nejlépe přenositelné na jiné systémy, s jinýmhardware a jinýmiCPU.
Proto se objevila druhá vlna (druhé generace mikrojader), která dala vzniknout mikrojádrům napsaným z větší části ve vyšších programovacích jazycích, zejména jako jsouprogramovací jazyky C aC++, a to mikrojádroL4Ka::Hazelnut a zejménaL4Ka::Pistachio nauniverzitě v Karlsruhe[11], aFiasco naTechnické univerzitě Drážďany.
Další vývoj přinesl potřebu třetí generace mikrojader, s vysokou bezpečností a dostupností, což vyústilo v požadavek formální (matematicky ověřené) bezchybnostizdrojového kódu mikrojader. Tato nová situace vedla k vývoji třetí generace mikrojader, jako jsouseL4[12][13] a pozdější verze Fiasco (Fiasco.OC, které je součástí systémuL4Linux).[14]
V roce2006 tedy zahájila skupinaNICTA programování třetí generace mikrokernelu, který se jmenujeseL4, s cílem poskytnout základ pro vysoce bezpečné a spolehlivé systémy, vhodné pro uspokojování bezpečnostních požadavků, jako jsou ty zCommon Criteria i mimo ně. Od začátku byl vývoj zaměřený na formální verifikaci jádra. Pro usnadnění splnění někdy vzájemně si odporujícími požadavků na výkon a verifikaci, tým použil middle-out softwarový proces, počínaje spustitelnou (modelovou) specifikací napsanou v jazyceHaskell.[12]seL4 používázabezpečení založené na způsobilosti (Capability-based access control) pro umožnění formální (matematické) kontroly ohledně přístupnosti objektů. Poté je však tento modelový kód v Haskellu (přibližně 5700 řádekzdrojového kódu)[15] přepsán dojazyka C (přibližně 8700 řádek) aassembleru (přibližně 600 řádek).[13][8][16]
seL4 je vyvíjen se zvláštním přihlédnutím k otázkám bezpečnosti a formální bezchybnostimikrojádra organizacíNICTA a dalšími vývojáři. Právě kvůli těmto vlastnostem byl vytvořen vývojový model, který umožňuje ověřit zdrojový kódseL4 vefunkcionálním jazyceHaskell pomocíformálních (matematických)důkazů.[8][1]
Ověření bezpečnosti operačních systémů pomocí matematického důkazu funguje i proti útokům využívající strojové učení. Ukazuje se, že útočník je ve výhodě, pokud útočí na komplikovaný systém, který navíc současnými prostředky nelze matematicky ověřit. Více zveřejňuje na svém blogu spoluautorseL4,Gernot Heiser.[17]
Operační systémseL4, na rozdíl od původního operačního systémuL4, implementuje jako uživatelskýserver navíc i správu paměti mikrojádra. Tento uživatelský server se tak stává nezbytnou součástí mikrokernelu. Výsledkem však je další snížení nezbytného počtusystémových volání a neúspěšných čtenípaměti cache.[8]
29. července2014,NICTA aGeneral Dynamics C4 Systems uvedly, že seL4 s příslušnými důkazy bylo uvolněno jakootevřený software.[18]Zdrojové kódy jádra amatematické důkazy (o jeho správnosti a bezpečnosti) byly uvolněny pod licencíGPLv2 a většina knihoven a nástrojů byla uvolněna pod2-klauzulovou BSD licencí.[19]
Nick Spinale, financovaný nadací seL4 Foundation, od roku 2023 vyvíjí podporu pro vývoj programů a aplikací vuživatelském prostoru seL4, vprogramovacím jazyceRust.
Spinale vytvořil komplexní infrastrukturu pro podporu jazyka Rust, která je dobře integrována se zbytkem ekosystému seL4 (capDL, Microkit, sel4test). Tato práce byla15. listopadu2023 přijata technickým řídícím výborem nadace seL4 a lze ji nalézt naGitHubu. Také Nickova přednáška na nedávném summitu seL4 je na kanáluYouTube seL4. Na GitHubu je k dispozici ukázkový systém, který využíváframeworkovladače zařízení, asynchronní programování v Rustu, a podporuknihoven z ekosystému Rustu k naprogramování maléhowebového serveru.
Celkovým výsledkem bude umožnit programátorům programovat bezpečnější kód, s méně chybami, na uživatelské úrovni nad systémem seL4, aniž by potřebovali úplné formální ověření (jako mikrojádro seL4), s jazykem Rust, který probouzí stále větší zájem, a který je v souladu s programováním vestavěných systémů kritických z hlediska zabezpečení a bezpečnosti.[20]
Samotné jádro seL4 pro provozování programovacího jazykaC++ nic nepotřebuje, pokud nepotřebujete používatstandardní knihovnu C++ (STL), která by tedy, v případě svého použití, měla být portována do konkrétního prostředí seL4. Pokud byste chtěli zkompilovat kód C++, který nepoužívá standardní knihovnu, pak je to relativně snadné a na GitHubu, v sekci sel4test je triviální příklad.[2]
Tento způsob je vhodný spíše pro vhled do problematiky, který by mohl trochu ukázat, co je vyžadováno pro správný port C++, ale nelze to brát jako dobrý nápad nebo způsob, jak vybudovat spolehlivý systém.[21]
{{Cite conference}} označená jako k „pouze dočasnému použití“.{{Cite conference}} označená jako k „pouze dočasnému použití“.{{Cite press release}} označená jako k „pouze dočasnému použití“.Archivováno 15. 3. 2016 naWayback Machine.Související témata
{{Cite conference}} označená jako k „pouze dočasnému použití“.Archivováno 5. 9. 2006 naWayback Machine. (on L4 kernel and compiler){{Cite conference}} označená jako k „pouze dočasnému použití“.Archivováno 12. 8. 2014 naWayback Machine. Evolution of L4 design and implementation approaches