stringtranslate.com

Семейство микроядер L4

L4 — это семейство микроядер второго поколения , используемых для реализации различных типов операционных систем (ОС), в основном для Unix-подобных систем , совместимых с интерфейсом переносимых операционных систем ( POSIX ).

L4, как и его предшественник микроядро L3, был создан немецким ученым-компьютерщиком Йохеном Лидтке в ответ на низкую производительность более ранних ОС на основе микроядра. Лидтке считал, что система, изначально разработанная для высокой производительности, а не для других целей, может создать микроядро практического применения. Его оригинальная реализация в вручную закодированном коде языка ассемблера Intel i386 в 1993 году привлекла внимание, будучи в 20 раз быстрее, чем Mach . [1] Последующая публикация два года спустя [2] была признана настолько влиятельной, что выиграла премию ACM SIGOPS Hall of Fame Award 2015. С момента своего появления L4 разрабатывался как кроссплатформенный и для улучшения безопасности , изоляции и надежности .

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

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

Парадигма дизайна

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

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

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

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

История

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

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

Л3

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

Генеалогическое древо L4 (черные стрелки указывают на наследование кода, зеленые стрелки — на наследование ABI)

Л4

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

L4Ka::Фундук

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

L4/Фиаско

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

Кроссплатформенный

L4Ka::Фисташка

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

Новые версии Fiasco

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

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

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

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

Позже группа UNSW, теперь в NICTA (ранее National ICT Australia, Ltd .), разветвила L4Ka::Pistachio в новую версию L4 под названием NICTA::L4-embedded . Она предназначалась для использования в коммерческих встраиваемых системах , и, следовательно, компромиссы реализации были в пользу малого размера памяти и снижения сложности. API был изменен, чтобы сделать почти все системные вызовы достаточно короткими, чтобы им не требовались точки прерывания, чтобы обеспечить высокую скорость реагирования в реальном времени. [11]

Коммерческое развертывание

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

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

Процессоры серии Apple A , начиная с A7 , содержат сопроцессор Secure Enclave , работающий под управлением операционной системы L4 [14], называемой sepOS (Secure Enclave Processor OS), основанной на встроенном ядре L4, разработанном в NICTA в 2006 году. [15] В результате L4 поставляется на всех современных устройствах Apple, включая Mac с Apple Silicon . Только в 2015 году общие поставки iPhone оценивались в 310 миллионов. [16]

Высокая надежность: seL4

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

Формальное доказательство функциональной корректности было завершено в 2009 году. [18] Доказательство гарантирует, что реализация ядра соответствует его спецификации, и подразумевает, что в нем нет ошибок реализации, таких как взаимоблокировки , лайвлокировки , переполнения буфера , арифметические исключения или использование неинициализированных переменных . seL4 считается первым в истории ядром операционной системы общего назначения, которое было проверено. [18] Работа над seL4 получила премию ACM SIGOPS Hall of Fame Award 2019.

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

29 июля 2014 года NICTA и General Dynamics C4 Systems объявили, что seL4 с доказательствами end-to-end теперь выпущен под лицензиями с открытым исходным кодом . [22] Исходный код ядра и доказательства лицензированы в соответствии с лицензией GNU General Public License версии 2 (GPLv2), а большинство библиотек и инструментов находятся под 2-м пунктом BSD . В апреле 2020 года было объявлено, что под эгидой Linux Foundation был создан фонд seL4 для ускорения разработки и развертывания seL4. [23]

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

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

В октябре 2023 года компания Nio Inc. объявила, что их операционные системы SkyOS на базе seL4 будут использоваться в массовых электромобилях с 2024 года. [28]

В 2023 году seL4 выиграл премию ACM Software System Award .

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

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

RedoxOS [30] — это операционная система на основе Rust, которая также вдохновлена ​​seL4 и использует микроядро.

CodeZero [31] — микроядро L4 для встраиваемых систем с фокусом на виртуализацию и реализацию собственных служб ОС. Существует версия с лицензией GPL , [32] и версия, которая была повторно лицензирована B Labs Ltd., приобретенной Nvidia , как закрытая исходная версия и разветвлена ​​в 2010 году. [33] [34]

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

Архитектура виртуализации ОС NOVA [36] — это исследовательский проект, направленный на создание безопасной и эффективной среды виртуализации [37] [38] с небольшой доверенной вычислительной базой. NOVA состоит из микрогипервизора, гипервизора уровня пользователя ( монитора виртуальной машины ) и непривилегированной компонентной многосерверной пользовательской среды, работающей на нем под названием NUL. NOVA работает на многоядерных системах на базе ARMv8-A и x86.

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

Helios — это микроядро, созданное на основе seL4. [41] Оно является частью операционной системы Ares, поддерживает x86-64 и aarch64 и по состоянию на февраль 2023 года все еще находится в стадии активной разработки. [42]

Смотрите также

