Rodzina mikrojądra L4 - L4 microkernel family

Rodzina mikrojądra L4
Deweloper Jochen Liedtke
Napisane w Asembler , potem C , C++
Rodzina systemów operacyjnych L4
Stan pracy Aktualny
Model źródłowy Otwarte źródło , zamknięte źródło
Pierwsze wydanie 1993 ; 28 lat temu ( 1993 )
Cel marketingowy Niezawodne przetwarzanie
Dostępne w angielski, niemiecki
Platformy Intel i386 , x86 , x86-64 , ramię , MIPS , SPARC
Typ jądra Mikrojądro
Licencja Kod źródłowy , dowody : Biblioteki GPLv2 , narzędzia : BSD 2 klauzula
Poprzedzony Eumel
Oficjalna strona internetowa os .inf .tu-drezno .de /L4

L4 to rodzina mikrojądra drugiej generacji , używana do implementacji różnych typów systemów operacyjnych (OS), choć głównie dla typów zgodnych z Unix , Portable Operating System Interface ( POSIX ).

L4, podobnie jak jego poprzednik microkernel L3 , został stworzony przez niemieckiego informatyka Jochena Liedtke w odpowiedzi na słabą wydajność wcześniejszych systemów operacyjnych opartych na mikrojądrze. Liedtke uważał, że system zaprojektowany od początku pod kątem wysokiej wydajności, a nie innych celów, może stworzyć mikrojądro o praktycznym zastosowaniu. Jego oryginalna implementacja w ręcznie zakodowanej Intel i386 specyficznych dla asemblerze kod w 1993 roku wywołał duże zainteresowanie w przemyśle komputerowym. Od momentu wprowadzenia L4 został opracowany jako wieloplatformowy i poprawiający bezpieczeństwo , izolację i niezawodność .

Dokonano różnych re-implementacji oryginalnego binarnego interfejsu binarnego aplikacji jądra L4 (ABI) i jego następców, w tym L4Ka::Pistachio ( Karlsruhe Institute of Technology ), L4/MIPS ( Uniwersytet Nowej Południowej Walii (UNSW)), Fiasco ( Politechnika w Dreźnie (TU Dresden)). Z tego powodu nazwa L4 została uogólniona i nie odnosi się już tylko do oryginalnej implementacji Liedtke. Obecnie dotyczy całej rodziny mikrojądra, w tym interfejsu jądra L4 i jego różnych wersji.

L4 jest szeroko stosowany. Jeden wariant, OKL4 z Open Kernel Labs , został dostarczony w miliardach urządzeń mobilnych.

Paradygmat projektowania

Określając ogólną ideę mikrojądra , Liedtke stwierdza:

Koncepcja jest tolerowana wewnątrz mikrojądra tylko wtedy, gdy przeniesienie jej poza jądro, tj. umożliwienie konkurencyjnych implementacji, uniemożliwiłoby implementację wymaganej funkcjonalności systemu.

W tym duchu mikrojądro L4 zapewnia kilka podstawowych mechanizmów: przestrzenie adresowe (abstrahowanie tabel stron i zapewnianie ochrony pamięci), wątki i planowanie (abstrakcja wykonania i ochrona czasowa) oraz komunikacja między procesami (do kontrolowanej komunikacji ponad granicami izolacji).

System operacyjny oparty na mikrojądrze, takim jak L4, zapewnia usługi jako serwery w przestrzeni użytkownika, które monolityczne jądra, takie jak Linux lub mikrojądra starszej generacji, zawierają wewnętrznie. Na przykład, aby zaimplementować bezpieczny system uniksowy , serwery muszą zapewniać zarządzanie prawami, które Mach zawierał w jądrze.

Historia

Słaba wydajność mikrojąder pierwszej generacji, takich jak Mach , skłoniła wielu programistów do ponownego przeanalizowania całej koncepcji mikrojądra w połowie lat dziewięćdziesiątych. Zastosowana w Mach koncepcja komunikacji asynchronicznej w procesie buforowania w jądrze okazała się jednym z głównych powodów jego słabej wydajności. Skłoniło to programistów systemów operacyjnych opartych na Mach do przeniesienia niektórych krytycznych czasowo komponentów, takich jak systemy plików lub sterowniki, z powrotem do jądra. Chociaż poprawiło to nieco problemy z wydajnością, wyraźnie narusza koncepcję minimalności prawdziwego mikrojądra (i marnuje ich główne zalety).

