L4 микро ядролар тобы - Википедия - L4 microkernel family

L4 екінші ұрпақтың отбасы микро ядролар, әдетте іске асыру үшін қолданылады Unix тәрізді операциялық жүйелер, сонымен қатар басқа жүйелерде қолданылады.

L4, оның алдыңғы нұсқасы сияқты L3 микро ядросы, құрылды Неміс информатик Джохен Лидтке ертерек орналасқан микро-ядроға негізделген операциялық жүйелердің нашар жұмысына жауап ретінде. Лидтке басынан бастап басқа мақсаттарға емес, жоғары өнімділікке арналған жүйе практикалық қолданудың микро ядроларын шығара алады деп ойлады. Қолмен кодталған оның алғашқы орындалуы Intel i386 - ерекше құрастыру тілі 1993 ж. код компьютерлік индустрияға үлкен қызығушылық тудырды.[дәйексөз қажет ] Ол енгізілген сәттен бастап L4 арнасы әзірленді платформаның тәуелсіздігі жетілдіруде қауіпсіздік, оқшаулау және беріктік.

L4 ядро ​​интерфейсінің бастапқы екілік интерфейсін әр түрлі қайта құру болды (ABI ) және оның ізбасарлары, соның ішінде L4Ka :: Пісте (Юни Карлсруэ ), L4 / MIPS (UNSW ), Фиаско (Дрезден ). Осы себепті аты L4 жалпыланған және енді Лидтенің алғашқы іске асырылуына ғана қатысты емес. Ол енді толығымен қолданылады микро ядро отбасы, соның ішінде L4 ядро интерфейс және оның әр түрлі нұсқалары.

L4 кеңінен таралған. Бір нұсқа, OKL4 Ядро зертханаларын ашыңыз, миллиардтаған мобильді құрылғыларға жеткізілді.[1][2]

Дизайн парадигмасы

А туралы жалпы идеяны көрсету микро ядро, Лидтке айтады:

Микро ядро ​​ішінде концепцияға ядро ​​сыртында қозғалған жағдайда ғана жол беріледі, яғни бәсекелес жүзеге асыруға рұқсат беру жүйенің қажетті функционалдығын іске асыруға кедергі келтіреді.[3]

Бұл тұрғыда L4 микро ядросы бірнеше негізгі механизмдерді ұсынады: мекенжай кеңістігі (бет кестелерін рефераттау және жадты қорғауды қамтамасыз ету), жіптер және жоспарлау (абстракциялау және уақытша қорғауды қамтамасыз ету), және процесаралық байланыс (оқшаулау шекаралары арқылы басқарылатын байланыс үшін).

L4 сияқты микро ядроларға негізделген операциялық жүйе серверлер ретінде қызмет көрсетеді пайдаланушы кеңістігі бұл монолитті ядролар сияқты Linux немесе аға буынның микро ядролары ішіне кіреді. Мысалы, қауіпсізді енгізу үшін Unix тәрізді жүйе, серверлер құқықтарды басқаруды қамтамасыз етуі керек Мах ядроның ішіне кіреді.

Тарих

Сияқты бірінші буын микро-ядроларының нашар жұмысы Мах, бірқатар әзірлеушілерді 90-шы жылдардың ортасында бүкіл микро ядро ​​тұжырымдамасын қайта зерттеуге мәжбүр етті. Асинхронды-буферлеу коммуникация процесі Махта қолданылған тұжырымдама оның нашар жұмысының негізгі себептерінің бірі болды. Бұл Mach негізіндегі операциялық жүйелерді жасаушыларды файлдық жүйелер немесе драйверлер сияқты уақыт өте маңызды компоненттерді ядро ​​ішіне қайта оралтуға мәжбүр етті.[дәйексөз қажет ] Бұл өнімділік мәселелерін біраз жақсартқанымен, ол нағыз микро ядроның минималды тұжырымдамасын бұзады (және олардың басты артықшылықтарын жоққа шығарады).

