✖


Jump to content

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

(Перенаправлено с SeL4 )

Семейство микроядер L4
Разработчик Йохен Лидтке
Написано в Язык ассемблера , затем C , C++
Семейство ОС Л4
Рабочее состояние Текущий
Исходная модель Открытый исходный код , закрытый исходный код
Первоначальный выпуск 1993 год ; 31 год назад ( 1993 )
Маркетинговая цель Надежные вычисления
Доступно в английский, немецкий
Платформы Intel i386 , x86 , x86-64 , ARM , MIPS , SPARC , Itanium , RISC-V
ядра Тип Микроядро
Лицензия Исходный код , доказательства : GPLv2.
Библиотеки , инструменты : 2-пункт BSD
Предшественник Юмель
Официальный сайт ты .inf .здесь-Дрезден .из /L4

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 (Ассоциация технического надзора). [ нужна ссылка ]

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

Л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 г.). ) (по имени Л 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]

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

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

  1. ^ Jump up to: Перейти обратно: а б Лидтке, Йохен (декабрь 1993 г.). «Улучшение IPC путем проектирования ядра» . 14-й симпозиум ACM по принципам работы операционных систем . Эшвилл, Северная Каролина, США. стр. 175–188.
  2. ^ Jump up to: Перейти обратно: а б с Лидтке, Йохен (декабрь 1995 г.). «О построении μ-ядра» . Материалы 15-го симпозиума ACM по принципам операционных систем (SOSP) . стр. 237–250. Архивировано из оригинала 25 октября 2015 года.
  3. ^ «Продукты для гипервизоров: системы миссии General Dynamics» . Системы миссии General Dynamics . Архивировано из оригинала 15 ноября 2017 года . Проверено 26 апреля 2018 г.
  4. ^ Jump up to: Перейти обратно: а б «Программное обеспечение Open Kernel Labs превысило отметку в 1,5 миллиарда поставок мобильных устройств» (пресс-релиз). Откройте лабораторию ядра . 19 января 2012 г. Архивировано из оригинала 11 февраля 2012 г.
  5. ^ Жеффло, Ален; Джагер, Трент; Пак, Юнхо; Лидтке, Йохен ; Эльфинстон, Кевин; Улиг, Фолькмар; Тидсвелл, Джонатон; Деллер, Люк; Рейтер, Ларс (2000). «Мультисерверный подход Sawmill» . Европейский семинар ACM SIGOPS . Колдинг, Дания. стр. 109–114.
  6. ^ «DROPS – Обзор» . Дрезденский технологический университет . Архивировано из оригинала 7 августа 2011 года . Проверено 10 августа 2011 г.
  7. ^ l4ka.org: Микроядро L4Ka::Pistachio Цитата: «...Разнообразие поддерживаемых архитектур делает L4Ka::Pistachio идеальной платформой для исследований и разработок для широкого спектра систем...»
  8. ^ Грей, Чарльз; Чепмен, Мэтью; Чабб, Питер; Мосбергер-Танг, Дэвид; Хайзер, Гернот (апрель 2005 г.). «Итаниум: рассказ системного разработчика» . Ежегодная техническая конференция USENIX . Аннахайм, Калифорния, США. стр. 264–278. Архивировано из оригинала 17 февраля 2007 года.
  9. ^ Лесли, Бен; Чабб, Питер; Фицрой-Дейл, Николас; Гетц, Стефан; Грей, Чарльз; Макферсон, Люк; Поттс, Дэниел; Шен, Юетинг; Эльфинстон, Кевин; Хайзер, Гернот (сентябрь 2005 г.). «Драйверы устройств пользовательского уровня: достигнутая производительность». Журнал компьютерных наук и технологий . 20 (5): 654–664. CiteSeerX   10.1.1.59.6766 . дои : 10.1007/s11390-005-0654-4 . S2CID   1121537 .
  10. ^ ван Шайк, Карл; Хейзер, Гернот (январь 2007 г.). «Высокопроизводительные микроядра и виртуализация на ARM и сегментированных архитектурах» . 1-й международный семинар по микроядрам для встраиваемых систем . Сидней, Австралия: НИКТА . стр. 11–21. Архивировано из оригинала 1 марта 2015 года . Проверено 25 октября 2015 г.
  11. ^ Руокко, Серджио (октябрь 2008 г.). «Экскурсия программиста реального времени по микроядрам L4 общего назначения» . Журнал EURASIP по встраиваемым системам . 2008 : 1–14. дои : 10.1155/2008/234710 . S2CID   7430332 .
  12. ^ «Микроядро NICTA L4 будет использоваться в некоторых наборах микросхем QUALCOMM» (пресс-релиз). НИКТА . 24 ноября 2005 г. Архивировано из оригинала 25 августа 2006 г.
  13. ^ «Автомобильная виртуализация Open Kernel Labs, выбранная Bosch для информационно-развлекательных систем» (пресс-релиз). Откройте лабораторию ядра . 27 марта 2012 г. Архивировано из оригинала 2 июля 2012 г.
  14. ^ «Безопасность iOS, iOS 12.3» (PDF) . Apple Inc., май 2019 г. Архивировано (PDF) из оригинала 24 июня 2020 г.
  15. ^ Мандт, Тарьей; Сольник, Мэтью; Ван, Дэвид (31 июля 2016 г.). «Демистификация процессора Secure Enclave» (PDF) . Блэкхэт США . Лас-Вегас, Невада, США. Архивировано (PDF) из оригинала 21 октября 2016 г.
  16. ^ Элмер-ДеВитт, Филип (28 октября 2014 г.). «Прогноз: в 2015 году Apple выпустит 310 миллионов iOS-устройств» . Удача . Архивировано из оригинала 27 сентября 2015 года . Проверено 25 октября 2015 г.
  17. ^ Деррин, Филип; Эльфинстон, Кевин; Кляйн, Гервин; Кок, Дэвид; Чакраварти, Мануэль М.Т. (сентябрь 2006 г.). «Выполнение руководства: подход к высоконадежной разработке микроядра» . Семинар по Haskell ACM SIGPLAN . Портленд, Орегон . стр. 60–71.
  18. ^ Jump up to: Перейти обратно: а б Кляйн, Гервин; Эльфинстон, Кевин; Хайзер, Гернот ; Андроник, июнь; Кок, Дэвид; Деррин, Филип; Элькадуве, Дхаммика; Энгельхардт, Кай; Колански, Рафаль; Норриш, Майкл; Сьюэлл, Томас; Тач, Харви; Уинвуд, Саймон (октябрь 2009 г.). «seL4: формальная проверка ядра ОС» (PDF) . 22-й симпозиум ACM по принципам работы операционных систем . Биг Скай, Монтана, США. Архивировано (PDF) из оригинала 28 июля 2011 года.
  19. ^ Элькадуве, Дхаммика; Деррин, Филип; Эльфинстон, Кевин (апрель 2008 г.). Конструкция ядра для изоляции и обеспечения физической памяти . 1-й семинар по изоляции и интеграции встраиваемых систем. Глазго, Великобритания. дои : 10.1145/1435458 . Архивировано из оригинала 22 февраля 2020 года . Проверено 22 февраля 2020 г. .
  20. ^ Jump up to: Перейти обратно: а б Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хайзер, Гернот (февраль 2014 г.). «Комплексная формальная верификация микроядра ОС». Транзакции ACM в компьютерных системах . 32 (1): 2:1–2:70. CiteSeerX   10.1.1.431.9140 . дои : 10.1145/2560537 . S2CID   4474342 .
  21. ^ Сьюэлл, Томас; Мирин, Магнус; Кляйн, Гервин (июнь 2013 г.). «Проверка перевода проверенного ядра ОС» . Конференция ACM SIGPLAN по проектированию и реализации языков программирования . Сиэтл, Вашингтон, США. дои : 10.1145/2491956.2462183 .
  22. ^ «Безопасная операционная система, разработанная NICTA, становится открытой» (Пресс-релиз). НИКТА . 29 июля 2014 г. Архивировано из оригинала 15 марта 2016 г.
  23. ^ «Безопасность получает поддержку Linux Foundation» (пресс-релиз). Фонд Linux . 7 апреля 2020 г. Архивировано из оригинала 15 марта 2016 г.
  24. ^ Кляйн, Гервин; Андроник, июнь; Эльфинстон, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафаль; Хейзер, Гернот (2014). «Комплексная формальная проверка микроядра ОС» (PDF) . Транзакции ACM в компьютерных системах . 32:64 . CiteSeerX   10.1.1.431.9140 . дои : 10.1145/2560537 . S2CID   4474342 . Архивировано (PDF) из оригинала 3 августа 2014 г.
  25. ^ Хайзер, Гернот (16 января 2015 г.). seL4 бесплатен: что это значит для вас? . Окленд, Новая Зеландия: Linux.conf.au.
  26. ^ «DARPA выбирает Rockwell Collins для применения технологий кибербезопасности на новых платформах» (пресс-релиз). Рокуэлл Коллинз . 24 апреля 2017 г. Архивировано из оригинала 11 мая 2017 г.
  27. ^ «Спонсор агентства DARPA доктор Джон Лаунбери» . СБИРИсточник . 2017. Архивировано из оригинала 29 сентября 2017 года . Проверено 16 мая 2017 г.
  28. ^ Халлгрен, Т.; Джонс, член парламента; Лесли, Р.; Толмач, А. (2005). «Принципиальный подход к построению операционной системы на Haskell» (PDF) . Уведомления ACM SIGPLAN . 40 (9): 116–128. дои : 10.1145/1090189.1086380 . ISSN   0362-1340 . Архивировано (PDF) из оригинала 15 июня 2010 г. Проверено 24 июня 2010 г.
  29. ^ «РедокОС» . РедоксОС .
  30. ^ «Анонс: представляем Codezero» . Дрезденский технологический университет .
  31. ^ «jserv/codezero: микроядро Codezero» . Гитхаб . Архивировано из оригинала 15 августа 2015 года . Проверено 20 октября 2020 г.
  32. ^ «Код Ноль: Встроенный гипервизор и ОС» . Архивировано из оригинала 11 января 2016 года . Проверено 25 января 2016 г.
  33. ^ «B Labs | Решения для мобильной виртуализации, виртуализация Android и Linux для архитектуры ARM» . Архивировано из оригинала 2 февраля 2014 года . Проверено 2 февраля 2014 г.
  34. ^ «Микроядро F9» . Гитхаб . Проверено 20 октября 2020 г.
  35. ^ «Сайт NOVA Microhypervisor» . Проверено 9 января 2021 г.
  36. ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). «NOVA: Архитектура безопасной виртуализации на основе микрогипервизора». EuroSys '10: Материалы 5-й Европейской конференции по компьютерным системам . Париж, Франция .
  37. ^ Стейнберг, Удо; Кауэр, Бернхард (апрель 2010 г.). «На пути к масштабируемой многопроцессорной среде пользовательского уровня». IIDS'10: Семинар по изоляции и интеграции надежных систем . Париж, Франция .
  38. ^ «ВрмОС» . Проверено 20 октября 2020 г.
  39. ^ «w4linux — это паравиртуализированное ядро ​​Linux, работающее на WrmOS» . Проверено 20 октября 2020 г.
  40. ^ "~sircmpwn/helios — Экспериментальное микроядро — sourcehut git" . git.sr.ht. ​Проверено 20 февраля 2023 г.
  41. ^ «Гелиос» . ares-os.org . Проверено 20 февраля 2023 г.

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

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

Retrieved from "https://en.wikipedia.org/w/index.php?title=L4_microkernel_family&oldid=1229618215#High_assurance:_seL4"
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 79772c6670b38ea391312446949e238c__1718644080
URL1:https://arc.ask3.ru/arc/aa/79/8c/79772c6670b38ea391312446949e238c.html
Заголовок, (Title) документа по адресу, URL1:
L4 microkernel family - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)