Szczegółowa analiza wąskiego gardła Macha wykazała, między innymi, że jego zbiór roboczy jest zbyt duży: kod IPC wyraża słabą lokalizację przestrzenną; oznacza to, że powoduje to zbyt wiele chybień w pamięci podręcznej , z których większość jest w jądrze. Ta analiza dała początek zasadzie, że wydajne mikrojądro powinno być na tyle małe, aby większość kodu krytycznego dla wydajności zmieściła się w pamięci podręcznej (pierwszego poziomu) (najlepiej niewielki ułamek wspomnianej pamięci podręcznej).

L3

Jochen Liedtke postanowił udowodnić, że dobrze zaprojektowana, cieńsza warstwa komunikacji międzyprocesowej (IPC), z dbałością o wydajność i konstrukcję specyficzną dla maszyny (w przeciwieństwie do oprogramowania wieloplatformowego ), może przynieść znaczną poprawę wydajności w świecie rzeczywistym. Zamiast złożonego systemu IPC Macha, jego mikrojądro L3 po prostu przekazywało wiadomość bez dodatkowych kosztów. Za określenie i wdrożenie wymaganych polityk bezpieczeństwa uznano obowiązki serwerów przestrzeni użytkownika . Rolą jądra było jedynie zapewnienie niezbędnego mechanizmu umożliwiającego serwerom na poziomie użytkownika egzekwowanie zasad. L3, opracowany w 1988 roku, sprawdził się jako bezpieczny i solidny system operacyjny , używany przez wiele lat m.in. przez Technischer Überwachungsverein (Stowarzyszenie Inspekcji Technicznej).

drzewo genealogiczne L4

L4

Po pewnym doświadczeniu w korzystaniu z L3, Liedtke doszedł do wniosku, że kilka innych koncepcji Macha również było niewłaściwie umiejscowionych. Upraszczając jeszcze bardziej koncepcje mikrojądra, opracował pierwsze jądro L4, które zostało zaprojektowane przede wszystkim z myślą o wysokiej wydajności. Aby wydobyć każdy kawałek wydajności, całe jądro zostało napisane w języku asemblerowym , a jego IPC było 20 razy szybsze niż Macha. Tak dramatyczny wzrost wydajności jest rzadkim wydarzeniem w systemach operacyjnych, a prace Liedtke zaowocowały nowymi implementacjami L4 i pracami nad systemami opartymi na L4 na wielu uniwersytetach i instytutach badawczych, w tym w IBM , gdzie Liedtke rozpoczęła pracę w 1996 roku, TU Dresden i UNSW . W IBM Thomas J. Watson Research Center Liedtke i jego koledzy kontynuowali badania nad systemami opartymi na L4 i mikrojądrach, zwłaszcza nad Sawmill OS.

L4Ka::Orzech laskowy

W 1999 roku Liedtke przejął Grupę Architektury Systemów na Uniwersytecie w Karlsruhe , gdzie kontynuował badania nad systemami mikrojądra. Jako dowód koncepcji, że mikrojądro o wysokiej wydajności może być również skonstruowane w języku wyższego poziomu, grupa opracowała L4Ka::Hazelnut , wersję jądra C++, która działa na maszynach opartych na IA-32 i ARM . Wysiłek zakończył się sukcesem, wydajność była nadal akceptowalna, a wraz z wydaniem, wersje jąder w języku asemblerowym zostały skutecznie wycofane.

L4/Fiasko

Równolegle do rozwoju L4Ka::Hazelnut, w 1998 roku Grupa Systemów Operacyjnych TUD:OS z TU Dresden zaczęła opracowywać własną implementację C++ interfejsu jądra L4, o nazwie L4/Fiasco. W przeciwieństwie do L4Ka::Hazelnut, który nie zezwala na współbieżność w jądrze, i jego następcy L4Ka::Pistachio, który zezwala na przerwania w jądrze tylko w określonych punktach wywłaszczania, L4/Fiasco było w pełni wywłaszczalne (z wyjątkiem ekstremalnie krótkich atomów operacji) w celu uzyskania niskiego opóźnienia przerwania . Uznano to za konieczne, ponieważ L4/Fiasco jest używany jako podstawa DROPS, systemu operacyjnego obsługującego twarde przetwarzanie czasu rzeczywistego , również opracowanego na Uniwersytecie Technicznym w Dreźnie. Jednak złożoność projektu z pełnym wywłaszczaniem skłoniła późniejsze wersje Fiasco do powrotu do tradycyjnego podejścia L4 polegającego na uruchamianiu jądra z wyłączonymi przerwaniami, z wyjątkiem ograniczonej liczby punktów wywłaszczania.