Mach бөтелкесін егжей-тегжейлі талдау, басқалармен қатар, оның екенін көрсетті жұмыс жиынтығы тым үлкен: IPC коды кеңістіктің нашар орналасуын білдіреді; бұл тым көп нәтижеге әкеледі кэш жіберіп алады, олардың көпшілігі ядро ​​ішінде.[3] Бұл талдау тиімді микро ядро ​​жеткілікті кішігірім болуы керек деген принципті туғызды, бұл өнімділіктің маңызды кодының көп бөлігі (бірінші деңгей) кэшке сәйкес келеді (жақсырақ аталған кэштің аз бөлігі).

L3

Джохен Лидтке жақсы жобаланған жіңішке екенін дәлелдеу үшін жолға шықты IPC қабат, өнімділікке мұқият назар аудару және машинаға тән (платформадан тәуелсіз) дизайн нақты әлемдегі өнімділікті жақсартуға әкелуі мүмкін. Мачтың күрделі IPC жүйесінің орнына оның L3 микро ядросы хабарламаны қосымша үстеме ақысыз жай ғана жіберді. Қажетті қауіпсіздік саясатын анықтау және жүзеге асыру міндеттері болып саналды пайдаланушы кеңістігі серверлер. Ядро рөлі пайдаланушы деңгейіндегі серверлерге саясатты орындауға мүмкіндік беретін қажетті механизмді қамтамасыз етуде ғана болды. 1988 жылы жасалған L3 өзін қауіпсіз әрі сенімді көрсетті операциялық жүйе, мысалы, көптеген жылдар бойы қолданылған TÜV SÜD[дәйексөз қажет ].

L4 шежіресі

L4

L3-ті қолданудың біраз тәжірибесінен кейін Лидтке Махтың тағы бірнеше тұжырымдамалары орынсыз деп тұжырым жасады. Микро ядролардың тұжырымдамаларын одан әрі жеңілдете отырып, ол бірінші L4 ядросын жасады, ол ең алдымен жоғары өнімділікті ескере отырып жасалған. Әрбір өнімділікті азайту үшін барлық ядро ​​жазылған құрастыру тілі, және оның IPC-і Mach-тен 20 есе жылдам болды.[4] Өнімділіктің мұндай күрт артуы операциялық жүйелерде сирек кездесетін оқиға болып табылады және Лидтенің жұмысы бірқатар жаңа университеттер мен ғылыми-зерттеу институттарында, соның ішінде L4 негізіндегі жүйелерде L4 жаңа енгізілімдері мен жұмыстарының пайда болуына түрткі болды. IBM Лидтке 1996 жылы жұмыс істей бастады, TU Дрезден және UNSW. IBM компаниясында Уотсон атындағы зерттеу орталығы Лидтке және оның әріптестері жалпы L4 және микро ядроларға негізделген жүйелер бойынша зерттеулерді жалғастырды, әсіресе Sawmill OS.[5]

L4Ka :: фундук

1999 жылы Лидтке жүйелер архитектурасы тобын қабылдады Карлсруэ университеті, онда ол микро ядролық жүйелерді зерттеуді жалғастырды. Жоғары өнімділікті микро ядро ​​жоғары деңгейлі тілде құрылуы мүмкін деген тұжырымдаманың дәлелі ретінде топ дамыды L4Ka :: фундук, IA-32 және ARM негізіндегі машиналарда жұмыс істеген ядродың C ++ нұсқасы. Күш-жігер сәтті болды - өнімділігі әлі де қолайлы болды - және оны шығарумен ядролардың құрастыру тіліндегі таза нұсқалары тиімді түрде тоқтатылды.

L4 / Fiasco

