Русская Википедия:L4 (микроядро)

Материал из Онлайн справочника
Перейти к навигацииПерейти к поиску

Шаблон:Значения Шаблон:Закончить перевод Шаблон:Infobox software

L4 — микроядро второго поколения, разработанное Йохеном Лидтке в 1993 году[1].

Архитектура микроядра L4 оказалась успешной. Было создано множество реализаций ABI и API микроядра L4. Все реализации стали называть семейством микроядер L4. Реализация Лидтке неофициально была названа «L4/x86»[2].

История

L1

В 1977 году Йохен Лидтке защитил дипломный проект по математике в университете города Билефельд (Германия). В рамках проекта Лидтке написал компилятор для языка ELAN (англ.). Язык ELAN создан в 1974 году на основе языка Алгол 68 для обучения программированию[3]. Лидтке назвал свою работу «L1»: буква «L» — первая буква фамилии автора (Liedtke); цифра «1» — порядковый номер работы.

L2

Шаблон:Основная статья

В 1977 году Лидтке получил диплом математика, остался в университете города Билефельд и приступил к созданию среды выполнения для языка ELAN.

8‑битные микроконтроллеры стали широко доступными. Требовалась операционная система, способная работать на небольших рабочих станциях в средних школах и вузах. CP/M не подходила. Национальный исследовательский центр компьютерных наук и технологий Германии GMD и университет города Билефельд решил разработать новую операционную систему с нуля[4].

В 1979 году Йохен Лидтке начал разработку новой операционной системы и назвал её «Eumel» (англ.) от Шаблон:Lang-en. Операционная система «Eumel» также называлась «L2», что означает «2‑я работа Liedtke». Новая ОС поддерживала 8-битовые процессоры Zilog Z80, была многопользовательской и многозадачной, была построена на основе микроядра, поддерживала en (Persistence (computer science)). Поддержка orthogonal persistence заключалась в следующем: ОС периодически сохраняла на диск своё состояние (содержимое памяти, регистров процессора и др.); после перебоев в подаче электроэнергии ОС восстанавливалась из сохранённого состояния; программы продолжали работать так, будто бы сбоя не происходило; терялись только изменения, внесённые с момента последнего сохранения. ОС Eumel проектировалась под влиянием ОС Multics и содержала много общего с ядрами en (Accent (programming language)) и Mach[4].

Позднее ОС Eumel была портирована на процессоры Zilog Z8000, Motorola 68000 и Intel 8086. Эти процессоры были 8‑ и 16‑битовыми, не содержали MMU и не поддерживали механизма защиты памяти. ОС Eumel эмулировала виртуальную машину, имеющую 32‑битовую адресацию и MMU[4]. Несмотря на использование эмуляции, к одной рабочей станции с ОС Eumel можно было подключить до пяти терминалов[4].

Поначалу писать программы для ОС Eumel можно было только на языке ELAN. Позднее были добавлены компиляторы для языков [[|en]] (Compiler Description Language), Pascal, Basic и en (DYNAMO (programming language)), но массово они не применялись[4].

С 1980 года началось применение ОС Eumel сначала для обучения программированию и обработки текста, а затем — и в коммерческих целях. Так, в середине 1980‑х годов ОС Eumel работала уже на более чем 2000 компьютеров в юридических и других фирмах[4].

L3

Шаблон:Основная статья

С появлением процессоров, поддерживающих виртуальную память (за счёт MMU) и механизмы для её защиты, пропала необходимость эмуляции виртуальной машины.

В 1984 году[5] Йохен Лидтке перешёл на работу в исследовательский центр GMD для создания ОС, аналогичной ОС Eumel, но работающей без эмуляции. В настоящее время GMD входит в состав организации «Общество Фраунгофера».

С 1987 года[4] Йохен Лидтке и его команда из института SET, входящем в состав GMD, приступили к разработке нового микроядра, получившего название «L3» («L3» от «3‑я работа Liedtke»).