Wieloplatformowy

L4Ka::Pistacja

Do czasu wydania L4Ka::Pistachio i nowszych wersji Fiasco wszystkie mikrojądra L4 były z natury powiązane z podstawową architekturą procesora. Następną dużą zmianą w rozwoju L4 było opracowanie wieloplatformowego (niezależnego od platformy) interfejsu programowania aplikacji ( API ), który nadal zachowywał wysoką wydajność pomimo wyższego poziomu przenośności. Chociaż podstawowe koncepcje jądra były takie same, nowe API wprowadziło wiele istotnych zmian w stosunku do poprzednich wersji L4, w tym lepszą obsługę systemów wieloprocesorowych, luźniejsze powiązania między wątkami i przestrzeniami adresowymi oraz wprowadzenie kontroli wątków na poziomie użytkownika bloki (UTCB) i rejestry wirtualne. Po wydaniu nowego interfejsu API L4 (wersja X.2 aka wersja 4) na początku 2001 roku, Grupa Architektury Systemu na Uniwersytecie w Karlsruhe wdrożyła nowe jądro, L4Ka::Pistachio , całkowicie od zera, skupiając się teraz zarówno na wysokiej wydajności, jak i ruchliwość. Został wydany na dwuklauzulowej licencji BSD .

Nowsze wersje Fiasco

Mikrojądro L4/Fiasco zostało również znacznie ulepszone na przestrzeni lat. Obsługuje teraz kilka platform sprzętowych, od x86 przez AMD64 do kilku platform ARM. Warto zauważyć, że wersja Fiasco (Fiasco-UX) może działać jako aplikacja na poziomie użytkownika w systemie Linux.

L4/Fiasco implementuje kilka rozszerzeń do API L4v2. Wyjątek IPC umożliwia jądru wysyłanie wyjątków procesora do aplikacji obsługi na poziomie użytkownika. Za pomocą obcych wątków można precyzyjnie kontrolować wywołania systemowe. Dodano UTCB w stylu X.2. Fiasco zawiera również mechanizmy kontroli praw komunikacji i wykorzystania zasobów na poziomie jądra. Na Fiasco opracowywany jest zbiór podstawowych usług na poziomie użytkownika (o nazwie L4Env), które są wykorzystywane między innymi do parawirtualizacji obecnej wersji systemu Linux (4.19, stan na maj 2019 r.) (o nazwie L 4 Linux ).

Uniwersytet Nowej Południowej Walii i NICTA

Rozwój nastąpił również na Uniwersytecie Nowej Południowej Walii (UNSW), gdzie programiści zaimplementowali L4 na kilku platformach 64-bitowych. Ich praca zaowocowała powstaniem L4/MIPS i L4/Alpha , w wyniku czego oryginalna wersja Liedtke została retrospektywnie nazwana L4/x86 . Podobnie jak oryginalne jądra Liedtke, jądra UNSW (napisane w mieszance assemblera i C) były nieprzenośne i każde zaimplementowane od zera. Wraz z wydaniem wysoce przenośnego L4Ka::Pistachio, grupa UNSW porzuciła własne jądra na rzecz produkcji wysoce dostrojonych portów L4Ka::Pistachio, w tym najszybszej w historii implementacji przekazywania komunikatów (36 cykli w architekturze Itanium ) . Grupa wykazała również, że sterowniki urządzeń mogą działać równie dobrze na poziomie użytkownika, jak w jądrze, i opracowała Wombat , wysoce przenośną wersję Linuksa na L4, która działa na procesorach x86 , ARM i MIPS . Na procesorach XScale koszty przełączania kontekstu Wombat są do 50 razy niższe niż w natywnym systemie Linux.

