Array ( [0] => 15596634 [id] => 15596634 [1] => cswiki [site] => cswiki [2] => SeL4 [uri] => SeL4 [3] => [img] => [4] => [day_avg] => [5] => [day_diff] => [6] => [day_last] => [7] => [day_prev_last] => [8] => [oai] => [9] => [is_good] => [10] => [object_type] => [11] => 0 [has_content] => 0 [12] => [oai_cs_optimisticky] => ) Array ( [0] => {{DISPLAYTITLE:seL4}} [1] => {{Infobox - operační systém [2] => | jméno = seL4 [3] => | logo = [4] => | velikost loga = [5] => | obrázek = [6] => | popisek = [7] => | vyvíjí = [[NICTA]] a další{{Citace elektronické monografie [8] => | příjmení = Mihulka [9] => | jméno = Stanislav [10] => | titul = Ochrání nehacknutelné jádro počítače před kybernetickými útoky? [11] => | vydavatel = http://www.osel.cz [12] => [13] => | datum_přístupu = 2015-10-04 [14] => | url = http://www.osel.cz/8438-ochrani-nehacknutelne-jadro-pocitace-pred-kybernetickymi-utoky.html [15] => | jazyk = česky [16] => }} [17] => | rodina = [[Unix-like]] a další [18] => | druh = [[Svobodný software]] [19] => | způsob aktualizace = [20] => | správce balíčků = [21] => | podporované platformy = 32bitové:
[[ARM]]:
ARMv6 (ARM11)
ARMv7 (Cortex A8, A9, A15)
[[Intel]]:
[[x86]]
64bitové:
ARM:
ARMv8 (Cortex A53 ([[Raspberry Pi|Raspberry Pi 3]]){{Citace elektronického periodika [22] => | titul = Raspberry PI 3 Model B and Model B+ {{!}} seL4 docs [23] => | periodikum = docs.sel4.systems [24] => | url = https://docs.sel4.systems/Hardware/Rpi3.html [25] => | datum přístupu = 2024-01-09 [26] => }}
(Cortex A72 [[Raspberry Pi|Raspberry Pi 4]]){{Citace elektronického periodika [27] => | titul = Raspberry Pi 4 Model B {{!}} seL4 docs [28] => | periodikum = docs.sel4.systems [29] => | url = https://docs.sel4.systems/Hardware/Rpi4.html [30] => | datum přístupu = 2024-01-09 [31] => }})
Intel:
[[x86-64]]
[[RISC-V]]:RV64[https://docs.sel4.systems/Hardware/]{{Citace elektronické monografie [32] => | příjmení = Osier-Mixon [33] => | jméno = Jeffrey [34] => | titul = seL4 is verified on RISC-V! [35] => | url = https://riscv.org/blog/2020/06/sel4-is-verified-on-risc-v/ [36] => | datum vydání = 2020-06-09 [37] => | datum přístupu = 2023-08-11 [38] => | jazyk = en-US [39] => }} [40] => | typ kernelu = [[mikrojádro]] třetí generace [41] => | programovací jazyk = [[Haskell (programovací jazyk)|Haskell]] ([[Simulace|model]]), [[C (programovací jazyk)|C]], [[assembler]] [42] => | uživatelské rozhraní = [43] => | aktuální verze = 12.1.0[https://sel4.discourse.group/t/15-june-2021-release/373 15 June 2021 Release][https://docs.sel4.systems/releases/sel4/12.1.0 seL4 Version 12.1.0 Release][https://docs.sel4.systems/releases/sel4/12.0.0.html seL4 Version 12.0.0 Release] [44] => | datum vydání = [[15. červen|15 června]] [[2021]] [45] => | licence = [[Svobodný software]], převážně [[GNU General Public License|GNU GPLv2]]{{Citace elektronického periodika |titul=License |url=https://sel4.systems/Info/GettingStarted/license.pml |datum přístupu=2017-01-29 |url archivu=https://web.archive.org/web/20170202062351/https://sel4.systems/Info/GettingStarted/license.pml |datum archivace=2017-02-02 }} a [[BSD licence|BSDv2]]. [46] => | stav = Aktivní [47] => | web = [http://sel4.systems/ seL4 (anglicky)]
[https://web.archive.org/web/20200424223717/http://ts.data61.csiro.au/projects/seL4/ seL4 Home]
[https://web.archive.org/web/20200418163906/https://ts.data61.csiro.au/projects/TS/l4.verified/ L4.verified Home] [48] => | podpora do = [49] => }} [50] => '''seL4''' ('''Secure Embedded L4''') je [[Svobodný software|svobodné]] [[jádro operačního systému]], přesněji [[mikrojádro]] třetí generace, zaměřené na vysokou [[počítačová bezpečnost|bezpečnost]] a [[teorie spolehlivosti|spolehlivost]]. [51] => [52] => Mikrojádro '''seL4''' bylo vytvořeno jako pokračovatel revolučního mikrojádra druhé generace [[L4 (jádro)|L4]] německého počítačového vědce jménem [[Jochen Liedtke]]. [53] => [54] => 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 [[Démon (software)|serverů]] (poskytovatelů služeb mikrojádra běžících v [[User space|uživatelském prostoru]]), ale též vlastního mikrojádra.{{Citace elektronické monografie [55] => | titul = Advanced Operating Systems [56] => | vydavatel = NICTA [57] => | datum_přístupu = 2015-07-19 [58] => | url = http://www.cse.unsw.edu.au/~cs9242/13/lectures/01-introx4.pdf [59] => | jazyk = anglicky [60] => }} [61] => [62] => == Historie == [63] => [64] => === První generace mikrojader === [65] => [[Operační systém]] typu mikrojádro vznikl jako reakce na neustálé zvětšování klasických [[Monolitické jádro|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é programování|strukturovaného programování]]. Výhoda mikrojádra spočívá v rozdělení systému na menší části (uživatelské [[Démon (software)|servery]] a vlastní mikrojádro), což přináší vyšší přehlednost kódu. [66] => [67] => 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. [68] => [69] => Špatný výkon první generace mikrokernelů, jako byl zejména [[Mach (jádro)|Mach 3]], vedl v polovině devadesátých let 20. století množství vývojářů k redefinici celého konceptu mikrokernelu. [70] => [71] => Asynchronní vnitro-kernelový koncept [[Meziprocesová komunikace|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]]){{Citace elektronické monografie [72] => | příjmení = Kousoulos [73] => | jméno = Constantine [74] => | titul = Re: Device drivers in Mach? [75] => | datum_vydání = 2007-03-21 [76] => | url = http://lists.gnu.org/archive/html/bug-hurd/2007-03/msg00089.html [77] => | jazyk = anglický [78] => }} a souborové systémy, zpět do jádra, často až k přechodu k [[hybridní jádro|hybridnímu jádru]] (systémy [[macOS]], [[Windows NT|NT]]).{{Citace monografie|příjmení = Custer|jméno = Helen|příjmení2 = |jméno2 = |titul = Windows NT|vydání = 1.|vydavatel = Grada Publishing|místo = Praha|rok = 1994|počet stran = 424|strany = |isbn = 80-85424-87-8}} 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). [79] => [80] => Detailní analýza [[Efekt hrdla láhve (software)|ú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|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]] [[Centrální procesorová jednotka|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). [81] => [82] => [[Soubor:L4 family tree.png|náhled|400px|L4 family tree]] [83] => [84] => === Druhá generace mikrojader === [85] => 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 ([[Jochen Liedtke|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 [[assembler]]u a jejich [[meziprocesová komunikace]] (IPC) tak byla 20krát rychlejší než v případě Machu. [86] => [87] => 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 [[assembler]]u, 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é [[Démon (software)|servery]], ale též vlastní mikrojádro, bylo co nejlépe přenositelné na jiné systémy, s jiným [[hardware]] a jinými [[Centrální procesorová jednotka|CPU]]. [88] => [89] => 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 [[C (programovací jazyk)|programovací jazyky C]] a [[C++]], a to mikrojádro '''L4Ka::Hazelnut''' a zejména '''L4Ka::Pistachio''' na [[Technologický institut v Karlsruhe|univerzitě v Karlsruhe]]{{Citace elektronické monografie [90] => | titul = L4Ka Project [91] => | vydavatel = http://www.kit.edu/english/ [92] => | datum_přístupu = 2015-07-11 [93] => | url = https://www.l4ka.org/ [94] => | jazyk = anglicky [95] => }}, a '''Fiasco''' na [[Technická univerzita Drážďany|Technické univerzitě Drážďany]]. [96] => [97] => === Třetí generace mikrojader === [98] => 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ý kód|zdrojového kódu]] mikrojader. Tato nová situace vedla k vývoji třetí generace mikrojader, jako jsou '''seL4'''{{cite conference [99] => | first = Philip [100] => | last = Derrin [101] => |author2=Elphinstone, Kevin |author3=Klein, Gerwin |author4=Cock |author5=David |author6= Chakravarty, Manuel M. T. [102] => | title = Running the manual: an approach to high-assurance microkernel development [103] => | booktitle = ACM SIGPLAN Haskell Workshop [104] => |date=September 2006 [105] => | pages = 60–71 [106] => | location = [[Portland, Oregon]] [107] => | url = http://portal.acm.org/citation.cfm?id=1159842.1159850&coll=portal&dl=ACM&type=series&idx=1159842&part=Proceedings&WantType=Proceedings&title=Haskell&CFID=18785943&CFTOKEN=93152956 [108] => }} [109] => A formal proof of functional correctness was completed in 2009. [110] => {{cite conference [111] => | first1 = Gerwin [112] => | last1 = Klein [113] => | first2 = Kevin [114] => | last2 = Elphinstone [115] => | first3 = Gernot [116] => | last3 = Heiser [117] => | author3-link = Gernot Heiser [118] => | first4 = June [119] => | last4 = Andronick [120] => | first5 = David [121] => | last5 = Cock [122] => | first6 = Philip [123] => | last6 = Derrin [124] => | first7 = Dhammika [125] => | last7 = Elkaduwe [126] => | first8 = Kai [127] => | last8 = Engelhardt [128] => | first9 = Rafal [129] => | last9 = Kolanski [130] => | first10 = Michael [131] => | last10 = Norrish [132] => | first11 = Thomas [133] => | last11 = Sewell [134] => | first12 = Harvey [135] => | last12 = Tuch [136] => | first13 = Simon [137] => | last13 = Winwood [138] => | title = seL4: Formal verification of an OS kernel [139] => | booktitle = 22nd ACM Symposium on Operating System Principles [140] => |date=October 2009 [141] => | location = Big Sky, MT, USA [142] => | doi = [143] => | url = http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf [144] => }} [145] => a pozdější verze Fiasco ('''Fiasco.OC''', které je součástí systému [[L4Linux]]).{{Citace elektronické monografie [146] => | titul = Fiasco.OC - The L4Re Microkernel [147] => | vydavatel = TU Dresden [148] => | datum_přístupu = 2015-07-11 [149] => | url = http://os.inf.tu-dresden.de/fiasco/ [150] => | jazyk = anglicky [151] => }} [152] => [153] => 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 ([[Vědecké modelování|modelovou]]) specifikací napsanou v jazyce [[Haskell (programovací jazyk)|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ý kód|zdrojového kódu]]){{Citace elektronické monografie|příjmení=|jméno=|titul=seL4: Formal Verification of an OS Kernel|url=http://www.mimuw.edu.pl/~iwanicki/courses/ds/2010/presentations/ds-presentation-18-10-sel4.pdf|vydavatel=|místo=|datum vydání=2010-12-15|datum přístupu=2016-11-06}} přepsán do [[C (programovací jazyk)|jazyka C]] (přibližně 8700 řádek) a [[assembler]]u (přibližně 600 řádek).{{Citace elektronické monografie|příjmení=|jméno=|titul=seL4: Formal Veri cation of an OS Kernel|url=http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf|vydavatel=|místo=|datum vydání=|datum přístupu=2016-06-08}} [154] => [155] => == Bezpečnost == [156] => '''seL4''' je vyvíjen se zvláštním přihlédnutím k otázkám bezpečnosti a formální bezchybnosti [[Mikrojádro|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í programování|funkcionálním jazyce]] [[Haskell (programovací jazyk)|Haskell]] pomocí [[Formální verifikace|formálních]] (matematických) [[Matematický důkaz|důkazů]]. [157] => [158] => ==== Výhoda mikrojader ověřených formálním důkazem ==== [159] => 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]].{{Citace elektronické monografie [160] => | titul = ML accelerates the cyber arms race — we need real security more than ever [161] => | url = https://microkerneldude.org/2022/11/08/ml-accelerates-the-cyber-arms-race-we-need-real-security-more-than-ever/ [162] => | datum vydání = 2022-11-08 [163] => | datum přístupu = 2022-11-08 [164] => | jazyk = en [165] => }} [166] => [167] => == Architektura == [168] => Operační systém '''seL4,''' na rozdíl od původního operačního systému '''L4''', implementuje jako uživatelský [[Démon (software)|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é volání|systémových volání]] a neúspěšných čtení [[Cache|paměti cache]]. [169] => [170] => == Open Source == [171] => [[29. červenec|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]].{{cite press release [172] => |title= Secure operating system developed by NICTA goes open source [173] => |url= https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/ [174] => |accessdate= June 25, 2015 [175] => |publisher= [[NICTA]] [176] => }} {{Wayback|url=https://www.nicta.com.au/category/research/media-releases/secure-operating-system-developed-by-nicta-goes-open-source/ |date=20160315212902 }} [[Zdrojový kód|Zdrojové kódy]] jádra a [[matematický důkaz|matematické důkazy]] (o jeho správnosti a bezpečnosti) byly uvolněny pod licencí [[GNU General Public License|GPLv2]] a většina knihoven a nástrojů byla uvolněna pod [[BSD licence|2-klauzulovou BSD]] licencí.{{Citace elektronického periodika [177] => | titul = Licensing {{!}} seL4 docs [178] => | periodikum = docs.sel4.systems [179] => | url = https://docs.sel4.systems/processes/licenses.html [180] => | datum přístupu = 2023-09-23 [181] => }} [182] => [183] => == Podpora pro programovací jazyky == [184] => [185] => === Podpora pro Rust v seL4 === [186] => Nick Spinale, financovaný nadací seL4 Foundation, od roku 2023 vyvíjí podporu pro vývoj programů a aplikací v [[User space|uživatelském prostoru]] seL4, v [[Programovací jazyk|programovacím jazyce]] [[Rust (programovací jazyk)|Rust]]. [187] => [188] => 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. listopad|15. listopadu]] [[2023]] přijata technickým řídícím výborem nadace seL4 a lze ji nalézt na [[GitHub|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č zařízení|ovladače zařízení]], asynchronní programování v Rustu, a podporu [[Knihovna (programování)|knihoven]] z ekosystému Rustu k naprogramování malého [[Webový server|webového serveru]]. [189] => [190] => Celkovým výsledkem bude umožnění 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.{{Citace elektronického periodika [191] => | titul = Support for Rust in seL4 userspace now available [192] => | periodikum = sel4.systems [193] => | url = https://sel4.systems/news/2023#support-rust [194] => | datum přístupu = 2024-01-28 [195] => }} [196] => [197] => === Podpora pro C++ v seL4 === [198] => Samotné jádro seL4 pro provozování programovacího jazyka [[C++]] nic nepotřebuje, pokud nepotřebujete používat [[Standard Template Library|standardní knihovnu]] C++ (STL), která by však 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.[https://github.com/seL4/sel4test] [199] => [200] => 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.{{Citace elektronického periodika [201] => | titul = Support for Rust in seL4 userspace now available [202] => | periodikum = lists.sel4.systems [203] => | url = https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/6EP46JFJ3ZSDC3ODQQLEF3KFNIJQKNXS/ [204] => | datum přístupu = 2024-01-28 [205] => }} [206] => [207] => == Odkazy == [208] => [209] => === Reference === [210] => [211] => [212] => === Související články === [213] => [214] => ==== GNU – GNU GPL (licence) ==== [215] => * [[Free Software Foundation]] (FSF) – organizace ([[nadace]]), která zastřešuje [[Projekt GNU]] [216] => ** Projekt GNU – projekt původně [[Richard Stallman|Richarda Stallmana]], který má za cíl vyvinout kvalitní a [[svobodný software|svobodný]] [[operační systém]] – [[GNU]] [217] => *** [[GNU General Public License|GNU GPL]] – licence napsané Richardem Stallmanem a dalšími, k uskutečnění cílů Projektu GNU [218] => **** [[GNU Hurd]] – svobodný operační systém založený na mikrokernelu [[GNU Mach]], vyvíjený Projektem GNU [219] => **** [[KataOS]] – svobodný operační systém od [[Google]] založený na mikrokernelu '''seL4'''{{Citace elektronického periodika [220] => | příjmení = PM [221] => | jméno = WN [222] => | titul = KataOS by mohl pohánět zařízení internetu věcí s podporou ML [223] => | periodikum = www.businessit.cz [224] => | url = https://www.businessit.cz/cz1/kataos-by-mohl-pohanet-zarizeni-internetu-veci-s-podporou-ml.php [225] => | datum přístupu = 2022-12-14 [226] => }}{{Citace elektronického periodika [227] => | titul = Google oznámil vývoj operačního systému KataOS [228] => | periodikum = www.abclinuxu.cz [229] => | url = https://www.abclinuxu.cz/zpravicky/google-oznamil-vyvoj-operacniho-systemu-kataos [230] => | datum přístupu = 2022-12-13 [231] => }}{{Citace elektronické monografie [232] => | titul = Announcing KataOS and Sparrow [233] => | url = https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html [234] => | datum přístupu = 2022-12-13 [235] => }} [236] => **** [[Linux (jádro)]] – jádro svobodného operačního systému, vyvíjené [[Linux Foundation]]; modulární [[monolitické jádro]] [237] => **** [[Linux-libre]] – jádro svobodného operačního systému, vyvíjené [[Dceřiná společnost|dcerou]] [[Free Software Foundation|FSF]] ([[Free Software Foundation Latin America|FSFLA]]), [[fork]] Linux (jádro); modulární monolitické jádro [238] => [239] => ==== BSD – BSD licence ==== [240] => * Berkeley Software Distribution – obchodní organizace při [[Kalifornská univerzita v Berkeley|University of California, Berkeley]], která vyvinula licenci [[BSD licence|BSD]] a používala pro práce nad operačním systémem [[BSD|BSD Unix]]. [241] => ** [[BSD licence]] – licence organizace BSD, která používala pro [[BSD|BSD Unix]] a odvozená díla [242] => *** [[FreeBSD]] – [[Svobodný software|svobodný]] [[operační systém]], který vznikl z [[BSD|BSD Unixu]]; modulární [[monolitické jádro]] [243] => *** [[DragonFly BSD]] – [[Svobodný software|svobodný]] [[operační systém]], [[fork]] [[FreeBSD]] 4.8 s [[Hybridní jádro|hybridním jádrem]] [244] => *** [[NetBSD]] – [[Svobodný software|svobodný]] [[operační systém]], který vznikl z [[BSD|BSD Unixu]] (před [[FreeBSD]]); modulární [[monolitické jádro]] [245] => *** [[OpenBSD]] – [[Svobodný software|svobodný]] [[operační systém]], [[fork]] [[NetBSD]] zaměřený na bezpečnost; [[monolitické jádro]] [246] => *** [[MINIX 3]] – [[Svobodný software|svobodný]] [[operační systém]]; [[mikrojádro]] navržené a vytvořené profesorem jménem [[Andrew S. Tanenbaum]]em; [[Softwarová kompatibilita|kompatibilita]] s NetBSD [247] => [248] => ==== Související systémy ==== [249] => * [[Fiasco.OC]] - mikrojádro třetí generace, pokračovatel L4, vytvořené [[Technická univerzita Drážďany|Technickou univerzitou Drážďany]]. Více vizte [[L4Linux]]. [250] => * [[SELinux]] - bezpečnostní rozšíření systému Linux [251] => '''Související témata''' [252] => * [[Jochen Liedtke|prof. Jochen Liedtke]] - autor původního návrhu L4, některé jeho názory a myšlenky [253] => * [[Formální verifikace]] - moderní metoda ověřování kvality software [254] => * [[Bezpečnostně zaměřený operační systém]] [255] => [256] => [257] => === Další čtení === [258] => * Jochen Liedtke, Ulrich Bartling, Uwe Beyer, Dietmar Heinrichs, Rudolf Ruland, Gyula Szalay. ''[http://portal.acm.org/citation.cfm?id=122124&dl=ACM&coll=&CFID=15151515&CFTOKEN=6184618 Two years of experience with a μ-Kernel based OS]'', ACM Press 1991 [259] => * {{Cite conference [260] => |first = Jochen [261] => |last = Liedtke [262] => |authorlink = Jochen Liedtke [263] => |coauthors = Haeberlen, Andreas; Park, Yoonho; Reuther, Lars; Uhlig, Volkmar [264] => |date = 2000-10-22 [265] => |title = Stub-Code Performance is Becoming Important [266] => |booktitle = In Proceedings of the 1st Workshop on Industrial Experiences with Systems Software (WIESS), San Diego, CA, October 2000 [267] => |url = http://l4ka.org:80/publications/ [268] => |url archivu = https://web.archive.org/web/20110130215823/http://l4ka.org/publications/ [269] => |format = PDF [270] => |accessdate = 2006-09-05 [271] => |titul = Archivovaná kopie [272] => |datum přístupu = 2015-06-19 [273] => |datum archivace = 2011-01-30 [274] => |nedostupné = ne [275] => }}{{Wayback|url=http://l4ka.org/publications/ |date=20060905181634 }} (on L4 kernel and compiler) [276] => * Cheng Guanghui, Nicholas Mc Guire. ''[https://web.archive.org/web/20120327161621/http://dslab.lzu.edu.cn:8080/docs/publications/l4_kickstart.pdf L4/Fiasco/L4Linux Kickstart]'', Distributed & Embedded Systems Lab – Lanzhou University [277] => * {{Cite conference [278] => | first1 = Kevin [279] => | last1 = Elphinstone [280] => | first2 = Gernot [281] => | last2 = Heiser [282] => | authorlink2 = Gernot Heiser [283] => | date = October 2014 [284] => | title = From L3 to seL4: What Have We Learnt in 20 Years of L4 Microkernels? [285] => | booktitle = 24th ACM SIGOPS Symposium on Operating Systems Principles [286] => | location = Farmington, PA, USA [287] => | pages = 133-150 [288] => | url = http://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml [289] => | titul = Archivovaná kopie [290] => | datum přístupu = 2015-06-19 [291] => | url archivu = https://web.archive.org/web/20140812065831/http://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml [292] => | datum archivace = 2014-08-12 [293] => | nedostupné = ano [294] => }} {{Wayback|url=http://ssrg.nicta.com.au/publications/nictaabstracts/Elphinstone_Heiser_13.abstract.pml |date=20140812065831 }} Evolution of L4 design and implementation approaches [295] => [296] => === Externí odkazy === [297] => * {{cs}} [https://www.root.cz/clanky/debian-14-bude-forky-google-oznamil-novy-operacni-system-kataos/ Google oznámil nový operační systém KataOS] [298] => * {{en}} [http://gernot-heiser.org Gernot Heiser's web page] [299] => * {{en}} [https://microkerneldude.org/ Gernot Heiser's blog] [300] => * {{en}} [https://microkerneldude.org/2024/04/18/gofetch-will-people-ever-learn/ GoFetch: Will people ever learn?] - hutnější článek o bezpečnosti operačních systémů [301] => * {{en}} [https://medium.com/dataseries/why-no-operating-system-is-safe-c8001de00539 Why No Operating System Is Safe] [302] => * {{en}} [https://web.archive.org/web/20140830054545/http://www.l4hq.org/ L4Hq]: L4 headquarters, community site for L4 projects [303] => * {{en}} [http://os.inf.tu-dresden.de/L4/ The L4 microkernel family]: Overview over L4 implementations, documentation and projects [304] => * {{en}} [http://wiki.tudos.org/ Official TUD:OS Wiki] [305] => * {{en}} [http://www.l4ka.org L4Ka]: Implementations L4Ka::Pistachio and L4Ka::Hazelnut [306] => * {{en}} [http://www.cse.unsw.edu.au/~disy/L4/ UNSW]: Implementations for [[DEC Alpha]] and [[MIPS (architektura)|MIPS architecture]] [307] => * {{en}} [https://web.archive.org/web/20080820043831/http://okl4.org/ OKL4]: Commercial L4 version from [https://web.archive.org/web/20090319021316/http://www.ok-labs.com/ Open Kernel Labs] [308] => * {{en}} [https://web.archive.org/web/20140717185304/http://www.ertos.nicta.com.au/research/l4/ NICTA L4]: Research Overview and Publications [309] => * {{en}} [http://genode.org/about/index Genode Operating System Framework], an offspring of the L4 community [310] => * {{cs}} [http://www.linuxexpres.cz/novinky/zdrojove-kody-sel4-otevreny Zdrojové kódy seL4 otevřeny] [311] => * {{sk}} [http://www.dsl.sk/article.php?article=7919 Vyvinutý operačný systém s matematickým dôkazom o svojej bezpečnosti] [312] => [313] => {{Portály|Svobodný software}} [314] => [[Kategorie:Operační systémy]] [315] => [[Kategorie:Mikrojádra]] [316] => [[Kategorie:Systémový software]] [317] => [[Kategorie:Svobodný software]] [318] => [[Kategorie:Svobodný software naprogramovaný v Haskellu]] [319] => [[Kategorie:Software v C]] [] => )
good wiki

SeL4

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. 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.

More about us

About

Expert Team

Vivamus eget neque lacus. Pellentesque egauris ex.

Award winning agency

Lorem ipsum, dolor sit amet consectetur elitorceat .

10 Year Exp.

Pellen tesque eget, mauris lorem iupsum neque lacus.

You might be interested in

,'Svobodný software','operační systém','NICTA','BSD','Démon (software)','monolitické jádro','assembler','BSD licence','fork','Jochen Liedtke','GNU General Public License','C (programovací jazyk)'

Assembler

BSD

Fork