Йохен Лидтке хотел проверить, возможно ли добиться высокой производительности компонента IPC, если выбрать для ядра подходящую архитектуру и в реализации использовать особенности архитектуры. Реализация механизма IPC оказалась удачной (по сравнению со сложной реализацией IPC в микроядре Mach). Позднее был реализован механизм изоляции областей памяти процессов, работающих в пространстве пользователя.

В 1988 году разработка была завершена и была выпущена одноимённая операционная система. Микроядро L3 было написано на языке ассемблера, задействовало особенности процессоров архитектуры Intel x86, не поддерживало другие платформы, по производительности обогнало микроядро Mach. ОС L3 была совместима с ОС Eumel: программы, созданные для ОС Eumel, работали под управлением ОС L3, но не наоборот[4].

Компоненты микроядра L3:

  • компонент IPC (реализовывал механизм для синхронного обмена сообщениями);
  • компонент, обеспечивающий работу со страницами памяти и работающий в пространстве пользователя[6];
  • компонент, реализующий механизм обеспечения безопасности, называемый Шаблон:Lang-en («tasks», «clans» и «chiefs»).

С 1989 года[4] ОС стала применяться:

  • в школах (заменила свою предшественницу — ОС Eumel)[4];
  • на примерно 3000 компьютерах, установленных в юридических фирмах Германии[5].

L4

Во время работы над микроядром L3 Йохен Лидтке обнаружил недостатки микроядра Mach. Желая повысить производительность, Лидтке стал составлять код нового микроядра на языке ассемблера с использованием особенностей архитектуры процессоров Intel i386. Новое микроядро получило название «L4» (от «4‑я работа Liedtke»).

В 1993 году реализация микроядра L4 была закончена. Компонент IPC оказался в 20 раз быстрее IPC из микроядра Mach[1].

ОС, построенные на микроядрах первого поколения (в частности, на микроядре Mach), отличались низкой производительностью. Из-за этого в середине 1990-х годов разработчики стали пересматривать концепцию микроядерной архитектуры. В частности, плохую производительность микроядра Mach объясняли переносом компонента, ответственного за IPC, в пространство пользователя.

Исследователи искали причины низкой производительности микроядра Mach и тщательно анализировали компоненты, важные для обеспечения хорошей производительности. Анализ показал, что ядро выделяло процессам слишком большой working set (много памяти), в результате чего при обращении ядра к памяти постоянно происходили кэш‑промахи (Шаблон:Lang-en)[6]. Анализ позволил сформулировать новое правило для разработчиков микроядер — микроядро должно проектироваться так, чтобы компоненты, важные для обеспечения высокой производительности, помещались в кэш процессора (желательно, первого уровня (Шаблон:Lang-en, L1) и желательно, чтобы в кеше ещё осталось немного места).

Из-за резкого скачка в производительности компонента IPC существующие ОС оказались неспособны обработать возросший поток сообщений IPC. Несколько университетов (например, технический университет Дрездена, университет Нового Южного Уэльса), институтов и организаций (например, IBM) начали создавать реализации L4 и строить на их основе новые ОС.

В 1996 году Лидтке защитил диссертацию на степень PhD[7] в техническом университете Берлина по теме «защищённые таблицы страниц»[8].

С 1996 года в en (Thomas J. Watson Research Center) Лидтке с коллегами продолжил исследования микроядра L4, микроядер вообще и операционной системы «Sawmill OS» в частности[9]. Из-за отсутствия коммерческого успеха у ОС «Шаблон:Не переведено 5», построенной на третьей версии микроядра Mach от CMU и разрабатываемой фирмой IBM с января 1991 года по 1996 год[10], вместо понятия «микроядро L4» использовалось понятие «Lava Nucleus» или, кратко, «LN».

Со временем код микроядра L4 был избавлен от привязки к платформе, были улучшены механизмы обеспечения безопасности и изоляции.

В 1999 году Лидтке стал работать профессором по операционным системам в технологическом институте Карлсруэ (Германия)[7].

Микроядро L4Ka::Hazelnut

В 1999 году Йохен Лидтке был принят в состав группы «Systems Architecture Group» (Шаблон:AnchorSAG), работающей в технологическом институте Карлсруэ (Германия), и продолжил исследования микроядерных ОС. Группа SAG также известна как группа «L4Ka».

