seL4

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání
seL4
Web seL4 (anglicky)
seL4 Home
L4.verified Home
Vyvíjí NICTA a další[1]
Rodina OS Unix-like a další
Druh Svobodný software
Aktuální verze 7.0.0[2] / 5. září 2017
Podporované platformy 32-bitové:
ARM:
ARMv6 (ARM11)
ARMv7 (Cortex A8, A9, A15)
Intel:
x86
64-bitové:
ARM:
ARMv8 (Cortex A53 (Raspberry Pi 3))
Intel:
x86-64[2]
Typ jádra mikrojádro třetí generace
Programovací jazyk Haskell (model), C, Assembler
Licence Svobodný software, převážně GNU GPLv2[3] a BSDv2.
Stav Aktivní

seL4 (Secure Embedded 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.[1]

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 jménem Jochen Liedtke.

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.[4]

Historie[editovat | editovat zdroj]

První generace mikrojader[editovat | editovat zdroj]

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)[5] a souborové systémy, zpět do jádra, často až k přechodu k hybridnímu jádru (systémy macOS, NT).[6] 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).

L4 family tree

Druhá generace mikrojader[editovat | editovat zdroj]

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 (mikrojádra 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 jeho meziprocesová komunikace (IPC) tak byla 20 krá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), 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[7], a Fiasco na Technické univerzitě Drážďany.

Třetí generace mikrojader[editovat | editovat zdroj]

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 je seL4[8][9] a pozdější verze Fiasco (Fiasco.OC, obsažené v systému L4Linux).[10]

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.[8] seL4 používá 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 (~5700 řádek)[11] přepsán do jazyka C (~8700 řádek) a assembleru (~600 řádek).[9][4][12]

Bezpečnost[editovat | editovat zdroj]

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 ve funkcionálním jazyce Haskell pomocí formálních důkazů.[4][1]

Architektura[editovat | editovat zdroj]

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.[4]

Open Source[editovat | editovat zdroj]

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.[13] 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í.

Odkazy[editovat | editovat zdroj]

Reference[editovat | editovat zdroj]

  1. a b c MIHULKA, Stanislav. Ochrání nehacknutelné jádro počítače před kybernetickými útoky? [online]. http://www.osel.cz, [cit. 2015-10-04]. Dostupné online. (česky) 
  2. a b seL4 Version 7.0.0 Release
  3. License
  4. a b c d Advanced Operating Systems [online]. NICTA, [cit. 2015-07-19]. Dostupné online. (anglicky) 
  5. KOUSOULOS, Constantine. Re: Device drivers in Mach? [online]. 2007-03-21. Dostupné online. (anglický) 
  6. CUSTER, Helen. Windows NT. 1.. vyd. Praha : Grada Publishing, 1994. 424 s. ISBN 80-85424-87-8.  
  7. L4Ka Project [online]. http://www.kit.edu/english/, [cit. 2015-07-11]. Dostupné online. (anglicky) 
  8. a b Derrin, Philip (September 2006). "Running the manual: an approach to high-assurance microkernel development". ACM SIGPLAN Haskell Workshop: 60–71. 
  9. a b A formal proof of functional correctness was completed in 2009. (October 2009) "seL4: Formal verification of an OS kernel". 22nd ACM Symposium on Operating System Principles. 
  10. Fiasco.OC - The L4Re Microkernel [online]. TU Dresden, [cit. 2015-07-11]. Dostupné online. (anglicky) 
  11. seL4: Formal Verification of an OS Kernel [online]. 2010-12-15, [cit. 2016-11-06]. Dostupné online.  
  12. seL4: Formal Veri cation of an OS Kernel [online]. [cit. 2016-06-08]. Dostupné online.  
  13. NICTA: Secure operating system developed by NICTA goes open source, tisková zpráva, [cit. June 25, 2015], Dostupné on-line.

Související články[editovat | editovat zdroj]

GNU – GNU GPL (licence)[editovat | editovat zdroj]

BSD – BSD licence[editovat | editovat zdroj]

Související systémy[editovat | editovat zdroj]

Související témata

Další čtení[editovat | editovat zdroj]

Externí odkazy[editovat | editovat zdroj]