L4Ka :: Hazelnut дамуымен қатар, 1998 жылы TUD операциялық жүйелер тобы: OS Дрезден (Дрезден технологиялық университеті) L4 / Fiasco деп аталатын L4 ядросының интерфейсін өз C ++ енгізуді дамыта бастады. Ядрода параллельдікке жол бермейтін L4Ka :: фундук пен оның ізбасары L4Ka :: Pistachio-дан айырмашылығы, бұл ядрода тек алдын-ала белгілі нүктелерде үзілістерге жол береді, L4 / Fiasco ең төменгі деңгейге жету үшін (өте қысқа атомдық операцияларды қоспағанда) толықтай басым болды кідіріс кідірісі. Бұл қажет деп саналды, өйткені L4 / Fiasco DROPS негізі ретінде пайдаланылады,[6] а нақты уақыт режимінде кезінде дамыған қабілетті операциялық жүйе Дрезден. Алайда, толықтай алдын-ала жасалынатын дизайнның күрделілігі Fiasco-дің кейінгі нұсқаларын алдын-ала алу нүктелерінің шектеулі санын қоспағанда, ядроны үзілістермен басқарудың дәстүрлі L4 тәсіліне оралуға мәжбүр етті.

Платформаның тәуелсіздігі

L4Ka :: Пісте

L4Ka :: Pistachio және Fiasco-дің жаңа нұсқалары шыққанға дейін, барлық L4 микро ядролары негізінен CPU архитектурасына жақын болды. L4 дамуындағы келесі үлкен өзгеріс - бұл портативтіліктің жоғары деңгейіне қарамастан, жоғары өнімділік сипаттамаларын сақтаған, тәуелсіз платформаны құру. Ядроның негізгі тұжырымдамалары бірдей болғанымен, жаңа API алдыңғы L4 нұсқаларына қатысты көптеген маңызды өзгерістерді, соның ішінде көп процессорлы жүйелерді жақсы қолдауды, ағындар мен адрестік кеңістіктер арасындағы байланыстарды босатуды және пайдаланушы деңгейіндегі тізбекті басқаруды енгізуді қамтамасыз етті. блоктар (UTCB) және виртуалды регистрлер. 2001 жылдың басында жаңа L4 API (X.2 нұсқасы, 4-нұсқа) шығарғаннан кейін Карлсруэ Университетіндегі жүйелік архитектура тобы жаңа ядро ​​енгізді, L4Ka :: Пісте, толығымен нөлден, енді жоғары өнімділікке де, портативтілікке де назар аударамыз. Ол астында шығарылды екі тармақты BSD лицензиясы.

Фиасконың жаңа нұсқалары

L4 / Fiasco микро ядросы да осы жылдар ішінде кеңейтілген. Ол x86-дан AMD64-ке дейін бірнеше ARM платформаларына дейінгі бірнеше аппараттық платформаларды қолдайды. Fiasco (Fiasco-UX) нұсқасы Linux деңгейінде қолданушы деңгейіндегі қосымша ретінде жұмыс істей алады.

L4 / Fiasco L4v2 API бірнеше кеңейтімдерін жүзеге асырады. Ерекше IPC ядроларға процессордың ерекшеліктерін пайдаланушы деңгейіндегі өңдеуші қосымшаларына жіберуге мүмкіндік береді. Көмегімен шетелдік жіптер жүйелік қоңырауларға нақты бақылауды жүзеге асыруға болады. X.2 стиліндегі UTCB қосылды. Сонымен қатар, Fiasco коммуникациялық құқықтарды, сондай-ақ ядро ​​деңгейіндегі ресурстарды тұтынуды басқару тетіктерін қамтиды. Фиасконың жоғарғы жағында пайдаланушылар деңгейінің базалық қызметтерінің жиынтығы әзірленді (L4Env деп аталады), басқалары арасында Linux-тың ағымдағы нұсқасын параллельдеу үшін қолданылады (2019 ж. Мамырдағы 4.19) L4Linux ).

Жаңа Оңтүстік Уэльс университеті және NICTA