Желая доказать возможность реализации микроядра на высокоуровневом языке, группа SAG разработала микроядро «L4Ka::Hazelnut». Работа велась в технологическом институте Карлсруэ при поддержке DFG[11]. Реализация была написана на языке C++ и поддерживала процессоры архитектур IA-32 и ARM. Производительность нового микроядра оказалась приемлемой, и разработка ядер на языке ассемблера была прекращена.

Микроядро L4/Fiasco

В 1998 году группа Operating Systems Group, входящая в состав технического университета Дрездена, начала разработку собственной реализации микроядра L4, получившую название «L4/Fiasco». Разработка велась на языке C++ параллельно с разработкой микроядра «L4Ka::Hazelnut».

В то время микроядро L4Ka::Hazelnut не поддерживало concurrency в пространстве ядра, а микроядро «L4Ka::Pistachio» поддерживало прерывания в пространстве ядра только в особых точках preemption. Разработчики микроядра «L4/Fiasco» реализовали полную вытесняющую многозадачность (за исключением некоторых атомарных операций). Это усложнило архитектуру ядра, но снизило задержки при прерываниях, что важно для операционной системы реального времени.

Микроядро «L4/Fiasco» использовалось в ОС «DROPS»[12] — ОС «жёсткого» реального времени (когда крайне важно, чтобы на событие реагировали в строго установленные сроки), также разработанной в техническом университете Дрездена.

Ввиду усложнения архитектуры микроядра в поздних версиях ОС «Fiasco» разработчики вернулись к традиционному подходу — запуску ядра с выключенными прерываниями (за исключением нескольких точек preemption).

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

Микроядро L4Ka::Pistachio

Реализации микроядра L4, созданные до выпуска микроядра L4Ka::Pistachio и поздних версий микроядра «Fiasco», использовали особенности архитектуры компьютера (были «привязаны» к архитектуре процессора). Был разработан API, не зависимый от архитектуры. Несмотря на добавление переносимости, API обеспечивал высокую производительность. Идеи, лежащие в основе микроядерной архитектуры, не изменились.

В начале 2001 года новое L4 API было опубликовано, сильно отличалось от L4 API предыдущей версии, получило номер версии 4 («version 4», также известно как «version X.2») и отличалось:

После выпуска новой версии API группа SAG приступила к созданию нового микроядра, получившего название «L4Ka::Pistachio»[13][14]. Код составлялся с нуля на языке C++, использовался опыт проекта L4Ka::Hazelnut. Внимание уделялось высокой производительности и переносимости.

10 июня 2001 года доктор Йохен Лидтке погиб[7] в автокатастрофе. После этого скорость развития проекта заметно снизилась.

В 2003 году[15] работа была завершена благодаря усилиям студентов Лидтке: Volkmar Uhlig, Uwe Dannowski и Espen Skoglund. Исходный код был выпущен под лицензией 2‑clause BSD.

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

Параллельно продолжалось развитие микроядра L4/Fiasco. Была добавлена поддержка нескольких аппаратных платформ (x86, AMD64, ARM). Примечательно, что версия Fiasco, названная «FiascoUX», могла работать в пространстве пользователя под управлением ОС Linux.

Разработчики микроядра L4/Fiasco реализовали несколько расширений к L4v2 API.

  • Исключение IPC позволило ядру передавать обработку исключений процессора в пространство пользователя.
  • Добавление Шаблон:Iw (потока, выполняемого одним ядром процессора от имени процесса, запущенного на другом ядре процессора) позволило реализовать детальное управление системными вызовами.
  • Добавление UTCB (таких же, как в L4 API версии X.2).

Кроме того, микроядро «Fiasco» предоставляло механизмы управления правами коммуникации. Такие же механизмы существовали для управления потребляемыми ядром ресурсами.

Был разработан «L4Env» — набор компонентов, работающих поверх микроядра «Fiasco» в пространстве пользователя. «L4Env» использовался в «L4Linux» — реализации паравиртуализации (виртуализации ABI) для ядер Linux версий 2.6.x.

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

