seL4 (security enhanced L4) je svobodné jádro operačního systému, přesněji mikrojádro třetí generace, zaměřené na vysokou bezpečnost a spolehlivost.
Mikrojádro seL4 bylo vytvořeno jako pokračovatel revolučního mikrojádra druhé generace L4 německého počítačového vědce Jochena Liedtkeho.
Mikrojádro L4 bylo vytvořeno zejména s důrazem na co nejvyšší výkon. Také mikrojádro seL4 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ých serverů (poskytovatelů služeb mikrojádra běžících v uživatelském prostoru), ale též vlastního mikrojádra.
Historie
První generace mikrojader Operační systém typu mikrojádro vznikl jako reakce na neustálé zvětšování klasických monolitický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á teorii strukturované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éna Mach 3, vedl v polovině devadesátých let 20. století množství vývojářů k redefinici celého konceptu mikrokernelu.
Asynchronní vnitro-kernelový koncept meziprocesové komunikace (IPC) mikrokernelu Mach 3, používající velkou vyrovná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ém GNU Hurd) a souborové systémy, zpět do jádra, často až k přechodu k hybridnímu jádru (systémy macOS, NT). 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ód meziprocesové 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í cache CPU (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).
náhled|400px|L4 family tree
Druhá generace mikrojader 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í mikrokernely L4 (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 v assembleru a jejich meziprocesová 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émem L4, který byl velice pečlivě vytvořen Jochenem Liedtkem v assembleru, 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ým hardware a jinými CPU.
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 jsou programovací jazyky C a C++, a to mikrojádro L4Ka::Hazelnut a zejména L4Ka::Pistachio na univerzitě v Karlsruhe, a Fiasco.OC na Technické univerzitě Drážďany.
Třetí generace mikrojader 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é) bezchybnosti zdrojového kódu mikrojader. Tato nová situace vedla k vývoji třetí generace mikrojader, jako jsou seL4A formal proof of functional correctness was completed in 2009.. (Později tato situace vedla k systému Verified Fiasco.)
V roce 2006 tedy zahájila skupina NICTA programování třetí generace mikrokernelu, který se jmenuje seL4, 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 z Common 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 jazyce Haskell. 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 řádek zdrojového kódu) přepsán do jazyka C (přibližně 8700 řádek) a assembleru (přibližně 600 řádek).
Bezpečnost seL4 je vyvíjen se zvláštním přihlédnutím k otázkám bezpečnosti a formální bezchybnosti mikrojá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ód seL4 ve funkcionálním jazyce Haskell pomocí formálních (matematických) důkazů.
Výhoda mikrojader ověřených formálním důkazem 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 spoluautor seL4, Gernot Heiser.
Architektura Operační systém seL4, na rozdíl od původního operačního systému L4, 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čtu systémových volání a neúspěšných čtení paměti cache.
Open Source 29. července 2014, NICTA a General Dynamics C4 Systems uvedly, že seL4 s příslušnými důkazy bylo uvolněno jako otevřený software. Zdrojové kódy jádra a matematické 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 pod 2-klauzulovou BSD licencí.
Ekosystém seL4 se běžně používá jako základ jádra pro komponentované vestavěné systémy a seL4 Foundation podporuje sadu souvisejících nástrojů a frameworků. Artefakty ekosystému (včetně kódu, nástrojů a důkazů) jsou obvykle poskytovány pod permisivními licencemi (BSD).
Microkit seL4 Microkit je framework operačního systému postavený na seL4, který poskytuje malou sadu abstrakcí zaměřených na snížení bariéry pro budování staticky strukturovaných systémů při zachování výkonu a efektivity paměti.
Device Driver Framework (sDDF) Framework ovladačů zařízení seL4 (sDDF) je architektura ovladačů pro systémy založené na seL4, o které se diskutovalo na několika summitech; materiály summitu popisují návrh s důrazem na oddělení odpovědností a komunikaci založenou na událostech/asynchronní komunikaci s datovými cestami ve sdílené paměti.
LionsOS náhled|250px|Systémová architektura referenčního systému LionsOS
LionsOS je v současné době ve vývoji společnosti Trustworthy Systems na Univerzitě Nového Jižního Walesu (UNSW) a jeho cílem je poskytovat aplikačně orientované operační služby, jako jsou sítě, souborové systémy a další I/O operace. I když se primárně zaměřoval na statické architektury, kde jsou zdroje alokovány při bootování (např. embedded), plánuje se podpora i pro dynamičtější operační systémy.
Primárním cílem systému LionsOS je konkurovat Linuxu pomocí mikrojádra seL4, které udržuje výkon systému a zároveň zajišťuje správnou implementaci hardwaru seL4 pomocí verifikačních nástrojů teorie splnitelnosti (Satisfiability Modulo Theories - SMT). Hlavními stavebními kameny navrhovaného systému jsou Mikrokit seL4 a Framework ovladačů zařízení seL4 (sDDF). Aktuální verze 0.4.0 byla vydána v srpnu 2026 a obsahuje mj. i framework Microkit 2.3.0 s jádrem seL4 16.0.0. Podpora pro programovací jazyky
Podpora pro Rust v seL4 Nick Spinale, financovaný nadací seL4 Foundation, od roku 2023 vyvíjí podporu pro vývoj programů a aplikací v uživatelském prostoru seL4, v programovacím jazyce Rust.
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 byla 15. listopadu 2023 přijata technickým řídícím výborem nadace seL4 a lze ji nalézt na GitHubu. Také Nickova přednáška na nedávném summitu seL4 je na kanálu YouTube seL4. Na GitHubu je k dispozici ukázkový systém, který využívá framework ovladače zařízení, asynchronní programování v Rustu, a podporu knihoven z ekosystému Rustu k naprogramování malého webové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.
Podpora pro C++ v seL4 Samotné jádro seL4 pro provozování programovacího jazyka C++ nic nepotřebuje, pokud nepotřebujete používat standardní 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.
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.
Podpora pro hardware (CPU)
Podpora MCS seL4 pro RISC-V Dne 29. června 2026 bylo dasaženo významného milníku v plánu verifikace seL4, který trval roky: konfigurace MCS seL4, což je operační systém reálného času, který poskytuje podporu pro systémy se smíšenou kritickou úrovní (naléhavostí, prioritou), byla nyní dokázána jako bezchybná na RISC-V.
Tato konfigurace je novou největší funkcí seL4, nepostradatelnou pro aplikace v reálném čase se smíšenou kritickou úrovní, jako je použití v automobilovém průmyslu. Obsahuje rozsáhlé změny v implementaci mikrojádra a API. Její ověření proto vyžadovalo značné úsilí a bylo dlouhodobě prioritou v plánu seL4.
Ověřovací tým dokončil klíčový formální důkaz funkční správnosti seL4 s MCS, aktuálně pro RISC‑V, přičemž důkaz je postaven tak, aby platil pro procesorovou architekturu RISC‑V (tj. zohledňuje její sémantiku), a teď se chystají převést ten samý typ důkazu na ARM 64-bit.
Odkazy
Reference
Související články
GNU – GNU GPL (licence) Free Software Foundation (FSF) – organizace (nadace), která zastřešuje Projekt GNU Projekt GNU – projekt původně Richarda Stallmana, který má za cíl vyvinout kvalitní a svobodný operační systém – GNU GNU GPL – licence napsané Richardem Stallmanem a dalšími, k uskutečnění cílů Projektu GNU GNU Hurd – svobodný operační systém založený na mikrokernelu GNU Mach, vyvíjený Projektem GNU KataOS – svobodný operační systém od Google založený na mikrokernelu seL4 LionsOS – svobodný operační systém od Trustworthy Systems založený na mikrokernelu seL4 (více licencí) Linux (jádro) – jádro svobodného operačního systému, vyvíjené Linux Foundation; modulární monolitické jádro Linux-libre – jádro svobodného operačního systému, vyvíjené dcerou FSF (FSFLA), fork Linux (jádro); modulární monolitické jádro
BSD – BSD licence