Из Википедии, бесплатной энциклопедии
  (Перенаправлено из Fiasco (клон L4) )
Перейти к навигации Перейти к поиску

L4 - это семейство микроядер второго поколения , обычно используемых для реализации Unix-подобных операционных систем , но также используемых во множестве других систем.

L4, как и его предшественник микроядро L3 , был создан немецким компьютерным ученым Йохеном Лидтке в ответ на низкую производительность более ранних операционных систем на основе микроядра. Лидтке считал, что система, разработанная с самого начала для обеспечения высокой производительности, а не для других целей, может создать микроядро для практического использования. Его первоначальная реализация в коде на языке ассемблера для Intel i386, написанном вручную, в 1993 году вызвала большой интерес в компьютерной индустрии. [ необходима цитата ] С момента своего появления L4 был разработан для обеспечения независимости от платформы, а также для улучшения безопасности , изоляции инадежность .

Были различные повторные реализации исходного двоичного интерфейса ядра L4 ( ABI ) и его преемников, включая L4Ka :: Pistachio ( Uni Karlsruhe ), L4 / MIPS ( UNSW ), Fiasco ( TU Dresden ). По этой причине название L4 было обобщено и больше не относится только к исходной реализации Лидтке. Теперь он применяется ко всему семейству микроядра, включая интерфейс ядра L4 и его различные версии.

L4 широко распространен. Один вариант, OKL4 от Open Kernel Labs , был доставлен в миллиарды мобильных устройств. [1] [2]

Парадигма дизайна [ править ]

Уточняя общую идею микроядра , Лидтке утверждает:

Концепция допускается внутри микроядра только в том случае, если ее перенос за пределы ядра, т. Е. Разрешение конкурирующих реализаций, помешает реализации требуемых функциональных возможностей системы. [3]

В этом духе микроядро L4 предоставляет несколько основных механизмов: адресные пространства (абстрагирование таблиц страниц и обеспечение защиты памяти), потоки и планирование (абстрагирование выполнения и обеспечение временной защиты) и межпроцессное взаимодействие (для контролируемого взаимодействия через границы изоляции).

Операционная система, основанная на микроядре, таком как L4, предоставляет услуги в качестве серверов в пользовательском пространстве, которые монолитные ядра, такие как Linux или микроядра старого поколения, включают внутри себя. Например, чтобы реализовать безопасную Unix-подобную систему, серверы должны обеспечивать управление правами, которое Mach включил в ядро.

История [ править ]

Низкая производительность микроядер первого поколения, таких как Mach , заставила ряд разработчиков пересмотреть всю концепцию микроядра в середине 1990-х годов. Используемая в Mach концепция асинхронной буферизации процесса внутри ядра оказалась одной из основных причин его низкой производительности. Это побудило разработчиков операционных систем на базе Mach переместить некоторые критичные ко времени компоненты, такие как файловые системы или драйверы, обратно внутрь ядра. [ необходима цитата ] Хотя это несколько улучшило проблемы с производительностью, это явно нарушает концепцию минимальности настоящего микроядра (и упускает их основные преимущества).

Детальный анализ узкого места Маха показал, что, среди прочего, его рабочий набор слишком велик: код IPC выражает плохую пространственную локальность; то есть, это приводит к слишком большому количеству промахов в кэше , большинство из которых в ядре. [3] Этот анализ привел к появлению принципа, согласно которому эффективное микроядро должно быть достаточно маленьким, чтобы большая часть критически важного для производительности кода помещалась в кэш (первого уровня) (предпочтительно небольшую часть указанного кеша).

L3 [ править ]

Йохен Лидтке намеревался доказать, что хорошо спроектированный более тонкий слой IPC с особым вниманием к производительности и машинно-ориентированному (в отличие от независимого от платформы) дизайну может привести к значительному повышению производительности в реальном мире. Вместо сложной системы IPC Маха его микроядро L3 просто передавало сообщение без каких-либо дополнительных накладных расходов. Определение и реализация необходимых политик безопасности считались обязанностями серверов пользовательского пространства . Роль ядра заключалась только в обеспечении необходимого механизма, позволяющего серверам пользовательского уровня применять политики. L3, разработанный в 1988 году, зарекомендовал себя как безопасную и надежную операционную систему , используется на протяжении многих лет, например с помощью TÜV SÜD [ править] .