Даму, сондай-ақ өтті Жаңа Оңтүстік Уэльс университеті (UNSW), мұнда әзірлеушілер L4-ді бірнеше 64 биттік платформаларға енгізді. Олардың жұмысы нәтиже берді L4 / MIPS және L4 / Альфанәтижесінде Лидткенің түпнұсқа нұсқасы ретроспективті түрде аталды L4 / x86. Liedtke-дің түпнұсқа ядролары сияқты, UNSW ядролары (құрастыру және С қоспасында жазылған) мүмкін емес және әрқайсысы нөлден іске асырылды. Жоғары портативті L4Ka :: Pistachio шығарылған кезде, UNSW тобы L4Ka :: Pistachio порттарын шығарудың пайдасына өздерінің ядроларынан бас тартты, соның ішінде хабарларды жылдам жіберу (36 цикл бойынша) Итан сәулет).[7] Топ сонымен қатар пайдаланушы деңгейіндегі құрылғы драйверлері ядро ​​ішіндегі драйверлер сияқты жұмыс істей алатындығын көрсетті,[8] және дамыған Вомбат, жоғары портативті нұсқасы Linux x86, ARM және MIPS процессорларында жұмыс істейтін L4-те. Қосулы XScale өңдеушілер, Вомбат жергілікті Linux-тен 50 есеге дейін төмен контекстті ауыстыру шығындарын көрсетеді.[9]

Кейінірек UNSW тобы, олардың жаңа үйінде NICTA, L4Ka :: Pistachio деп аталатын жаңа L4 нұсқасына айырылды NICTA :: L4 ендірілген. Атауынан көрініп тұрғандай, бұл коммерциялық ендірілген жүйелерде қолдануға бағытталған, демек, сауда-саттық шағын жадтың іздерін жақсартып, күрделілікті азайтуға бағытталған. Жүйелік қоңыраулардың барлығын дерлік қысқа етіп ұстап тұру үшін API өзгертілді, сондықтан нақты уақыт режимінде жоғары жылдамдықты қамтамасыз ету үшін алдын-ала ұпай қажет емес.[10]

Коммерциялық орналастыру

2005 жылдың қарашасында, NICTA жарияланды[11] бұл Qualcomm оларға NICTA-дің L4 нұсқасын орналастырды Мобильді станция модемі чипсет. Бұл L4-ті қолдануға әкелді ұялы телефон 2006 жылдың соңынан бастап сатылатын телефондар. 2006 жылдың тамызында ERTOS жетекшісі және UNSW профессоры Gernot Heiser атты компанияны шығарды Ядро зертханаларын ашыңыз (OK зертханалары) коммерциялық L4 пайдаланушыларына қолдау көрсету және L4 маркасын коммерциялық мақсатта брендтік атпен дамыту OKL4, NICTA-мен тығыз ынтымақтастықта. 2008 жылдың сәуірінде шыққан OKL4 2.1 нұсқасы бірінші болды жалпы қол жетімді ұсынылған L4 нұсқасы мүмкіндікке негізделген қауіпсіздік. OKL4 3.0, 2008 жылдың қазанында шығарылды, OKL4-тің соңғы ашық бастапқы нұсқасы болды. Соңғы нұсқалары жабық көз болып табылады және OKL4 Microvisor деп аталатын жергілікті гипервизор нұсқасын қолдау үшін қайта жазуға негізделген. OK зертханалары сонымен қатар ОК деп аталатын паравируалдандырылған Linux таратты: Linux, Wombat ұрпағы, сонымен қатар паравирализацияланған нұсқалары SymbianOS және Android. OK зертханалары да құқықты алды seL4 NICTA-дан.

2012 жылдың басында OKL4 жеткізілімдері 1,5 миллиардтан асты,[2] көбінесе Qualcomm сымсыз модем чиптерінде. Басқа орналастырулар кіреді автомобильдік ойын-сауық жүйелер.[12]

Apple A сериясы бастап басталатын процессорлар A7 құрамында қауіпсіз анклав бар сопроцессор L4 амалдық жүйесін іске қосу[13]L4 ендірілген ядросы негізінде жасалған NICTA 2006 жылы.[14]Бұл L4-дің барлық iOS құрылғыларында жеткізілуін білдіреді, олардың жалпы жеткізілімі 2015 жылға 310 млн.[15]

Жоғары сенімділік: seL4