Шаблон:AnchorРазработчики из университета Нового Южного Уэльса создали микроядра L4/MIPS и L4/Alpha — реализации L4 для 64‑битовых процессоров серий MIPS и DEC Alpha. Оригинальное микроядро L4 поддерживало только процессоры архитектуры x86 и неофициально стало называться «L4/x86». Реализации были написаны с нуля на языке C и языке ассемблера, не были переносимы. После выпуска независимого от платформы микроядра L4Ka::Pistachio группа UNSW прекратила разработку своих микроядер, занялась портированием микроядра L4Ka::Pistachio. Реализация механизма передачи сообщений оказалась быстрее других реализаций (36 тактов на процессорах архитектуры Itanium)[16].

Группа UNSW показала, что драйвер, работающий в пространстве пользователя, может исполняться так же, как и драйвер, работающий в пространстве ядра[17].

Она разработала компоненты для паравиртуализации ядер Linux. Компоненты работали поверх микроядра L4. Результат был назван «Шаблон:Не переведено 5». Wombat OS могла работать на процессорах архитектур x86, ARM и MIPS. На процессорах Intel XScale ОС Wombat OS выполняла переключение контекста в 30 раз медленнее, чем монолитное ядро Linux[18].

Затем группа UNSW перешла в фирму NICTA, создала ответвление микроядра L4Ka::Pistachio и назвала его «NICTA::L4-embedded». Новое микроядро писалось для коммерческих встраиваемых систем, требовало мало памяти и реализовывало упрощённый API L4. С упрощённым API системные вызовы были сделаны настолько «короткими», что не требовали точек вытесняющей многозадачности и позволяли реализовать ОС реального времени[19].

Коммерческое применение

Фирма Qualcomm запускала реализацию микроядра L4, разработанную фирмой «Шаблон:Не переведено 5», на наборе микросхем, называемом «Mobile Station Modem» (MSM). Об этом в ноябре 2005 года сообщили[20] представители фирмы «NICTA», а в конце 2006 года наборы микросхем MSM поступили в продажу. Так реализация микроядра L4 оказалась в сотовых телефонах.

В августе 2006 года en (Gernot Heiser) основал фирму Open Kernel Labs. Тогда Хейсер занимал должность руководителя программы ERTOS, организованной фирмой NICTA[21], и был профессором в университете UNSW. Фирма «OK Labs» создавалась для

  • оказания технической поддержки коммерческим пользователям L4;
  • продолжения разработки L4 совместно с фирмой «NICTA» для продолжения коммерческого использования реализации L4, но уже под брендом «OKL4».

В апреле 2008 года была выпущена версия 2.1 микроядра «OKL4» — первая общедоступная реализация L4, имеющая capability-based security. В октябре 2008 года вышла версия 3.0[22] — последняя версия «OKL4» с открытым исходным кодом. Исходный код следующих версий был закрыт. Прослойка микроядра, обеспечивающая работу гипервизора, была переписана с целью добавления поддержки native гипервизора, называемого «OKL4 microvisor»[23].

Фирма «OK Labs» распространяла паравиртуализированную (Шаблон:Lang-en) ОС Linux, называемую «OK:Linux»[24]. «OK:Linux» была потомком ОС «Wombat OS»Шаблон:Ref-en. Также фирма «OK Labs» распространяла паравиртуализированные версии операционных систем Symbian и Android.

Фирма «OK Labs» приобрела у фирмы «NICTA» права на микроядро «seL4».

В начале 2012 года было продано более 1,5 миллиарда устройств, оснащённых реализацией микроядра L4[25]. Большинство из этих устройств содержало микросхемы, реализующие беспроводные модемы и было выпущено фирмой «Qualcomm».

Реализация L4 также использовалась в автомобильных развлекательных системах[26].

ОС, построенная на основе реализации L4, исполнялась процессором secure enclave, входящим в состав размещённой на кристалле электронной схемы Apple A7[27]. Эта же реализация L4 использовалась в проекте «Darbat» фирмы NICTA[28]. Устройства, содержащие Apple A7, поставлялись с ОС iOS. По состоянию на 2015 год количество устройств с ОС iOS составляло примерно 310 миллионов[29].