L4 генеалогическое древо

L4 [ править ]

После некоторого опыта использования L3 Лидтке пришел к выводу, что несколько других концепций Маха также неуместны. Еще больше упростив концепции микроядра, он разработал первое ядро ​​L4, которое в первую очередь проектировалось с учетом высокой производительности. Чтобы выжать каждый бит производительности, все ядро ​​было написано на языке ассемблера , и его IPC был в 20 раз быстрее, чем у Маха. [4] Такое резкое повышение производительности - редкое явление для операционных систем, и работа Лидтке привела к появлению новых реализаций L4 и работы над системами на основе L4 в ряде университетов и исследовательских институтов, включая IBM , где Лидтке начал работать в 1996 г. Дрезден и UNSW. В исследовательском центре Томаса Дж. Ватсона IBMЛидтке и его коллеги продолжили исследования систем на базе L4 и микроядра в целом, особенно ОС Sawmill. [5]

L4Ka :: Hazelnut [ править ]

В 1999 году Лидтке возглавил группу системной архитектуры в Университете Карлсруэ , где продолжил исследования в области микроядерных систем. В качестве доказательства концепции того, что высокопроизводительное микроядро также может быть построено на языке более высокого уровня, группа разработала L4Ka :: Hazelnut , версию ядра C ++, работающую на машинах на базе IA-32 и ARM. Усилия увенчались успехом - производительность оставалась приемлемой - и с его выпуском версии ядер на чистом языке ассемблера были фактически прекращены.

L4 / Fiasco [ править ]

Параллельно с разработкой L4Ka :: Hazelnut в 1998 году Группа операционных систем TUD: OS Технического университета Дрездена (Дрезденский технологический университет) начала разрабатывать собственную реализацию C ++ интерфейса ядра L4, названную L4 / Fiasco. В отличие от L4Ka :: Hazelnut, который вообще не допускает параллелизма в ядре, и его преемника L4Ka :: Pistachio, который разрешает прерывания в ядре только в определенных точках вытеснения, L4 / Fiasco был полностью вытеснен (за исключением чрезвычайно короткие атомарные операции) для достижения низкой задержки прерывания . Это было сочтено необходимым, потому что L4 / Fiasco используется в качестве основы DROPS, [6] операционной системы с поддержкой жесткого реального времени , также разработанной вТУ Дрезден . Однако сложность полностью вытесняемого проекта побудила более поздние версии Fiasco вернуться к традиционному подходу L4, когда ядро ​​запускалось с отключенными прерываниями, за исключением ограниченного числа точек вытеснения.

Независимость от платформы [ править ]

L4Ka :: Фисташка [ править ]

Вплоть до выпуска L4Ka :: Pistachio и более новых версий Fiasco все микроядра L4 по своей сути были привязаны к базовой архитектуре ЦП. Следующим большим сдвигом в разработке L4 стала разработка платформенно-независимого API, который все еще сохранял высокие характеристики производительности, несмотря на более высокий уровень переносимости. Хотя базовые концепции ядра остались прежними, новый API предоставил множество значительных изменений по сравнению с предыдущими версиями L4, включая лучшую поддержку многопроцессорных систем, более слабые связи между потоками и адресными пространствами и введение управления потоками на уровне пользователя. блоки (UTCB) и виртуальные регистры. После выпуска нового L4 API (версия X.2, также известная как версия 4) в начале 2001 года, группа системной архитектуры Университета Карлсруэ внедрила новое ядро,L4Ka :: Pistachio , полностью с нуля, теперь с упором как на высокую производительность, так и на портативность. Он был выпущен под лицензией BSD, состоящей из двух пунктов .

Более новые версии Fiasco [ править ]

Микроядро L4 / Fiasco также значительно улучшилось за эти годы. Теперь он поддерживает несколько аппаратных платформ от x86 до AMD64 до нескольких платформ ARM. Примечательно, что версия Fiasco (Fiasco-UX) может работать как приложение пользовательского уровня поверх Linux.