2006 жылы NICTA тобы а-дан жобалауды бастады үшінші ұрпақ микро ядросы сияқты seL4 деп аталатын, қауіпсіздік талаптарын қанағаттандыруға жарамды, жоғары қауіпсіз және сенімді жүйелер үшін негіз жасау мақсатында Жалпы критерийлер және одан тыс жерлерде. Даму басынан бастап бағытталған ресми тексеру ядро. Өнімділік пен тексерудің кейде қарама-қайшы талаптарын қанағаттандыру үшін, команда а ортаңғы бағдарламалық жасақтама орындалатын спецификация жазылған Хаскелл.[16]seL4 қолданады мүмкіндікке негізделген қол жетімділікті басқару объектінің қол жетімділігі туралы формальды дәлелдеуді қосу.

Функционалды дұрыстығының ресми дәлелі 2009 жылы аяқталды.[17]Дәлел ядроның орындалуы оның сипаттамасына сәйкес дұрыс екендігіне кепілдік береді және оның тұйықталу сияқты қателіктерден босатылатындығын білдіреді, тірі құлыптар, буферден асып кету, арифметикалық ерекшеліктер немесе инициализацияланбаған айнымалыларды пайдалану. seL4 - бұл бірінші рет тексерілген жалпы мақсаттағы операциялық жүйенің ядросы.[17]

seL4 ядролық ресурстарды басқаруға жаңа көзқараспен қарайды,[18] ядро ресурстарын басқаруды пайдаланушы деңгейіне экспорттау және оларды бірдей бағындыру мүмкіндікке негізделген пайдаланушы ресурстары ретінде қатынасты басқару. Сондай-ақ қабылданған бұл модель Бөшке, оқшаулау қасиеттері туралы пайымдауды жеңілдетеді және seL4 тұтастық пен құпиялылықтың негізгі қауіпсіздік қасиеттерін күшейтетін кейінгі дәлелдерге мүмкіндік берді.[19] NICTA тобы сонымен бірге C-ден орындалатын машиналық кодқа аударудың дұрыстығын дәлелдеді құрастырушы ішінен сенімді есептеу базасы seL4. Бұл ядро ​​үшін қауіпсіздіктің жоғары деңгейінің дәлелі орындалатындығын білдіреді. seL4 - бұл толық және дыбыстық сипаттағы алғашқы жарияланған қорғалған ОЖ ядросы ең нашар жағдайда орындау уақыты (WCET) талдау, оны қатты қолдану үшін алғышарт нақты уақыт жүйелері.[19]

2014 жылғы 29 шілдеде, NICTA және General Dynamics C4 жүйелері соңына дейін дәлелдермен seL4 енді шығарылды деп жариялады бастапқы коды ашық лицензиялар.[20]Ядро көзі және дәлелдері астында GPLv2 және көптеген кітапханалар мен құралдар 2 тармақтан тұратын BSD лицензиясына сәйкес келеді.

Зерттеушілер ресми бағдарламалық қамтамасыздандырудың бағасы әлдеқайда сенімді нәтижелерге қол жеткізгенімен, дәстүрлі «жоғары сенімділік» бағдарламалық қамтамасыздандырудың бағасынан төмен екенін айтады.[21] Нақтырақ айтсақ, біреуінің құны кодтың сызығы seL4 дамуы кезінде шамамен бағаланды 400 АҚШ доллары, салыстырғанда 1000 АҚШ доллары дәстүрлі жоғары сенімділік жүйелері үшін.[22]

Астында ДАРПА Жоба серіктестерімен бірге NICTA жоғары сенімділікті кибер әскери жүйелер (HACMS) бағдарламасы Рокуэлл Коллинз, Galois Inc, Миннесота университеті және Боинг жоспарланған технологияны ерікті түрде пилотталған автономды режимге ауыстыра отырып, басқа сенімділік құралдары мен бағдарламалық жасақтамаларымен бірге seL4 негізінде жоғары сенімділікті ұшақ жасады Ұшқышсыз кішкентай құс Boeing әзірлеп жатқан тікұшақ. HACMS технологиясының соңғы демонстрациясы Стерлингте, ВА-да 2017 жылдың сәуірінде өтті.[23] DARPA бірнеше қаржыландырды Шағын кәсіпкерлікті инновациялық зерттеу Доктор бастаған бағдарлама шеңберінде (SBIR) seL4-ке қатысты келісімшарттар. Джон Ланчбери. SeL4-ке байланысты SBIR алатын шағын бизнеске: DornerWorks, Techshot, Wearable Inc, Real Time Innovations және Critical Technologies кіреді.[24]