Верификация

seL4

В 2006 году началась разработка микроядра третьего поколения, получившего название «seL4»[30]. Разработка началась с нуля группой программистов из фирмы «NICTA». Цель: создание основы для построения безопасных и надёжных систем, способных удовлетворить современным требованиям безопасности, записанным, например, в документе «Общие критерии оценки защищённости информационных технологий». С самого начала код микроядра писался так, чтобы была возможность его верификации (проверки корректности). Верификация выполнялась с помощью языка Haskell: на языке Haskell записывались требования к микроядру (спецификация); объекты микроядра представлялись в виде объектов Haskell; работа с оборудованием эмулировалась[31]. Чтобы иметь возможность получения информации о доступности объекта путём выполнения формального рассуждения, в seL4 использовался контроль доступа, основанный на capability-based security.

В 2009 году было завершено доказательство корректности кода микроядра seL4[32]. Существование доказательства гарантировало соответствие реализации и спецификации, подтверждало отсутствие в реализации некоторых ошибок (например, отсутствие взаимных блокировок, livelocks, переполнений буферов, арифметических исключений и случаев использования неинициализированных переменных). Микроядро seL4 было первым микроядром, предназначенным для ОС общего назначения и прошедшим верификацию[32].

В микроядре seL4 было реализовано нестандартное управление ресурсами ядра[33]:

  • управлением ресурсами ядра занимался компонент, работающий в пространстве пользователя;
  • механизм capability-based security использовался не только для контроля доступа к ресурсам пространства пользователя, но и для контроля доступа к ресурсам ядра.

Нечто похожее было реализовано в экспериментальной ОС Barrelfish. Благодаря такому подходу к управлению ресурсами ядра появилась возможность выполнения рассуждения о изолированности свойств, а в дальнейшем было выполнено доказательство того, что микроядро seL4 обеспечивает целостность и конфиденциальность свойств[34]. Доказательство было выполнено для исходного кода.

Команда исследователей из фирмы NICTA доказала корректность трансляции текста с языка C на машинный код. Это позволило исключить компилятор из списка доверенного ПО и считать доказательство, выполненное для исходного кода микроядра, справедливым и для исполняемого файла микроядра.

Микроядро seL4 стало первым ядром, поддерживающим защищённый режим, для которого анализ worst-case execution-time был выполнен полностью, а результаты этого анализа были опубликованы. Результаты анализа необходимы для использования микроядра в ОС жёсткого реального времени[34].

29 июля 2014 года фирмы NICTA и Шаблон:Нп3 объявили о выпуске микроядра seL4 (включая все доказательства их корректности) под открытыми лицензиями[35]. Исходный код микроядра и доказательства поставлялись под лицензией GPL v2. Большинство библиотек и инструментов поставлялись под лицензией 2-clause BSD.

Интересно заявление исследователей[36] о том, что стоимость выполнения верификации ПО ниже стоимости традиционного исследования ПО несмотря на то, что при верификации можно получить намного больше заслуживающей доверие информации.

В августе 2012 года фирмы NICTA, Шаблон:Нп3, Galois Inc, Boeing и университет Миннесоты в рамках программы по разработке высоконадежных военных кибер-систем[37], организованной агентством DARPA, приступили к разработке беспилотного летательного аппарата[38]. Основное требование к разработке — обеспечение высокой надёжности аппарата. У каждой из перечисленных фирм была своя роль в программе. Фирма NICTA была ответственна за разработку ОС и построила её на основе микроядра seL4. Ответственные задачи были реализованы в виде компонентов микроядра, а не ответственные — запускались под паравиртуализированной ОС Linux. Наработки программы планировалось использовать в вертолёте «NICTA Unmanned Little Bird», разработкой которого занималась фирма Boeing. Вертолёт должен был поддерживать как управление пилотом, так и беспилотный режим. В ноябре 2015 года было сообщено об успешной реализации[39].

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

Hurd/L4. В ноябре 2000 года для обсуждения идеи портирования ядра «GNU Hurd» на микроядро L4 был создан список рассылки «l4-hurd». Портирование осуществлялось в течение 2002‑2004 годов, результат получил название «Hurd/L4». Реализация «Hurd/L4» не была окончена. В 2005 году проект был остановлен[40].