L4 / Fiasco реализует несколько расширений API L4v2. IPC исключения позволяет ядру отправлять исключения ЦП приложениям-обработчикам на уровне пользователя. С помощью чужих потоков можно осуществлять детальный контроль над системными вызовами. Добавлены UTCB в стиле X.2. Кроме того, Fiasco содержит механизмы для управления правами связи, а также потреблением ресурсов на уровне ядра. На вершине Fiasco разработан набор базовых сервисов пользовательского уровня (называемых L4Env), которые, среди прочего, используются для паравиртуализации текущей версии Linux (4.19 по состоянию на май 2019 года) (называемой L 4 Linux ).

Университет Нового Южного Уэльса и NICTA [ править ]

Разработка также велась в Университете Нового Южного Уэльса (UNSW), где разработчики реализовали L4 на нескольких 64-битных платформах. Результатом их работы стали L4 / MIPS и L4 / Alpha , в результате чего оригинальная версия Лидтке была ретроспективно названа L4 / x86 . Как и исходные ядра Liedtke, ядра UNSW (написанные на смеси ассемблера и C) были непереносимыми, и каждое реализовывалось с нуля. С выпуском сверхпортативного L4Ka :: Pistachio группа UNSW отказалась от собственных ядер в пользу создания хорошо настроенных портов L4Ka :: Pistachio, включая самую быструю из когда-либо зарегистрированных реализаций передачи сообщений (36 циклов на архитектуре Itanium ) . [7]Группа также продемонстрировала, что драйверы устройств пользовательского уровня могут работать так же, как драйверы в ядре [8], и разработала Wombat , очень портативную версию Linux на L4, которая работает на процессорах x86, ARM и MIPS. На процессорах XScale Wombat демонстрирует затраты на переключение контекста, которые до 50 раз ниже, чем в родном Linux. [9]

Позже группа UNSW в своем новом доме в NICTA разделила L4Ka :: Pistachio на новую версию L4 под названием NICTA :: L4-embedded . Как следует из названия, это было предназначено для использования в коммерческих встроенных системах, и, следовательно, компромиссы при реализации благоприятствовали небольшому объему памяти и были направлены на снижение сложности. API был изменен так, чтобы почти все системные вызовы оставались достаточно короткими, чтобы им не требовались точки прерывания для обеспечения высокой скорости отклика в реальном времени. [10]

Коммерческое развертывание [ править ]

В ноябре 2005 года NICTA объявила [11], что Qualcomm развертывает версию NICTA L4 на своих наборах микросхем модемов мобильных станций . Это привело к использованию L4 в мобильных телефонах, продаваемых с конца 2006 года. В августе 2006 года лидер ERTOS и профессор UNSW Гернот Хайзер создал компанию под названием Open Kernel Labs (OK Labs) для поддержки коммерческих пользователей L4 и дальнейшего развития L4 для коммерческое использование под торговой маркой OKL4 в тесном сотрудничестве с NICTA. OKL4 Version 2.1, выпущенная в апреле 2008 года, была первой общедоступной версией L4, которая обеспечивала безопасность на основе возможностей.. OKL4 3.0, выпущенный в октябре 2008 года, был последней версией OKL4 с открытым исходным кодом. Более поздние версии имеют закрытый исходный код и основаны на переписывании для поддержки собственного варианта гипервизора, называемого микровизором OKL4. OK Labs также распространяла паравиртуализированный Linux под названием OK: Linux, потомок Wombat, а также паравиртуализированные версии SymbianOS и Android . OK Labs также приобрела права на seL4 у NICTA.

В начале 2012 года поставки OKL4 превысили 1,5 миллиарда, [2] в основном это были микросхемы беспроводных модемов Qualcomm. Другие варианты развертывания включают автомобильные информационно-развлекательные системы. [12]

Процессоры Apple серии A , начиная с A7, содержат сопроцессор Secure Enclave, работающий под управлением операционной системы L4 [13] на основе встроенного ядра L4, разработанного в NICTA в 2006 году. [14] Это означает, что L4 теперь поставляется на всех устройствах iOS, т.е. общий объем поставок которых оценивается в 310 миллионов на 2015 год. [15]

Высокая гарантия: seL4 [ править ]