Басқа зерттеулер мен әзірлемелер

Osker, жазылған OS Хаскелл, L4 сипаттамасына бағытталған; дегенмен, бұл жоба а функционалды бағдарламалау Микро ядролық зерттеулерге емес, ОЖ-ны дамытуға арналған тіл.[25]

CodeZero - виртуалдандыруға және отандық ОС қызметтерін енгізуге бағытталған кіріктірілген жүйелерге бағытталған L4 микро ядролары. Бар GPL - лицензияланған нұсқа,[26] және әзірлеушілер жабық ақпарат көзі ретінде рисензияланған және 2010 жылы айырылған нұсқасы.[27]

F9 микро ядросы,[28] BSD лицензияланған L4 енгізу, арналған ARM Cortex-M жадты қорғаумен терең ендірілген құрылғыларға арналған процессорлар.

NOVA OS виртуалдандыру архитектурасы - бұл қауіпсіз және тиімді виртуалдандыру ортасын құруға бағытталған ғылыми жоба[29][30]шағын сенімді есептеу базасымен. NOVA микрохипервайзерден, пайдаланушы деңгейінен тұрады виртуалды-машиналық монитор, және NUL деп аталатын, оның үстінде жұмыс жасайтын, артықшылығы жоқ компоненттелген көп серверлі орта. NOVA x86 негізіндегі көп ядролы жүйелерде жұмыс істейді.

WrmOS[31] бұл L4 микро ядросына негізделген нақты уақыттағы операциялық жүйе. Оның SPARC, ARM, x86 және x86_64 архитектураларын қолдайтын ядролардың, стандартты кітапханалардың және желілік стектің жеке енгізілімдері бар. Паравиризацияланған Linux ядросы бар (w4linux)[32]) WrmOS үстінде жұмыс істеу.

