Семейство микроядер L4
| Разработчик | Йохен Лидтке |
|---|---|
| Написано в | Язык ассемблера , затем C , C++ |
| Семейство ОС | Л4 |
| Рабочее состояние | Текущий |
| Исходная модель | Открытый исходный код , закрытый исходный код |
| Начальная версия | 1993 год |
| Маркетинговая цель | Надежные вычисления |
| Доступно в | английский, немецкий |
| Платформы | Intel i386 , x86 , x86-64 , ARM , MIPS , SPARC , Itanium , RISC-V |
| ядра Тип | Микроядро |
| Лицензия | Исходный код , доказательства : GPLv2. Библиотеки , инструменты : 2-пункт BSD |
| Предшествует | Юмель |
| Официальный веб-сайт | ты |
L4 — это семейство микроядер второго поколения , используемых для реализации различных типов операционных систем (ОС), хотя в основном для Unix-подобных , совместимых с интерфейсом переносимой операционной системы ( POSIX типов ).
L4, как и его предшественник, микроядро L3 , был создан немецким ученым-компьютерщиком Йохеном Лидтке в ответ на плохую производительность более ранних ОС на основе микроядра. Лидтке считал, что система, изначально спроектированная для высокой производительности, а не для других целей, может создать микроядро практического использования. коде , написанном вручную Intel i386 для Его первоначальная реализация на ассемблерном , в 1993 году привлекла внимание тем, что была в 20 раз быстрее, чем Mach . [1] Следующая публикация два года спустя [2] считался настолько влиятельным, что получил ACM SIGOPS награду Зала славы 2015 года . С момента своего появления L4 разрабатывался как кроссплатформенный и улучшающий безопасность , изоляцию и надежность .
Были различные повторные реализации исходного ядра бинарного интерфейса приложения L4 (ABI) и его преемников, включая L4Ka::Pistachio (реализованный Лидтке и его студентами в Технологическом институте Карлсруэ ), L4/MIPS ( Университет Нового Южного Уэльса). (UNSW)), Фиаско ( Дрезденский технологический университет (TU Dresden)). По этой причине название L4 было обобщено и больше не относится только к исходной реализации Лидтке. Теперь это применимо ко всему семейству микроядер, ядра L4 включая интерфейс и его различные версии.
L4 широко распространен. Один вариант, OKL4 от Open Kernel Labs , поставляется на миллиардах мобильных устройств. [3] [4]
Парадигма дизайна [ править ]
Конкретизируя общую идею микроядра , Лидтке утверждает :
Концепция допускается внутри микроядра только в том случае, если ее перемещение за пределы ядра, т. е. разрешение конкурирующих реализаций, помешало бы реализации требуемой функциональности системы. [2]
В этом духе микроядро L4 предоставляет несколько основных механизмов: адресные пространства (абстрагирование таблиц страниц и обеспечение защиты памяти), потоки и планирование (абстрагирование выполнения и обеспечение временной защиты) и межпроцессное взаимодействие (для контролируемого взаимодействия через границы изоляции).
Операционная система, основанная на микроядре, таком как L4, предоставляет службы в качестве серверов в пользовательском пространстве , которые монолитные ядра , такие как Linux , или микроядра старшего поколения включают внутри себя. Например, чтобы реализовать безопасную Unix-подобную систему, серверы должны обеспечивать управление правами, которое Mach включил в ядро.
История [ править ]
Низкая производительность микроядер первого поколения, таких как Mach , побудила ряд разработчиков пересмотреть всю концепцию микроядра в середине 1990-х годов. Концепция асинхронной коммуникации процессов с буферизацией внутри ядра , используемая в Mach, оказалась одной из основных причин его плохой производительности. Это побудило разработчиков операционных систем на базе Mach переместить некоторые критичные по времени компоненты, такие как файловые системы или драйверы, обратно в ядро. [ нужна цитата ] Хотя это несколько улучшило проблемы с производительностью, оно явно нарушает концепцию минимальности настоящего микроядра (и лишает его основных преимуществ).
Детальный анализ узкого места Маха показал, что, среди прочего, его рабочий набор слишком велик: код IPC выражает плохую пространственную локальность; то есть это приводит к слишком большому количеству промахов в кэше , большинство из которых происходят в ядре. [2] Этот анализ породил принцип, согласно которому эффективное микроядро должно быть достаточно маленьким, чтобы большая часть критически важного для производительности кода помещалась в кэш (первого уровня) (предпочтительно небольшую часть указанного кэша).
Л3 [ править ]
Йохен Лидтке намеревался доказать, что хорошо спроектированный более тонкий уровень межпроцессного взаимодействия (IPC) с тщательным вниманием к производительности и машинно-ориентированному проектированию (в отличие от кроссплатформенного программного обеспечения ) может привести к значительному повышению реальной производительности. Вместо сложной системы IPC Маха его микроядро L3 просто передавало сообщение без каких-либо дополнительных затрат. Определение и реализация необходимой политики безопасности считались обязанностями серверов пользовательского пространства . Роль ядра заключалась только в обеспечении необходимого механизма, позволяющего серверам пользовательского уровня применять политики. L3, разработанная в 1988 году, зарекомендовала себя как безопасная и надежная операционная система , используемая в течение многих лет, например, Technischer Überwachungsverein (Ассоциация технического надзора). [ нужна цитата ]
Л4 [ править ]
После некоторого опыта использования L3 Лидтке пришел к выводу, что некоторые другие концепции Маха также неуместны. Еще больше упростив концепцию микроядра, он разработал первое ядро L4, которое в первую очередь было разработано для обеспечения высокой производительности. Для максимизации производительности всё ядро было написано на языке ассемблера , а его IPC был в 20 раз быстрее, чем у Маха. [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 Дрезденского технического университета начала разработку собственной C++-реализации интерфейса ядра L4 под названием L4/Fiasco. В отличие от L4Ka::Hazelnut, который не допускает параллелизма в ядре, и его преемника L4Ka::Pistachio, который допускает прерывания в ядре только в определенных точках вытеснения, L4/Fiasco был полностью вытесняемым (за исключением чрезвычайно коротких атомных прерываний). операций) для достижения низкой задержки прерывания . Это было сочтено необходимым, поскольку в качестве основы DROPS используется L4/Fiasco. [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 г.). [update]) (по имени Л 4 Линукс ).
Нового Южного Уэльса 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 внедряет версию L4 от NICTA на своих наборах микросхем модемов мобильных станций . Это привело к использованию L4 в мобильных телефонах , продаваемых с конца 2006 года. В августе 2006 года руководитель ERTOS и профессор UNSW Гернот Хейзер основал компанию Open Kernel Labs (OK Labs) для поддержки коммерческих пользователей L4 и дальнейшей разработки L4 для коммерческое использование под торговой маркой OKL4 в тесном сотрудничестве с NICTA. OKL4 μKernel версии 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.
В начале 2012 года поставки OKL4 превысили 1,5 миллиарда. [4] в основном на чипах беспроводных модемов Qualcomm. Другие варианты внедрения включают автомобильные информационно-развлекательные системы. [13]
Apple серии A Процессоры , начиная с A7, Secure Enclave содержат сопроцессор под управлением операционной системы L4. [14] называется sepOS (Secure Enclave Processor OS) на основе встроенного ядра L4, разработанного в NICTA в 2006 году. [15] В результате L4 поставляется на всех современных устройствах Apple, включая компьютеры Mac с процессором Apple . Только в 2015 году общий объем поставок iPhone оценивался в 310 миллионов штук. [16]
Высокая надежность: seL4 [ править ]
В 2006 году группа NICTA начала с нуля разработку микроядра третьего поколения , получившего название seL4, с целью обеспечить основу для высокозащищенных и надежных систем, подходящих для удовлетворения требований безопасности, таких как требования Common Criteria и выше. С самого начала разработка была направлена на формальную проверку ядра. Чтобы облегчить выполнение иногда противоречивых требований производительности и проверки, команда использовала промежуточный программный процесс, начиная с исполняемой спецификации , написанной на языке Haskell . [17] seL4 использует управление доступом на основе возможностей , чтобы обеспечить формальное обоснование доступности объекта.
Формальное доказательство функциональной корректности было завершено в 2009 году. [18] Доказательство дает гарантию того, что реализация ядра соответствует спецификации, и подразумевает, что оно не содержит ошибок реализации, таких как взаимоблокировки , живые блокировки , переполнение буфера , арифметические исключения или использование неинициализированных переменных . seL4 считается первым проверенным ядром операционной системы общего назначения. [18] Работа над seL4 получила ACM SIGOPS награду Зала славы 2019 года .
seL4 использует новый подход к управлению ресурсами ядра. [19] экспортирует управление ресурсами ядра на уровень пользователя и подвергает их тому же контролю доступа на основе возможностей, что и к пользовательским ресурсам. Эта модель, которая также была принята Barrelfish , упрощает рассуждения о свойствах изоляции и послужила основой для последующих доказательств того, что seL4 обеспечивает соблюдение основных свойств безопасности, таких как целостность и конфиденциальность. [20] Команда NICTA также доказала корректность трансляции с языка программирования C в исполняемый машинный код , выведя компилятор из доверенной вычислительной базы seL4. [21] Это означает, что доказательства безопасности высокого уровня справедливы для исполняемого файла ядра. seL4 также является первым опубликованным ядром ОС с защищенным режимом и полным и надежным анализом времени выполнения в наихудшем случае (WCET), что является необходимым условием для его использования в вычислениях в жестком режиме реального времени . [20]
29 июля 2014 года NICTA и General Dynamics C4 Systems объявили, что seL4 со сквозными проверками теперь выпускается под лицензиями с открытым исходным кодом . [22] ядра Исходный код и доказательства лицензируются по лицензии GNU General Public License версии 2 (GPLv2), а большинство библиотек и инструментов находятся под 2-пунктом BSD . В апреле 2020 года было объявлено, что SeL4 Foundation был создан под эгидой Linux Foundation для ускорения разработки и развертывания seL4. [23]
Исследователи заявляют, что стоимость формальной проверки программного обеспечения ниже, чем стоимость разработки традиционного программного обеспечения «высокой надежности», несмотря на то, что оно обеспечивает гораздо более надежные результаты. [24] В частности, стоимость одной строки кода во время разработки seL4 оценивалась примерно в 400 долларов США по сравнению с 1000 долларов США для традиционных систем высокой надежности. [25]
Агентства перспективных исследовательских проектов Министерства обороны ( DARPA В рамках программы High-Assurance Cyber Military Systems (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 года .
В 2023 году seL4 выиграл премию ACM Software System Award .
и разработки Другие исследования
Osker, операционная система, написанная на Haskell , ориентирована на спецификацию L4; хотя этот проект был сосредоточен в основном на использовании функционального языка программирования для разработки ОС, а не на исследовании микроядра. [28]
РедоксОС [29] — это операционная система на основе Rust, которая также вдохновлена seL4 и использует дизайн микроядра.
КодЗеро [30] — это микроядро L4 для встраиваемых систем с упором на виртуализацию и реализацию собственных служб ОС. Существует версия под лицензией GPL . [31] и версия, лицензия на которую была повторно лицензирована B Labs Ltd., приобретена Nvidia как с закрытым исходным кодом и разветвлена в 2010 году. [32] [33]
микроядро F9, [34] реализация L4 под лицензией BSD, предназначенная для процессоров ARM Cortex-M для глубоко встраиваемых устройств с защитой памяти.
Архитектура виртуализации ОС NOVA [35] это исследовательский проект, направленный на создание безопасной и эффективной среды виртуализации. [36] [37] с небольшой доверенной вычислительной базой. NOVA состоит из микрогипервизора, гипервизора пользовательского уровня ( монитора виртуальной машины ) и работающей на нем непривилегированной компонентной многосерверной пользовательской среды с именем NUL. NOVA работает на многоядерных системах на базе ARMv8-A и x86.
ВрмОС [38] — операционная система реального времени, основанная на микроядре L4. Он имеет собственные реализации ядра, стандартных библиотек и сетевого стека, поддерживая архитектуры ARM, SPARC, x86 и x86-64. Есть паравиртуализированное ядро Linux (w4linux [39] ) работаю на WrmOS.
Helios — это микроядро, созданное на основе seL4. [40] Он является частью операционной системы Ares, поддерживает x86-64 и aarch64 и по состоянию на февраль 2023 года все еще находится в активной разработке. [41]
См. также [ править ]
Ссылки [ править ]
- ^ Перейти обратно: а б Лидтке, Йохен (декабрь 1993 г.). «Улучшение IPC путем проектирования ядра» . 14-й симпозиум ACM по принципам операционных систем . Эшвилл, Северная Каролина, США. стр. 175–188.
- ^ Перейти обратно: а б с Лидтке, Йохен (декабрь 1995 г.). «О построении μ-ядра» . Материалы 15-го симпозиума ACM по принципам операционных систем (SOSP) . стр. 237–250. Архивировано из оригинала 25 октября 2015 года.
- ^ «Продукты для гипервизоров: системы миссии General Dynamics» . Системы миссии General Dynamics . Архивировано из оригинала 15 ноября 2017 года . Проверено 26 апреля 2018 г.
- ^ Перейти обратно: а б «Программное обеспечение Open Kernel Labs превысило отметку в 1,5 миллиарда поставок мобильных устройств» (пресс-релиз). Откройте лабораторию ядра . 19 января 2012 г. Архивировано из оригинала 11 февраля 2012 г.
- ^ Жеффло, Ален; Джагер, Трент; Пак, Юнхо; Лидтке, Йохен ; Эльфинстон, Кевин; Улиг, Фолькмар; Тидсвелл, Джонатон; Деллер, Люк; Рейтер, Ларс (2000). «Мультисерверный подход Sawmill» . Европейский семинар ACM SIGOPS . Колдинг, Дания. стр. 109–114.
- ^ «DROPS – Обзор» . Дрезденский технологический университет . Архивировано из оригинала 7 августа 2011 года . Проверено 10 августа 2011 г.
- ^ l4ka.org: Микроядро L4Ka::Pistachio Цитата: «...Разнообразие поддерживаемых архитектур делает L4Ka::Pistachio идеальной платформой для исследований и разработок для широкого спектра систем...»
- ^ Грей, Чарльз; Чепмен, Мэтью; Чабб, Питер; Мосбергер-Танг, Дэвид; Хайзер, Гернот (апрель 2005 г.). «Итаниум: рассказ системного разработчика» . Ежегодная техническая конференция USENIX . Аннахайм, Калифорния, США. стр. 264–278. Архивировано из оригинала 17 февраля 2007 года.
- ^ Лесли, Бен; Чабб, Питер; Фицрой-Дейл, Николас; Гетц, Стефан; Грей, Чарльз; Макферсон, Люк; Поттс, Дэниел; Шен, Юетинг; Эльфинстон, Кевин; Хайзер, Гернот (сентябрь 2005 г.). «Драйверы устройств пользовательского уровня: достигнутая производительность». Журнал компьютерных наук и технологий . 20 (5): 654–664. CiteSeerX 10.1.1.59.6766 . дои : 10.1007/s11390-005-0654-4 . S2CID 1121537 .
- ^ ван Шайк, Карл; Хейзер, Гернот (январь 2007 г.). «Высокопроизводительные микроядра и виртуализация на ARM и сегментированных архитектурах» . 1-й международный семинар по микроядрам для встраиваемых систем . Сидней, Австралия: НИКТА . стр. 11–21. Архивировано из оригинала 1 марта 2015 года . Проверено 25 октября 2015 г.
- ^ Руокко, Серджио (октябрь 2008 г.). «Экскурсия программиста реального времени по микроядрам L4 общего назначения» . Журнал EURASIP по встраиваемым системам . 2008 : 1–14. дои : 10.1155/2008/234710 . S2CID 7430332 .
- ^ «Микроядро NICTA L4 будет использоваться в некоторых наборах микросхем QUALCOMM» (пресс-релиз). НИКТА . 24 ноября 2005 г. Архивировано из оригинала 25 августа 2006 г.
- ^ «Автомобильная виртуализация Open Kernel Labs, выбранная Bosch для информационно-развлекательных систем» (пресс-релиз). Откройте лабораторию ядра . 27 марта 2012 г. Архивировано из оригинала 2 июля 2012 г.
- ^ «Безопасность iOS, iOS 12.3» (PDF) . Apple Inc., май 2019 г. Архивировано (PDF) из оригинала 24 июня 2020 г.
- ^ Мандт, Тарьей; Сольник, Мэтью; Ван, Дэвид (31 июля 2016 г.). «Демистификация процессора Secure Enclave» (PDF) . Блэкхэт США . Лас-Вегас, Невада, США. Архивировано (PDF) из оригинала 21 октября 2016 г.
- ^ Элмер-ДеВитт, Филип (28 октября 2014 г.). «Прогноз: в 2015 году Apple выпустит 310 миллионов iOS-устройств» . Удача . Архивировано из оригинала 27 сентября 2015 года . Проверено 25 октября 2015 г.
- ^ Деррин, Филип; Эльфинстон, Кевин; Кляйн, Гервин; Кок, Дэвид; Чакраварти, Мануэль М.Т. (сентябрь 2006 г.). «Выполнение руководства: подход к высоконадежной разработке микроядра» . Семинар по Haskell ACM SIGPLAN . Портланд, штат Орегон . стр. 60–71.
- ^ Перейти обратно: а б Кляйн, Гервин; Эльфинстон, Кевин; Хайзер, Гернот ; Андроник, июнь; Кок, Дэвид; Деррин, Филип; Элькадуве, Дхаммика; Энгельхардт, Кай; Колански, Рафаль; Норриш, Майкл; Сьюэлл, Томас; Тач, Харви; Уинвуд, Саймон (октябрь 2009 г.). «seL4: формальная проверка ядра ОС» (PDF) . 22-й симпозиум ACM по принципам работы операционных систем . Биг Скай, Монтана, США. Архивировано (PDF) из оригинала 28 июля 2011 года.
- ^ Элькадуве, Дхаммика; Деррин, Филип; Эльфинстон, Кевин (апрель 2008 г.). Конструкция ядра для изоляции и обеспечения физической памяти . 1-й семинар по изоляции и интеграции встраиваемых систем. Глазго, Великобритания. дои : 10.1145/1435458 . Архивировано из оригинала 22 февраля 2020 года . Проверено 22 февраля 2020 г. .
- ^ Перейти обратно: а б Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хайзер, Гернот (февраль 2014 г.). «Комплексная формальная верификация микроядра ОС». Транзакции ACM в компьютерных системах . 32 (1): 2:1–2:70. CiteSeerX 10.1.1.431.9140 . дои : 10.1145/2560537 . S2CID 4474342 .
- ^ Сьюэлл, Томас; Мирин, Магнус; Кляйн, Гервин (июнь 2013 г.). «Проверка перевода проверенного ядра ОС» . Конференция ACM SIGPLAN по проектированию и реализации языков программирования . Сиэтл, Вашингтон, США. дои : 10.1145/2491956.2462183 .
- ^ «Безопасная операционная система, разработанная NICTA, становится открытой» (Пресс-релиз). НИКТА . 29 июля 2014 г. Архивировано из оригинала 15 марта 2016 г.
- ^ «Безопасность получает поддержку Linux Foundation» (пресс-релиз). Фонд Linux . 7 апреля 2020 г. Архивировано из оригинала 15 марта 2016 г.
- ^ Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хейзер, Гернот (2014). «Комплексная формальная проверка микроядра ОС» (PDF) . Транзакции ACM в компьютерных системах . 32:64 . CiteSeerX 10.1.1.431.9140 . дои : 10.1145/2560537 . S2CID 4474342 . Архивировано (PDF) из оригинала 3 августа 2014 года.
- ^ Хайзер, Гернот (16 января 2015 г.). seL4 бесплатен: что это значит для вас? . Окленд, Новая Зеландия: Linux.conf.au.
- ^ «DARPA выбирает Rockwell Collins для применения технологий кибербезопасности на новых платформах» (пресс-релиз). Рокуэлл Коллинз . 24 апреля 2017 г. Архивировано из оригинала 11 мая 2017 г.
- ^ «Спонсор агентства DARPA доктор Джон Лаунбери» . СБИРИсточник . 2017. Архивировано из оригинала 29 сентября 2017 года . Проверено 16 мая 2017 г.
- ^ Халлгрен, Т.; Джонс, член парламента; Лесли, Р.; Толмач, А. (2005). «Принципиальный подход к построению операционной системы на Haskell» (PDF) . Уведомления ACM SIGPLAN . 40 (9): 116–128. дои : 10.1145/1090189.1086380 . ISSN 0362-1340 . Архивировано (PDF) из оригинала 15 июня 2010 г. Проверено 24 июня 2010 г.
- ^ «РедокОС» . РедоксОС .
- ^ «Анонс: представляем Codezero» . Дрезденский технологический университет .
- ^ «jserv/codezero: микроядро Codezero» . Гитхаб . Архивировано из оригинала 15 августа 2015 года . Проверено 20 октября 2020 г.
- ^ «Код Ноль: Встроенный гипервизор и ОС» . Архивировано из оригинала 11 января 2016 года . Проверено 25 января 2016 г.
- ^ «B Labs | Решения для мобильной виртуализации, виртуализация Android и Linux для архитектуры ARM» . Архивировано из оригинала 2 февраля 2014 года . Проверено 2 февраля 2014 г.
- ^ «Микроядро F9» . Гитхаб . Проверено 20 октября 2020 г.
- ^ «Сайт NOVA Microhypervisor» . Проверено 9 января 2021 г.
- ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). «NOVA: Архитектура безопасной виртуализации на основе микрогипервизора». EuroSys '10: Материалы 5-й Европейской конференции по компьютерным системам . Париж, Франция .
- ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). «На пути к масштабируемой многопроцессорной среде пользовательского уровня». IIDS'10: Семинар по изоляции и интеграции надежных систем . Париж, Франция .
- ^ «ВрмОС» . Проверено 20 октября 2020 г.
- ^ «w4linux — это паравиртуализированное ядро Linux, работающее на WrmOS» . Проверено 20 октября 2020 г.
- ^ "~sircmpwn/helios — Экспериментальное микроядро — sourcehut git" . git.sr.ht. Проверено 20 февраля 2023 г.
- ^ «Гелиос» . ares-os.org . Проверено 20 февраля 2023 г.
Дальнейшее чтение [ править ]
- Лидтке, Йохен ; Бартлинг, Ульрих; Бейер, Уве; Генрихс, Дитмар; Руланд, Рудольф; Салай, Дьюла (апрель 1991 г.). «Два года опыта работы с ОС на базе μ-Kernel» . Обзор операционных систем ACM SIGOPS . 25 (2): 51–62. дои : 10.1145/122120.122124 . S2CID 17602151 .
- Лидтке, Йохен ; Хеберлен, Андреас; Пак, Юнхо; Ройтер, Ларс; Улиг, Фолькмар (22 октября 2000 г.). «Производительность стаб-кода становится важной» . Материалы 1-го семинара по промышленному опыту использования системного программного обеспечения (WIESS), Сан-Диего, Калифорния, октябрь 2000 г. Архивировано из оригинала (PDF) 5 сентября 2006 года . Проверено 5 сентября 2006 г. (на ядре L4 и компиляторе)
- Ченг, Гуанхуэй; Макгуайр, Николас. Кикстарт L4/Fiasco/L4Linux (PDF) . Лаборатория распределенных и встраиваемых систем (Отчет). Ланьчжоуский университет. Архивировано из оригинала (PDF) 27 марта 2012 года.
- Эльфинстон, Кевин; Хейзер, Гернот (ноябрь 2013 г.). «От L3 к seL4: чему мы научились за 20 лет микроядер L4?» (PDF) . 24-й симпозиум ACM SIGOPS по принципам работы операционных систем . Фармингтон, Пенсильвания, США. стр. 133–150. CiteSeerX 10.1.1.636.9410 . дои : 10.1145/2517349.2522720 . ISBN 978-1-4503-2388-8 . Эволюция подходов к проектированию и реализации L4
Внешние ссылки [ править ]
- L4Hq: штаб-квартира L4, сайт сообщества для проектов L4. Архивировано 25 октября 2019 г. на Wayback Machine.
- The L4 μ-Kernel Family , обзор реализаций L4, документация, проекты
- Официальная вики по TUD:OS
- L4Ka : Реализации L4Ka::Pistachio и L4Ka::Hazelnut
- Официальный сайт , seL4
- UNSW : Реализации архитектуры DEC Alpha и MIPS.
- OKL4. Архивировано 20 августа 2008 г. на Wayback Machine : коммерческая версия L4 из Open Kernel Labs. Архивировано 19 марта 2009 г. на Wayback Machine.
- NICTA L4 : Обзор исследования и архив публикаций] 17 июля 2014 г. на Wayback Machine
- Группа Trustworthy Systems в Data61 CSIRO : нынешний дом бывшей группы NICTA, разработавшей seL4.
- Genode Operating System Framework : детище сообщества L4.