В 2006 году группа NICTA начала с нуля проектирование микроядра третьего поколения , названного seL4, с целью создания основы для высоконадежных и высоконадежных систем, подходящих для удовлетворения требований безопасности, таких как Common Criteria и выше. С самого начала разработка была направлена ​​на формальную проверку ядра. Чтобы упростить выполнение иногда противоречивых требований к производительности и проверке, команда использовала промежуточный программный процесс, начиная с исполняемой спецификации, написанной на Haskell . [16] seL4 использует управление доступом на основе возможностей. для формального рассуждения о доступности объекта.

Формальное доказательство функциональной корректности было завершено в 2009 году. [17] Доказательство обеспечивает гарантию того, что реализация ядра соответствует его спецификации, и подразумевает, что оно не содержит ошибок реализации, таких как взаимоблокировки, живые блокировки , переполнение буфера, арифметические исключения и т. Д. использование неинициализированных переменных. seL4 считается первым в истории ядром операционной системы общего назначения, которое было проверено. [17]

seL4 использует новый подход к управлению ресурсами ядра [18], экспортируя управление ресурсами ядра на уровень пользователя и подвергая их тому же управлению доступом на основе возможностей, что и пользовательским ресурсам. Эта модель, которая также была принята Barrelfish , упрощает рассуждения о свойствах изоляции и использовалась для более поздних доказательств того, что seL4 обеспечивает соблюдение основных свойств безопасности, таких как целостность и конфиденциальность. [19] Команда NICTA также подтвердила правильность перевода с C в исполняемый машинный код, исключив компилятор из надежной вычислительной базы seL4. [20]Это означает, что для исполняемого файла ядра сохраняются высокоуровневые доказательства безопасности. seL4 также является первым опубликованным ядром ОС защищенного режима с полным и надежным анализом времени выполнения в наихудшем случае (WCET), необходимым условием для его использования в системах жесткого реального времени . [19]

29 июля 2014 года NICTA и General Dynamics C4 Systems объявили, что seL4 со сквозными доказательствами теперь выпускается под лицензиями с открытым исходным кодом . [21] Исходный код ядра и доказательства находятся под GPLv2 , а большинство библиотек и инструментов находятся под лицензией BSD с двумя пунктами. В апреле 2020 года было объявлено о создании seL4 Foundation под эгидой Linux Foundation для ускорения разработки и развертывания seL4. [22]

Исследователи заявляют, что стоимость формальной проверки программного обеспечения ниже, чем стоимость разработки традиционного «высоконадежного» программного обеспечения, несмотря на то, что дает гораздо более надежные результаты. [23] В частности, стоимость одной строки кода во время разработки seL4 оценивалась примерно в 400 долларов США по сравнению с 1000 долларов США для традиционных систем высокой надежности. [24]

В рамках программы DARPA High-Assurance Cyber ​​Military Systems (HACMS) NICTA вместе с партнерами по проекту Rockwell Collins , Galois Inc, Университетом Миннесоты и Boeing разработали беспилотный летательный аппарат с высоким уровнем надежности на основе seL4 вместе с другими инструментами и программным обеспечением для обеспечения безопасности запланированный перенос технологий на опционально пилотируемый автономный вертолет Unmanned Little Bird, разрабатываемый компанией Boeing. Окончательная демонстрация технологии HACMS состоялась в Стерлинге, штат Вирджиния, в апреле 2017 года. [25] DARPA также профинансировало несколько контрактов на исследования в области инноваций малого бизнеса (SBIR), связанных с seL4 в рамках программы, начатой ​​доктором Джоном Лаунчбери.. Малые предприятия, получившие SBIR, относящиеся к seL4, включают: DornerWorks, Techshot, Wearable Inc, Real Time Innovations и Critical Technologies. [26]

Другие исследования и разработки [ править ]

Osker, ОС, написанная на Haskell , нацелена на спецификацию L4; хотя этот проект был сосредоточен на использовании функционального языка программирования для разработки ОС, а не на исследованиях микроядра как таковых. [27]

CodeZero [28] - это микроядро L4, предназначенное для встраиваемых систем с акцентом на виртуализацию и реализацию собственных сервисов ОС. Существует версия под лицензией GPL , [29] и версия, которая была повторно лицензирована B Labs Ltd., приобретена Nvidia как закрытый исходный код и разветвлена ​​в 2010 году. [30] [31]