Osker — операционная система, реализующая L4 и написанная на языке Haskell в 2005 году. Цель проекта: проверка возможности реализации ОС на функциональном языке (а не исследовании микроядра)[41].

Codezero — реализация микроядра L4 для встраиваемых систем, ставшая общедоступной летом 2009 года[42]. Создана разработчиками британской фирмы «B Labs» с нуля. Код составлялся на языке C. Реализация поддерживает процессоры архитектуры ARM, реализует гипервизор первого порядка, поддерживает виртуализацию ОС Linux и Android[43][44]. Несмотря на заявление о поставке кода под лицензией GPL v3, скачать код с официального сайта нельзя.

F9 — реализация микроядра L4, ставшая общедоступной в июле 2013 года[45]. Написана с нуля на языке C. Предназначена для встраиваемых систем. Поддерживает серии процессоров Cortex-M архитектуры ARM. Код поставляется под лицензией BSD.

Fiasco.OC — микроядро третьего поколения, созданное на основе микроядра «L4/Fiasco». Реализует механизм Шаблон:Нп3, поддерживает многоядерные процессоры и аппаратную виртуализацию[46].

L4 Runtime Environment (кратко, L4Re) — каркас, работающий поверх микроядра «Fiasco.OC» и предназначенный для создания компонентов в пространстве пользователя. L4Re предоставляет функционал для создания клиент-серверных приложений, реализации файловых систем, реализует популярные библиотеки, например, стандартную библиотеку языка C («libc»), стандартную библиотеку языка C++ («libstdc++») и библиотеку pthreads.

Каркас L4Re и микроядро «Fiasco.OC» поддерживали процессоры архитектур x86 (IA-32 и AMD64), ARM и PowerPC (WiP).

L4Linux — подсистема для запуска ОС Linux поверх микроядра «Fiasco.OC» с помощью паравиртуализации[47]. Ранее вместо пары «Fiasco.OC» — L4Re использовалась пара «L4/Fiasco» — L4Env.

NOVA (Шаблон:Lang-en) — исследовательский проект, созданный с целью создания безопасного и эффективного окружения для виртуализации[48][49][50] с небольшим списком доверенного ПО (Шаблон:Lang-en). В состав NOVA входят:

  • микроядро, реализующее L4 и гипервизор первого порядка (Шаблон:Lang-en);
  • VMM Vancouver — компонент микроядра (процесс), работающий в пространстве пользователя, занимающийся обслуживанием (эмуляцией оборудования) одной виртуальной машины и лишённый привилегий. На каждую виртуальную машину запускалось по одному VMM. VMM Vancouver входит в состав NUL и может быть заменён на VMM Seoul. VMM Seoul[51] создан на основе VMM Vancouver;
  • NUL (Шаблон:Lang-en) — некоторые компоненты микроядра, работающие в пространстве пользователя (VMM Vancouver, драйверы устройств (например, сетевой карты); partition manager; компоненты, предназначенные для управления памятью, вводом-выводом; компоненты, реализующие стеки TCP/IP, USB и др.). NUL может быть заменён на genode или NRE. NRE (Шаблон:Lang-en) — потомок NUL.

Проект NOVA поддерживал многоядерные процессоры архитектуры x86. Для запуска под управлением микрогипервизора (гипервизора, построенного на микроядре) NOVA гостевая ОС должна поддерживать Intel VT-x или AMD-V. Исходный код поставлялся под лицензией GPL v2.

Xameleon — ОС на микроядре L4[52]. Проект основал в 2001 году единственный разработчик Алексей Мандрыкин (род. 19 января 1973 года). Изначально ОС была построена поверх микроядра «L4/Fiasco». Позднее автор перевёл ОС на микроядро «L4Ka::Pistachio». Исходный код ОС закрыт.