Później grupa UNSW, w swoim nowym domu w NICTA (dawniej National ICT Australia, Ltd. ), rozwidliła L4Ka::Pistachio do nowej wersji L4 o nazwie NICTA::L4-embedded . Jak sama nazwa wskazuje, był przeznaczony do użytku w komercyjnych systemach wbudowanych , a w konsekwencji kompromisy w implementacji faworyzowały mały rozmiar pamięci i zmniejszoną złożoność. Interfejs API został zmodyfikowany tak, aby prawie wszystkie wywołania systemowe były wystarczająco krótkie, aby nie wymagały punktów wywłaszczania, aby zapewnić wysoką responsywność w czasie rzeczywistym.

Wdrożenie komercyjne

W listopadzie 2005 r. firma NICTA ogłosiła, że Qualcomm wdraża wersję L4 firmy NICTA na swoich chipsetach Mobile Station Modem . Doprowadziło to do użycia L4 w telefonach komórkowych sprzedawanych pod koniec 2006 roku. W sierpniu 2006 roku lider ERTOS i profesor UNSW Gernot Heiser założył firmę o nazwie Open Kernel Labs (OK Labs) w celu wspierania komercyjnych użytkowników L4 i dalszego rozwoju L4 dla komercyjne wykorzystanie pod marką OKL4 , w ścisłej współpracy z NICTA. OKL4 Wersja 2.1, wydana w kwietniu 2008 roku, była pierwszą ogólnie dostępną wersją L4, która zawierała zabezpieczenia oparte na możliwościach . OKL4 3.0, wydana w październiku 2008 roku, była ostatnią wersją OKL4 o otwartym kodzie źródłowym. Nowsze wersje są zamkniętymi źródłami i opierają się na przepisaniu w celu obsługi natywnego wariantu hiperwizora o nazwie OKL4 Microvisor. OK Labs dystrybuował także parawirtualizowanego Linuksa o nazwie OK:Linux, potomka Wombata, oraz parawirtualizowane wersje SymbianOS i Androida . OK Labs nabył również prawa do seL4 od NICTA.

Dostawy OKL4 przekroczyły 1,5 miliarda na początku 2012 roku, głównie na chipach modemów bezprzewodowych Qualcomm. Inne wdrożenia obejmują samochodowe systemy informacyjno-rozrywkowe .

Procesory z serii Apple A zaczynające się od A7 zawierają koprocesor Secure Enclave z systemem operacyjnym L4 opartym na jądrze L4 opracowanym w NICTA w 2006 roku. Oznacza to, że L4 jest obecnie dostarczany na wszystkich urządzeniach z systemem iOS, których całkowita dostawa jest szacowana na 310 mln za rok 2015.

Wysoka pewność: seL4

W 2006 roku grupa NICTA rozpoczęła projektowanie od podstaw mikrojądra trzeciej generacji , nazwanego seL4, w celu stworzenia podstawy dla wysoce bezpiecznych i niezawodnych systemów, spełniających wymagania bezpieczeństwa, takie jak wymagania Common Criteria i wyższe. Od początku rozwój miał na celu formalną weryfikację jądra. Aby ułatwić spełnienie czasami sprzeczne wymagania wydajności i weryfikacji, zespół użył środkowy-out proces oprogramowania począwszy od specyfikacji wykonywalnego pisemnej w Haskell . seL4 wykorzystuje kontrolę dostępu opartą na możliwościach, aby umożliwić formalne wnioskowanie o dostępności obiektów.

Formalny dowód poprawności funkcjonalnej została zakończona w roku 2009. Dowodem daje gwarancję, że realizacja kernela jest poprawny przed jego specyfikacji oraz powoduje, że jest on wolny od błędów wykonawczych, takich jak zakleszczenia, livelocks , przepełnienia bufora, arytmetyka wyjątki lub wykorzystanie zainicjalizowana zmienne. seL4 jest uważane za pierwsze w historii zweryfikowane jądro systemu operacyjnego ogólnego przeznaczenia.