Микроядро F9 [32], реализация L4 под лицензией BSD, предназначена для процессоров ARM Cortex-M для глубоко встроенных устройств с защитой памяти.

Архитектура виртуализации ОС NOVA [33] - это исследовательский проект с акцентом на построение безопасной и эффективной среды виртуализации [34] [35] с небольшой надежной вычислительной базой. NOVA состоит из микрогипервизора, монитора виртуальной машины на уровне пользователя и запущенной поверх него непривилегированной компонентной многосерверной пользовательской среды, называемой NUL. NOVA работает на многоядерных системах на базе ARMv8-A и x86.

WrmOS [36] - это операционная система реального времени, основанная на микроядре L4. Имеет собственные реализации ядра, стандартных библиотек и сетевого стека, поддерживающие архитектуры SPARC, ARM, x86 и x86_64. Есть паравиртуализированное ядро ​​Linux (w4linux [37] ), работающее поверх WrmOS.

См. Также [ править ]

  • PikeOS

Ссылки [ править ]

  1. ^ "Продукты гипервизора - Системы миссии General Dynamics" . gdmissionsystems.com . Архивировано 15 ноября 2017 года . Проверено 26 апреля 2018 года .
  2. ^ a b «Программное обеспечение Open Kernel Labs превзошло рубеж в 1,5 миллиарда отгрузок мобильных устройств» (пресс-релиз). Откройте Kernel Labs . 19 января 2012 года архив с оригинала на 11 февраля 2012 года.
  3. ^ a b Лидтке, Йохен (декабрь 1995 г.). «О построении µ-ядра» . Proc. 15-й симпозиум ACM по принципам операционных систем (SOSP) . С. 237–250. Архивировано 25 октября 2015 года.
  4. ^ Liedtke, Jochen (декабрь 1993). «Улучшение IPC за счет дизайна ядра» . 14-й симпозиум ACM по принципам операционных систем . Эшвилл, Северная Каролина, США. С. 175–88.
  5. ^ Gefflaut, Ален; Джегер, Трент; Пак, Юнхо; Лидтке, Йохен ; Эльфинстон, Кевин; Улиг, Фолькмар; Тидсуэлл, Джонатон; Деллер, Люк; Рейтер, Ларс (2000). «Многосерверный подход Лесопилки» . ACM SIGOPS Европейский семинар . Колдинг, Дания. С. 109–114.
  6. ^ "Архивная копия" . Архивировано 07 августа 2011 года . Проверено 10 августа 2011 .CS1 maint: archived copy as title (link)
  7. ^ Грей, Чарльз; Чепмен, Мэтью; Чабб, Питер; Мосбергер-Танг, Дэвид; Хайзер, Гернот (апрель 2005 г.). «Itanium - сказка разработчика систем» . Ежегодная техническая конференция USENIX . Аннахайм, Калифорния, США. С. 264–278. Архивировано 17 февраля 2007 года.
  8. ^ Лесли, Бен; Чабб, Питер; Фитцрой-Дейл, Николас; Гётц, Стефан; Грей, Чарльз; Макферсон, Люк; Поттс, Дэниел; Шен, Ютинг; Эльфинстон, Кевин; Хайзер, Гернот (сентябрь 2005 г.). «Драйверы устройств пользовательского уровня: достигнутая производительность». Журнал компьютерных наук и технологий . 20 (5): 654–664. CiteSeerX 10.1.1.59.6766 . DOI : 10.1007 / s11390-005-0654-4 . S2CID 1121537 .  
  9. ^ ван Шайк, Карл; Хайзер, Гернот (январь 2007 г.). «Высокопроизводительные микроядра и виртуализация на ARM и сегментированных архитектурах» . 1-й международный семинар по микроядрам для встраиваемых систем . Сидней, Австралия: НИКТА. С. 11–21. Архивировано 01 марта 2015 года . Проверено 25 октября 2015 .
  10. ^ Ruocco, Серджио (октябрь 2008). "Путешествие программиста в реальном времени по микроядрам L4 общего назначения". Журнал EURASIP по встроенным системам . 2008 : 1–14. DOI : 10.1155 / 2008/234710 . S2CID 7430332 . 
  11. ^ «Микроядро NICTA L4 для использования в некоторых решениях для набора микросхем QUALCOMM» (пресс-релиз). НИКТА. 24 ноября 2005 года Архивировано из оригинального 25 августа 2006 года.
  12. ^ «Open Kernel Labs Automotive Virtualization, выбранная Bosch для информационно-развлекательных систем» (пресс-релиз). Откройте Kernel Labs . 27 марта 2012 года в архив с оригинала на 2 июля 2012 года.
  13. ^ «Безопасность iOS, iOS 12.3» (PDF) . Apple Inc., май 2019 г.
  14. ^ Мандт, Тарьей; Сольник, Мэтью; Ван, Дэвид (31 июля 2016 г.). «Демистификация процессора Secure Enclave» (PDF) . BlackHat USA . Лас-Вегас, Невада, США. Архивировано 21 октября 2016 года (PDF) .
  15. Рианна Элмер-ДеВитт, Филип (28 октября 2014 г.). «Прогноз: в 2015 году Apple поставит 310 миллионов устройств iOS» . Удача . Архивировано 27 сентября 2015 года . Проверено 25 октября 2015 года .
  16. ^ Деррин, Филип; Эльфинстон, Кевин; Кляйн, Гервин; Петух; Дэйвид; Чакраварти, Мануэль MT (сентябрь 2006 г.). «Выполнение руководства: подход к разработке высоконадежного микроядра» . ACM SIGPLAN Haskell Workshop . Портленд, штат Орегон . С. 60–71.
  17. ^ а б Кляйн, Гервин; Эльфинстон, Кевин; Хайзер, Гернот ; Андроник, июнь; Петух, Дэвид; Деррин, Филип; Элькадуве, Дхаммика; Энгельгардт, Кай; Колански, Рафаль; Норриш, Майкл; Сьюэлл, Томас; Туч, Харви; Уинвуд, Саймон (октябрь 2009 г.). «seL4: Формальная проверка ядра ОС» (PDF) . 22-й симпозиум ACM по принципам операционных систем . Big Sky, MT, США. Архивировано (PDF) из оригинала 28 июля 2011 года.
  18. ^ Элькадуве, Дхаммика; Деррин, Филип; Эльфинстон, Кевин (апрель 2008 г.). Дизайн ядра для изоляции и обеспечения физической памяти . 1-й семинар по изоляции и интеграции во встроенных системах. Глазго, Великобритания. DOI : 10.1145 / 1435458 . Проверено 22 февраля 2020 .
  19. ^ а б Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хайзер, Гернот (февраль 2014 г.). «Комплексная формальная проверка микроядра ОС». ACM-транзакции в компьютерных системах . 32 (1): 2: 1-2: 70. CiteSeerX 10.1.1.431.9140 . DOI : 10.1145 / 2560537 . S2CID 4474342 .  
  20. ^ Сьюэлл, Томас; Майрин, Магнус; Кляйн, Гервин (июнь 2013 г.). «Проверка перевода для проверенного ядра ОС» . ACM SIGPLAN Конференция по проектированию и реализации языков программирования . Сиэтл, Вашингтон, США.
  21. ^ «Безопасная операционная система, разработанная NICTA, выходит с открытым исходным кодом» (пресс-релиз). НИКТА . 29 июля 2014 года. Архивировано 15 марта 2016 года.
  22. ^ «Безопасность получает поддержку Linux Foundation» (пресс-релиз). Linux Foundation . 7 апреля 2020 г. Архивировано 15 марта 2016 г.
  23. ^ Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хайзер, Гернот (2014). «Комплексная формальная проверка микроядра ОС» (PDF) . ACM-транзакции в компьютерных системах . 32 : 64. CiteSeerX 10.1.1.431.9140 . DOI : 10.1145 / 2560537 . S2CID 4474342 . Архивировано (PDF) из оригинала на 2014-08-03.   
  24. ^ seL4 бесплатно - что это значит для вас? на YouTube
  25. ^ «DARPA выбирает Rockwell Collins для применения технологии кибербезопасности на новых платформах» (пресс-релиз). Рокуэлл Коллинз . 24 апреля 2017 года. Архивировано 11 мая 2017 года.
  26. ^ "Спонсор агентства DARPA доктор Джон Лаанчбери" . SBIRSource . 2017. Архивировано 29 сентября 2017 года . Проверено 16 мая 2017 года .
  27. ^ Hallgren, T .; Джонс, депутат; Лесли, Р .; Толмач, А. (2005). «Принципиальный подход к построению операционных систем на Haskell» (PDF) . Труды Десятой Международной конференции ACM SIGPLAN по функциональному программированию . 40 (9): 116–128. DOI : 10.1145 / 1090189.1086380 . ISSN 0362-1340 . Архивировано (PDF) из оригинала 15.06.2010 . Проверено 24 июня 2010 .  
  28. ^ ОБЪЯВЛЕНИЕ - Знакомство с Codezero
  29. ^ "jserv / codezero: Микроядро Codezero" . Архивировано 15 августа 2015 года . Проверено 20 октября 2020 .
  30. ^ «Code Zero: встроенный гипервизор и ОС» . Архивировано из оригинального 11 - го января 2016 года . Проверено 25 января 2016 года .
  31. ^ "Архивная копия" . Архивировано из оригинала на 2 февраля 2014 года . Проверено 2 февраля 2014 года .CS1 maint: archived copy as title (link)
  32. ^ "Микроядро F9" . Проверено 20 октября 2020 .
  33. ^ "Сайт NOVA Microhypervisor" . Проверено 9 января 2021 .
  34. ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). "NOVA: Архитектура безопасной виртуализации на основе микрогипервизора". EuroSys '10: Материалы 5-й Европейской конференции по компьютерным системам . Париж, Франция .
  35. ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). «На пути к масштабируемой многопроцессорной среде пользовательского уровня». IIDS'10: Практикум по изоляции и интеграции для надежных систем . Париж, Франция .
  36. ^ "WrmOS" . Проверено 20 октября 2020 .
  37. ^ "w4linux - это паравиртуализированное ядро ​​Linux, работающее поверх WrmOS" . Проверено 20 октября 2020 .