Ссылки

  1. ^ ab Liedtke, Jochen (декабрь 1993 г.). «Улучшение IPC с помощью проектирования ядра». 14-й симпозиум ACM по принципам операционных систем . Эшвилл, Северная Каролина, США. стр. 175–188.
  2. ^ abc Liedtke, Jochen (декабрь 1995 г.). "On μ-Kernel Construction". Труды 15-го симпозиума ACM по принципам операционных систем (SOSP) . стр. 237–250. Архивировано из оригинала 25 октября 2015 г.
  3. ^ "Hypervisor Products: General Dynamics Mission Systems". General Dynamics Mission Systems . Архивировано из оригинала 15 ноября 2017 года . Получено 26 апреля 2018 года .
  4. ^ ab "Open Kernel Labs Software Surpasses Milestone of 1.5 Billion Mobile Device Shipments" (пресс-релиз). Open Kernel Labs . 19 января 2012 г. Архивировано из оригинала 11 февраля 2012 г.
  5. ^ Жеффло, Ален; Джагер, Трент; Пак, Юнхо; Лидтке, Йохен ; Эльфинстон, Кевин; Улиг, Фолькмар; Тидсвелл, Джонатон; Деллер, Люк; Рейтер, Ларс (2000). «Многосерверный подход Sawmill». Европейский семинар ACM SIGOPS . Колдинг, Дания. стр. 109–114.
  6. ^ "DROPS – Overview". Дрезденский технический университет . Архивировано из оригинала 7 августа 2011 года . Получено 10 августа 2011 года .
  7. ^ l4ka.org: Микроядро L4Ka::Pistachio Цитата: «...Разнообразие поддерживаемых архитектур делает L4Ka::Pistachio идеальной платформой для исследований и разработок для самых разных систем...»
  8. ↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (апрель 2005 г.). «Itanium: A system implementor's tale». Ежегодная техническая конференция USENIX . Аннахайм, Калифорния, США. С. 264–278. Архивировано из оригинала 17 февраля 2007 г.
  9. ^ Лесли, Бен; Чабб, Питер; Фицрой-Дейл, Николас; Гётц, Стефан; Грей, Чарльз; Макферсон, Люк; Поттс, Дэниел; Шен, Юетинг; Элфинстоун, Кевин; Хейзер, Гернот (сентябрь 2005 г.). «Драйверы устройств пользовательского уровня: достигнутая производительность». Журнал компьютерной науки и технологий . 20 (5): 654–664. CiteSeerX 10.1.1.59.6766 . doi :10.1007/s11390-005-0654-4. S2CID  1121537. 
  10. ^ van Schaik, Carl; Heiser, Gernot (январь 2007 г.). «Высокопроизводительные микроядра и виртуализация на ARM и сегментированных архитектурах». 1-й международный семинар по микроядрам для встраиваемых систем . Сидней, Австралия: NICTA . стр. 11–21. Архивировано из оригинала 1 марта 2015 г. Получено 25 октября 2015 г.
  11. ^ Руокко, Серджио (октябрь 2008 г.). «Обзор универсальных микроядер L4 для программистов реального времени». Журнал EURASIP по встраиваемым системам . 2008 : 1–14. doi : 10.1155/2008/234710 (неактивен 1 ноября 2024 г.). S2CID  7430332.{{cite journal}}: CS1 maint: DOI неактивен по состоянию на ноябрь 2024 г. ( ссылка )
  12. ^ "NICTA L4 Microkernel to be Utilised in Select QUALCOMM Chipset Solutions" (пресс-релиз). NICTA . 24 ноября 2005 г. Архивировано из оригинала 25 августа 2006 г.
  13. ^ "Автомобильная виртуализация Open Kernel Labs выбрана Bosch для информационно-развлекательных систем" (пресс-релиз). Open Kernel Labs . 27 марта 2012 г. Архивировано из оригинала 2 июля 2012 г.
  14. ^ "iOS Security, iOS 12.3" (PDF) . Apple Inc. Май 2019. Архивировано (PDF) из оригинала 24 июня 2020.
  15. ^ Мандт, Тарьей; Сольник, Мэтью; Ван, Дэвид (31 июля 2016 г.). «Демистификация процессора Secure Enclave» (PDF) . Блэкхэт США . Лас-Вегас, Невада, США. Архивировано (PDF) из оригинала 21 октября 2016 г.
  16. ^ Элмер-ДеВитт, Филип (28 октября 2014 г.). «Прогноз: Apple поставит 310 миллионов устройств iOS в 2015 году». Fortune . Архивировано из оригинала 27 сентября 2015 г. Получено 25 октября 2015 г.
  17. ^ Деррин, Филипп; Элфинстоун, Кевин; Кляйн, Гервин; Кок, Дэвид; Чакраварти, Мануэль MT (сентябрь 2006 г.). «Запуск руководства: подход к высоконадежной разработке микроядра». Семинар ACM SIGPLAN Haskell . Портленд, Орегон . С. 60–71.
  18. ^ ab Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot ; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (октябрь 2009 г.). "seL4: Формальная проверка ядра ОС" (PDF) . 22-й симпозиум ACM по принципам операционных систем . Биг-Скай, Монтана, США. Архивировано (PDF) из оригинала 28 июля 2011 г.
  19. ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (апрель 2008 г.). Проектирование ядра для изоляции и обеспечения физической памяти. 1-й семинар по изоляции и интеграции во встраиваемых системах. Глазго, Великобритания. doi :10.1145/1435458. Архивировано из оригинала 22 февраля 2020 г. . Получено 22 февраля 2020 г. .
  20. ^ ab Klein, Gerwin; Andronick, June; Elphinstone, Kevin; Murray, Toby; Sewell, Thomas; Kolanski, Rafal; Heiser, Gernot (февраль 2014 г.). «Комплексная формальная проверка микроядра ОС». ACM Transactions on Computer Systems . 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140 . doi :10.1145/2560537. S2CID  4474342. 
  21. ^ Сьюэлл, Томас; Майрин, Магнус; Кляйн, Гервин (июнь 2013 г.). «Проверка перевода для проверенного ядра ОС». Конференция ACM SIGPLAN по проектированию и реализации языков программирования . Сиэтл, Вашингтон, США. doi :10.1145/2491956.2462183.
  22. ^ "Безопасная операционная система, разработанная NICTA, становится общедоступной" (пресс-релиз). NICTA . 29 июля 2014 г. Архивировано из оригинала 15 марта 2016 г.
  23. ^ "Security Gets Support of Linux Foundation" (пресс-релиз). Linux Foundation . 7 апреля 2020 г. Архивировано из оригинала 15 марта 2016 г.
  24. ^ Кляйн, Гервин; Андроник, Джун; Элфинстоун, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафал; Хейзер, Гернот (2014). «Комплексная формальная проверка микроядра ОС» (PDF) . ACM Transactions on Computer Systems . 32 : 64. CiteSeerX 10.1.1.431.9140 . doi :10.1145/2560537. S2CID  4474342. Архивировано (PDF) из оригинала 3 августа 2014 г. 
  25. ↑ Хейзер, Гернот (16 января 2015 г.). seL4 бесплатен: что это значит для вас?. Окленд, Новая Зеландия: Linux.conf.au.
  26. ^ "DARPA выбирает Rockwell Collins для применения технологии кибербезопасности на новых платформах" (пресс-релиз). Rockwell Collins . 24 апреля 2017 г. Архивировано из оригинала 11 мая 2017 г.
  27. ^ "DARPA Agency Sponsor Dr. John Launchbury". SBIRSource . 2017. Архивировано из оригинала 29 сентября 2017. Получено 16 мая 2017 .
  28. ^ "Новости о seL4 и seL4 Foundation". sel4.systems . Получено 20 сентября 2024 г. .
  29. ^ Hallgren, T.; Jones, MP; Leslie, R.; Tolmach, A. (2005). "Принципиальный подход к построению операционной системы на языке Haskell" (PDF) . ACM SIGPLAN Notices . 40 (9): 116–128. doi :10.1145/1090189.1086380. ISSN  0362-1340. Архивировано (PDF) из оригинала 15 июня 2010 г. . Получено 24 июня 2010 г. .
  30. ^ "RedoxOS". RedoxOS .
  31. ^ "Анонс: Представляем Codezero". Дрезденский технический университет .
  32. ^ "jserv/codezero: Codezero Microkernel". GitHub . Архивировано из оригинала 15 августа 2015 г. Получено 20 октября 2020 г.
  33. ^ "Code Zero: Embedded Hypervisor and OS". Архивировано из оригинала 11 января 2016 года . Получено 25 января 2016 года .
  34. ^ "B Labs | Решения для мобильной виртуализации, виртуализация Android и Linux для архитектуры ARM". Архивировано из оригинала 2 февраля 2014 г. Получено 2 февраля 2014 г.
  35. ^ "F9 Microkernel". GitHub . Получено 20 октября 2020 г.
  36. ^ "Сайт NOVA Microhypervisor" . Получено 9 января 2021 г. .
  37. ^ Steinberg, Udo; Kauer, Bernhard (апрель 2010 г.). "NOVA: архитектура безопасной виртуализации на основе микрогипервизора". EuroSys '10: Труды 5-й Европейской конференции по компьютерным системам . Париж, Франция .
  38. ^ Steinberg, Udo; Kauer, Bernhard (апрель 2010 г.). «На пути к масштабируемой многопроцессорной среде пользовательского уровня». IIDS'10: Семинар по изоляции и интеграции для надежных систем . Париж, Франция .
  39. ^ "WrmOS" . Получено 20 октября 2020 г.
  40. ^ "w4linux — это паравиртуализированное ядро ​​Linux, работающее на WrmOS" . Получено 20 октября 2020 г.
  41. ^ "~sircmpwn/helios – Экспериментальное микроядро – sourcehut git". git.sr.ht . Получено 20 февраля 2023 г. .
  42. ^ "Helios". ares-os.org . Получено 20 февраля 2023 г. .

Дальнейшее чтение

Внешние ссылки