seL4 stosuje nowatorskie podejście do zarządzania zasobami jądra, eksportując zarządzanie zasobami jądra na poziom użytkownika i poddając je tej samej kontroli dostępu opartej na możliwościach, co zasoby użytkownika. Model ten, który został również przyjęty przez firmę Barrelfish , upraszcza wnioskowanie o właściwościach izolacji i umożliwił późniejsze udowodnienie, że seL4 wymusza podstawowe właściwości zabezpieczeń, takie jak integralność i poufność. Zespół NICTA udowodnił również poprawność translacji z języka C na wykonywalny kod maszynowy, wyprowadzając kompilator z zaufanej bazy obliczeniowej seL4. Oznacza to, że dla pliku wykonywalnego jądra są zachowane weryfikacje zabezpieczeń wysokiego poziomu. seL4 jest również pierwszym opublikowanym jądrem systemu operacyjnego w trybie chronionym z kompletną i solidną analizą najgorszego przypadku wykonania w czasie (WCET), co jest warunkiem wstępnym jego użycia w twardych systemach czasu rzeczywistego .

29 lipca 2014 r. NICTA i General Dynamics C4 Systems ogłosiły, że seL4 z pełnymi dowodami jest teraz udostępniany na licencjach open source . Kod źródłowy jądra i dowody są objęte licencją GNU General Public License w wersji 2 (GPLv2), a większość bibliotek i narzędzi podlega klauzuli 2 BSD . W kwietniu 2020 r. ogłoszono, że Fundacja seL4 została utworzona pod patronatem Linux Foundation w celu przyspieszenia rozwoju i wdrażania seL4.

Naukowcy twierdzą, że koszt formalnej weryfikacji oprogramowania jest niższy niż koszt inżynierii tradycyjnego oprogramowania „high assurance”, mimo że zapewnia znacznie bardziej wiarygodne wyniki. W szczególności koszt jednej linii kodu podczas opracowywania seL4 oszacowano na około 400 USD , w porównaniu do 1000 USD w przypadku tradycyjnych systemów o wysokiej pewności.

W ramach programu DARPA High-Assurance Cyber ​​Military Systems (HACMS), NICTA wraz z partnerami projektu Rockwell Collins , Galois Inc, University of Minnesota i Boeing opracowali drona o wysokiej pewności opartego na seL4, wraz z innymi narzędziami i oprogramowaniem zapewniającym bezpieczeństwo. planowany transfer technologii do opcjonalnie pilotowanego autonomicznego śmigłowca bezzałogowego Little Bird opracowywanego przez Boeinga. Ostateczna demonstracja technologii HACMS odbyła się w Sterling w stanie Wirginia w kwietniu 2017 r. DARPA sfinansowała również kilka kontraktów Small Business Innovative Research (SBIR) związanych z seL4 w ramach programu rozpoczętego przez dr Johna Launchbury . Małe firmy, które otrzymały SBIR związane z seL4, obejmowały: DornerWorks, Techshot, Wearable Inc, Real Time Innovations i Critical Technologies.

Inne badania i rozwój

Osker, system operacyjny napisany w Haskell , kierował się specyfikacją L4; chociaż ten projekt koncentrował się głównie na wykorzystaniu funkcjonalnego języka programowania do rozwoju systemu operacyjnego, a nie na badaniach mikrojądra.

CodeZero to mikrojądro L4 dla systemów wbudowanych z naciskiem na wirtualizację i implementację natywnych usług systemu operacyjnego. Istnieje wersja na licencji GPL oraz wersja, która została ponownie licencjonowana przez B Labs Ltd., przejęta przez Nvidię jako zamknięte źródło i rozwidlona w 2010 roku.

Mikrojądro F9, implementacja L4 na licencji BSD, jest dedykowana procesorom ARM Cortex-M dla głęboko osadzonych urządzeń z ochroną pamięci.

Architektura wirtualizacji NOVA OS to projekt badawczy skupiający się na zbudowaniu bezpiecznego i wydajnego środowiska wirtualizacji z niewielką zaufaną bazą obliczeniową. NOVA składa się z mikrohiperwizora, hiperwizora na poziomie użytkownika ( monitor maszyny wirtualnej ) oraz działającego na nim nieuprzywilejowanego wieloserwerowego środowiska użytkownika o nazwie NUL. NOVA działa na systemach wielordzeniowych opartych na architekturze ARMv8-A i x86.

WrmOS to system operacyjny czasu rzeczywistego oparty na mikrojądrze L4. Posiada własne implementacje jądra, standardowych bibliotek i stosu sieciowego, obsługujące architektury ARM, SPARC, x86 i x86-64. Na WrmOS działa parawirtualizowane jądro Linux (w4linux).

Zobacz też

Bibliografia

Dalsza lektura

Zewnętrzne linki