Дальнейшее чтение [ править ]

  • Йохен Лидтке, Ульрих Бартлинг, Уве Бейер, Дитмар Генрихс, Рудольф Руланд, Дьюла Салай. Два года опыта работы с ОС на основе μ-ядра , ACM Press, 1991 г.
  • Лидтке, Йохен ; Хэберлен, Андреас; Пак, Юнхо; Рейтер, Ларс; Улиг, Фолькмар (2000-10-22). «Производительность стаб-кода становится важной» . Труды 1 - го семинара по промышленным опыта в области систем программного обеспечения (Wiess), Сан - Диего, штат Калифорния, октябрь 2000 года . Архивировано из оригинального (PDF) 05 сентября 2006 года . Проверено 5 сентября 2006 . (на ядре L4 и компиляторе)
  • Ченг Гуанхуи, Николас МакГвайр. L4 / Fiasco / L4Linux Kickstart , Distributed & Embedded Systems Lab - Университет Ланьчжоу
  • Эльфинстон, Кевин; Хайзер, Гернот (ноябрь 2013 г.). «От L3 к seL4: что мы узнали за 20 лет использования микроядер L4?» . 24-й симпозиум ACM SIGOPS по принципам операционных систем . Фармингтон, Пенсильвания, США. С. 133–150. Эволюция подходов к проектированию и реализации L4

Внешние ссылки [ править ]

  • Официальный сайт , L4Hq: штаб-квартира L4, сайт сообщества проектов L4
  • домашняя страница seL4
  • Фонд seL4
  • Семейство микроядер L4 : обзор реализаций L4, документации и проектов
  • Официальный TUD: OS Wiki
  • L4Ka : реализации L4Ka :: Pistachio и L4Ka :: Hazelnut
  • UNSW : реализации для архитектуры DEC Alpha и MIPS
  • OKL4 : коммерческая версия L4 от Open Kernel Labs
  • NICTA L4 : Обзор исследований и публикации
  • Группа надежных систем в CSIRO's Data61 : нынешний дом бывшей группы NICTA, которая разработала seL4
  • Платформа операционной системы Genode : детище сообщества L4
  • seL4 : высокозащищенная и надежная система