Әдебиеттер тізімі

  1. ^ «Hypervisor өнімдері - General Dynamics Mission Systems». gdmissionsystems.com. Мұрағатталды түпнұсқадан 2017 жылғы 15 қарашада. Алынған 26 сәуір 2018.
  2. ^ а б «Ашық ядролық зертханалық бағдарламалық қамтамасыз ету мобильді құрылғылардың жеткізілімі бойынша 1,5 миллиардтан асып түсті» (Баспасөз хабарламасы). Ядро зертханаларын ашыңыз. 19 қаңтар 2012. Мұрағатталған түпнұсқа 2012 жылғы 11 ақпанда.
  3. ^ а б Лидтке, Джохен (Желтоқсан 1995). «Ядролық құрылыс туралы». Proc. Операциялық жүйелердің принциптері бойынша 15-ші ACM симпозиумы (SOSP). 237–250 бб. Мұрағатталды түпнұсқадан 2015 жылғы 25 қазанда.
  4. ^ Лидтке, Джохен (Желтоқсан 1993). «IPC-ді ядро ​​дизайны бойынша жетілдіру». Операциялық жүйенің принциптері бойынша 14-ші ACM симпозиумы. Ашевилл, NC, АҚШ. 175–88 беттер.
  5. ^ Геффлаут, Ален; Джагер, Трент; Парк, Юнхо; Лидтке, Джохен; Элфинстон, Кевин; Ухлиг, Волкмар; Тидсвелл, Джонатон; Деллер, Люк; Ройтер, Ларс (2000). «Sawmill мультисерверлік тәсілі». ACM SIGOPS Еуропалық семинары. Колдинг, Дания. 109–114 бб.
  6. ^ «Мұрағатталған көшірме». Мұрағатталды түпнұсқасынан 2011-08-07 ж. Алынған 2011-08-10.CS1 maint: тақырып ретінде мұрағатталған көшірме (сілтеме)
  7. ^ Сұр, Чарльз; Чэпмен, Мэттью; Чубб, Питер; Мосбергер-Тан, Дэвид; Хейзер, Герно (Сәуір 2005). «Итан - жүйені жүзеге асырушының ертегісі». USENIX жыл сайынғы техникалық конференциясы. Аннахайм, Калифорния, АҚШ. 264–278 беттер. Мұрағатталды 2007-02-17 аралығында түпнұсқадан.
  8. ^ Лесли, Бен; Чубб, Питер; ФицРой-Дейл, Николас; Гётц, Стефан; Сұр, Чарльз; Макферсон, Люк; Поттс, Даниел; Шен, Юэтинг; Элфинстон, Кевин; Хейзер, Герно (Қыркүйек 2005). «Пайдаланушы деңгейіндегі құрылғы драйверлері: қол жеткізілген өнімділік». Информатика және технологиялар журналы. 20 (5): 654–664. CiteSeerX  10.1.1.59.6766. дои:10.1007 / s11390-005-0654-4. S2CID  1121537.
  9. ^ ван Шайк, Карл; Хейзер, Герно (Қаңтар 2007). «ARM және сегменттелген архитектуралардағы өнімділігі жоғары микронутналар және виртуалдандыру». Кіріктірілген жүйелерге арналған микрожүйелер бойынша 1-ші халықаралық семинар. Сидней, Австралия: NICTA. 11-21 бет. Мұрағатталды түпнұсқасынан 2015-03-01. Алынған 2015-10-25.
  10. ^ Руокко, Серхио (қазан 2008). «Нақты уақыттағы бағдарламашының туристік мақсаттағы L4 микроэлементтерінің туры». Енгізілген жүйелер туралы EURASIP журналы. 2008: 1–14. дои:10.1155/2008/234710. S2CID  7430332.
  11. ^ «NICTA L4 микро ядролы таңдау QUALCOMM чипсет шешімдерінде қолданылады» (Баспасөз хабарламасы). NICTA. 24 қараша 2005 ж. Мұрағатталған түпнұсқа 2006 жылы 25 тамызда.
  12. ^ «Bosch ақпараттық ойын-сауық жүйелері үшін таңдалған ашық ядролық зертханалық машиналық виртуализация» (Баспасөз хабарламасы). Ядро зертханаларын ашыңыз. 27 наурыз 2012 ж. Мұрағатталған түпнұсқа 2012 жылғы 2 шілдеде.
  13. ^ «iOS қауіпсіздігі, iOS 12.3» (PDF). Apple Inc. мамыр 2019.
  14. ^ Мандт, Тардей; Солник, Мэттью; Ванг, Дэвид (31 шілде, 2016). «Қауіпсіз анклавтық процессордың демистификациясы» (PDF). BlackHat АҚШ. Лас-Вегас, НВ, АҚШ. Мұрағатталды (PDF) түпнұсқадан 2016 жылғы 21 қазанда.
  15. ^ Элмер-Дэвит, Филипп (28 қазан, 2014). «Болжам: Apple 2015 жылы 310 миллион iOS құрылғысын жеткізеді». Сәттілік. Мұрағатталды түпнұсқадан 2015 жылғы 27 қыркүйекте. Алынған 25 қазан, 2015.
  16. ^ Деррин, Филип; Элфинстон, Кевин; Клейн, Гервин; Әтеш; Дэвид; Чакраварти, Мануэль М. Т. (қыркүйек 2006). «Нұсқаулықты қолдану: жоғары сенімділікті микро ядроларды дамытуға көзқарас». ACM SIGPLAN Haskell шеберханасы. Портленд, Орегон. 60-71 бет.
  17. ^ а б Клейн, Гервин; Элфинстон, Кевин; Хейзер, Герно; Андроник, маусым; Кок, Дэвид; Деррин, Филип; Элкадуве, Даммика; Энгельхардт, Кай; Колански, Рафал; Норриш, Майкл; Сьюэлл, Томас; Туч, Харви; Уинвуд, Саймон (қазан 2009). «seL4: ОЖ ядросының ресми тексерісі» (PDF). Операциялық жүйенің принциптері бойынша 22-ACM симпозиумы. Big Sky, MT, АҚШ. Мұрағатталды (PDF) түпнұсқасынан 2011-07-28.
  18. ^ Элкадуве, Даммика; Деррин, Филип; Элфинстон, Кевин (сәуір, 2008). Физикалық жадыны оқшаулауға және қамтамасыз етуге арналған ядро ​​дизайны. Ендірілген жүйелердегі оқшаулау және интеграциялау бойынша 1-ші семинар. Глазго, Ұлыбритания. дои:10.1145/1435458. Алынған 2020-02-22.
  19. ^ а б Клейн, Гервин; Андроник, маусым; Элфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафал; Хейзер, Герно (ақпан 2014). «ОЖ микро ядроларын кешенді формальды тексеру». Компьютерлік жүйелердегі ACM транзакциялары. 32 (1): 2:1–2:70. CiteSeerX  10.1.1.431.9140. дои:10.1145/2560537. S2CID  4474342.
  20. ^ «NICTA жасаған қауіпсіз операциялық жүйе ашық қайнар көзге айналды» (Баспасөз хабарламасы). NICTA. 2014 жылғы 29 шілде. Мұрағатталды түпнұсқадан 2016 жылғы 15 наурызда.
  21. ^ Клейн, Гервин; Андроник, маусым; Элфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафал; Хейзер, Герно (2014). «ОЖ микро ядроларын кешенді ресми тексеру» (PDF). Компьютерлік жүйелердегі ACM транзакциялары. 32: 64. CiteSeerX  10.1.1.431.9140. дои:10.1145/2560537. S2CID  4474342. Мұрағатталды (PDF) түпнұсқасынан 2014-08-03.
  22. ^ seL4 тегін - бұл сіз үшін нені білдіреді? қосулы YouTube
  23. ^ «DARPA киберқауіпсіздік технологиясын жаңа платформаларға қолдану үшін Рокуэлл Коллинзді таңдайды» (Баспасөз хабарламасы). Рокуэлл Коллинз. 24 сәуір, 2017. Мұрағатталды түпнұсқадан 2017 жылғы 11 мамырда.
  24. ^ «DARPA агенттігінің демеушісі доктор Джон Лончбери». SBIRSource. 2017. Мұрағатталды түпнұсқасынан 2017 жылғы 29 қыркүйекте. Алынған 16 мамыр, 2017.
  25. ^ Халлгрен, Т .; Джонс, М.П .; Лесли, Р .; Толмач, А. (2005). «Хаскеллде операциялық жүйені құруға принципиалды көзқарас» (PDF). Функционалды бағдарламалау бойынша оныншы ACM SIGPLAN халықаралық конференциясының материалдары. 40 (9): 116–128. дои:10.1145/1090189.1086380. ISSN  0362-1340. Мұрағатталды (PDF) түпнұсқадан 2010-06-15. Алынған 2010-06-24.
  26. ^ «jserv / codezero: Codezero Microkernel». Мұрағатталды түпнұсқасынан 2015-08-15. Алынған 2020-10-20.
  27. ^ «Мұрағатталған көшірме». Архивтелген түпнұсқа 2016 жылдың 11 қаңтарында. Алынған 25 қаңтар, 2016.CS1 maint: тақырып ретінде мұрағатталған көшірме (сілтеме)
  28. ^ «F9 микро ядролы». Алынған 2020-10-20.
  29. ^ Стейнберг, Удо; Кауер, Бернхард (сәуір 2010). «NOVA: Microhypervisor негізіндегі қауіпсіз виртуалдандыру архитектурасы». EuroSys '10: компьютерлік жүйелер бойынша 5-ші еуропалық конференция материалдары. Париж, Франция.
  30. ^ Стейнберг, Удо; Кауер, Бернхард (сәуір 2010). «Пайдаланушы деңгейіндегі ауқымды мультипроцессорлық ортаға қарай». IIDS'10: Оқшаулану және сенімді жүйелер үшін интеграциялау бойынша семинар. Париж, Франция.
  31. ^ «WrmOS». Алынған 2020-10-20.
  32. ^ «w4linux - бұл пармиртуалданған, Linux ядросы, WrmOS үстінде жұмыс істейді». Алынған 2020-10-20.

Әрі қарай оқу

Сыртқы сілтемелер