WrmOS — операционная система реального времени (РТОС) с открытым исходным кодом, основанная на микроядре L4. WrmOS имеет собственную реализацию ядра, стандартных библиотек и сетевого стэка. Поддержаны следующие процессорные архитектуры — SPARC, ARM, x86, x86_64. Ядро WrmOS базируется на документе L4 Kernel Reference Manual Version X.2. Существует паравиртуализированное ядро Linux (w4linux) работающее поверх WrmOS.

Примечания

Шаблон:Примечания

Литература

Ссылки

  1. 1,0 1,1 Шаблон:Cite conference Шаблон:Cite web
  2. Семейство микроядер L4. Обзор Шаблон:WaybackШаблон:Ref-en // Сайт технического университета Дрездена (Германия).
  3. Язык ELAN Шаблон:WaybackШаблон:Ref-en // Сайт технического университета Дрездена.
  4. 4,0 4,1 4,2 4,3 4,4 4,5 4,6 4,7 4,8 4,9 Шаблон:Cite conference Шаблон:Cite web
  5. 5,0 5,1 In Memoriam Jochen Liedtke (1953—2001) Шаблон:Wayback.
  6. 6,0 6,1 Шаблон:Cite conference Шаблон:Cite web
  7. 7,0 7,1 7,2 System architecture group. About us. People. Liedtke. Архивная копия.
  8. Jochen Liedtke. Page table structures for fine-grain virtual memory Шаблон:Wayback. Technical report 872. German national research center for computer science (GMD). Октябрь 1994 года.
  9. Шаблон:Cite conference
  10. Шаблон:Статья
  11. Страница группы «L4Ka» // archive.org.
  12. Drops overview Шаблон:Wayback.
  13. Микроядро «L4Ka::Pistachio» Шаблон:WaybackШаблон:Ref-en.
  14. Команда разработчиков «L4Ka» Шаблон:WaybackШаблон:Ref-en.
  15. The L4Ka::Pistachio Microkernel.Шаблон:Ref-en Белая книга. PDF. 1 мая 2003 года // archive.org.
  16. Шаблон:Cite conference Шаблон:Cite web
  17. Шаблон:Статья
  18. Шаблон:Cite conference Шаблон:Cite web
  19. Шаблон:СтатьяШаблон:Недоступная ссылка
  20. [1] Шаблон:Wayback.
  21. Страница программы ERTOS на сайте NICTA // archive.org.
  22. Шаблон:Cite web
  23. OKL4 microvisor Шаблон:Wayback.
  24. Шаблон:Cite web
  25. Шаблон:Cite press release
  26. Шаблон:Cite press release
  27. Шаблон:Cite web
  28. Darbat project Шаблон:Wayback.
  29. [2] Шаблон:Wayback.
  30. [3] Шаблон:Wayback.
  31. Шаблон:Cite conference Шаблон:Cite web
  32. 32,0 32,1 Шаблон:Cite conference Шаблон:Cite web
  33. Шаблон:Cite conference Шаблон:Cite web
  34. 34,0 34,1 Шаблон:Статья
  35. Шаблон:Cite press release
  36. Шаблон:Статья
  37. High-assurance cyber military systems Шаблон:Webarchive (HACMS).
  38. Проект SMACCM Шаблон:Wayback // Сайт фирмы Шаблон:Нп3. SMACCM — аббревиатура от Шаблон:Lang-en.
  39. Дронов нового поколения взломать невозможно Шаблон:Wayback // Журнал «Популярная механика». 12 ноября 2015 года.
  40. История GNU Hurd. Портирование на другое микроядро Шаблон:WaybackШаблон:Ref-en.
  41. Шаблон:Статья
  42. Codezero Шаблон:Wayback на сайте genode.org.
  43. dev.b-labs.com // archive.org.
  44. Официальный сайт проекта Codezero Шаблон:Wayback.
  45. Репозиторий проекта F9 Шаблон:Wayback // github.com.
  46. Шаблон:Cite conference
  47. L4Linux Шаблон:Wayback.
  48. Шаблон:Cite conference
  49. Шаблон:Cite conference
  50. Проект Nova Шаблон:Wayback. Официальный сайт.
  51. VMM Seoul Шаблон:Wayback // github.com
  52. l4os.ru Шаблон:Wayback. Официальный сайт проекта Xameleon.