Войти
L4- это семейство микроядер второго поколения, обычно используемых для реализации Unix-подобных операционные системы, но также используются во множестве других систем.
L4, как и его предшественник микроядро L3, был создан немецким компьютерным ученым Йохеном Лидтке в ответ на низкая производительность более ранних операционных систем на базе микроядра. Лидтке считал, что система, разработанная с самого начала для обеспечения высокой производительности, а не для других целей, может создать микроядро для практического использования. Его первоначальная реализация в коде Intel i386, специфичного для языка, написанного вручную, в 1993 году вызвала большой интерес в компьютерной индустрии. С момента своего появления L4 был разработан для независимости от платформы, а также для улучшения безопасности, изоляции и устойчивости.
Были различные повторные реализации исходного двоичного файла. Интерфейс ядра L4 (ABI ) и его преемники, включая L4Ka :: Pistachio (Uni Karlsruhe ), L4 / MIPS (UNSW ), Fiasco (TU Dresden ). По этой причине имя L4 было обобщено и больше не относится только к исходной реализации Лидтке. Теперь он применяется ко всему семейству микроядра, включая L4 kernel интерфейс и его различные версии.
L4 широко используется. Один вариант, OKL4 от Open Kernel Labs, был доставлен в миллиардах мобильных устройств.
Определение общей идеи микроядро, Лидтке заявляет:
Концепция допускается внутри микроядра только в том случае, если ее перенос за пределы ядра, т. Е. Разрешение конкурирующих реализаций, помешает реализации требуемой функциональности системы.
В этом духе микроядро L4 предоставляет несколько основных механизмов: адресные пространства (абстрагирование таблиц страниц и обеспечение защиты памяти), потоки и планирование ( абстрагирование исполняемого ion и обеспечение временной защиты) и межпроцессное взаимодействие (для управляемой связи через границы изоляции).
Операционная система, основанная на микроядре, таком как L4, предоставляет услуги в качестве серверов в пользовательском пространстве, которое включает монолитные ядра, такие как Linux или микроядра предыдущего поколения. внутренне. Например, чтобы реализовать безопасную Unix-подобную систему, серверы должны обеспечивать управление правами, которое Mach включено в ядро.
Низкая производительность микроядер первого поколения, таких как Mach, вынудила ряд разработчиков пересмотреть всю концепцию микроядра в середине 1990-х.. Концепция асинхронной буферизации внутри ядра процесса взаимодействия, используемая в Mach, оказалась одной из основных причин его низкой производительности. Это побудило разработчиков операционных систем на базе Mach переместить некоторые критичные ко времени компоненты, такие как файловые системы или драйверы, обратно внутрь ядра. Хотя это несколько уменьшило проблемы с производительностью, это явно нарушает концепцию минимальности настоящего микроядра (и упускает их основные преимущества).
Детальный анализ узкого места Маха показал, что, среди прочего, его рабочий набор слишком велик: код IPC выражает плохую пространственную локальность; то есть, это приводит к слишком большому количеству промахов кеша, большинство из которых происходит внутри ядра. Этот анализ привел к появлению принципа, согласно которому эффективное микроядро должно быть достаточно маленьким, чтобы большая часть критически важного для производительности кода помещалась в кэш (первого уровня) (предпочтительно небольшую часть указанного кеша).
Йохен Лидтке намеревался доказать, что хорошо спроектированный более тонкий слой IPC с особым вниманием к характеристикам и машинно-ориентированной (в отличие от платформенно-независимой) конструкции может привести к значительному повышению производительности в реальном мире. Вместо сложной IPC-системы Маха его микроядро L3 просто передавало сообщение без дополнительных накладных расходов. Определение и реализация необходимых политик безопасности считались обязанностями серверов пространства пользователя. Роль ядра заключалась только в обеспечении необходимого механизма, позволяющего серверам пользовательского уровня применять политики. L3, разработанная в 1988 году, зарекомендовала себя как безопасная и надежная операционная система, которая в течение многих лет использовалась, например, TÜV SÜD.
семейным деревом L4 После Имея некоторый опыт использования L3, Лидтке пришел к выводу, что несколько других концепций Маха также неуместны. Еще больше упростив концепции микроядра, он разработал первое ядро L4, которое в первую очередь проектировалось с учетом высокой производительности. Чтобы выжать каждый бит производительности, все ядро было написано на языке ассемблера, и его IPC был в 20 раз быстрее, чем у Маха. Такое резкое повышение производительности - редкое явление в операционных системах, и работа Лидтке привела к появлению новых реализаций L4 и работы над системами на основе L4 в ряде университетов и исследовательских институтов, включая IBM, где Лидтке начал работать в 1996, Технический университет Дрездена и UNSW. В исследовательском центре Томаса Дж. Ватсона IBM Лидтке и его коллеги продолжили исследования систем на базе L4 и микроядра в целом, особенно ОС Sawmill.
В 1999 году Лидтке возглавил группу системной архитектуры в Университете Карлсруэ, где продолжил исследования в области микроядерных систем. В качестве доказательства концепции того, что высокопроизводительное микроядро также может быть построено на языке более высокого уровня, группа разработала L4Ka :: Hazelnut, версию ядра C ++, работающую на IA-32- и ARM- на базе машин. Эта попытка увенчалась успехом - производительность оставалась приемлемой - и с его выпуском версии ядер на чистом языке ассемблера были фактически прекращены.
Параллельно с разработкой L4Ka :: Hazelnut в 1998 г. группа операционных систем TUD: ОС Технического университета Дрездена (Дрезденский технологический университет) начали разрабатывать собственную реализацию C ++ интерфейса ядра L4, названную L4 / Fiasco. В отличие от L4Ka :: Hazelnut, который вообще не допускает параллелизма в ядре, и его преемника L4Ka :: Pistachio, который разрешает прерывания в ядре только в определенных точках вытеснения, L4 / Fiasco был полностью вытеснен (за исключением чрезвычайно коротких атомарных операций) для достижения низкой задержки прерывания . Это было сочтено необходимым, потому что L4 / Fiasco используется в качестве основы DROPS, операционной системы с поддержкой жесткого реального времени, также разработанной в Техническом университете Дрездена. Однако сложность полностью вытесняемой конструкции побудила более поздние версии Fiasco вернуться к традиционному подходу L4 к запуску ядра с отключенными прерываниями, за исключением ограниченного числа точек вытеснения.
Вплоть до выпуска L4Ka :: Pistachio и более новых версий Fiasco все микроядра L4 были неотъемлемо привязаны к базовым Архитектура процессора. Следующим большим сдвигом в разработке L4 была разработка платформенно-независимого API, который все еще сохранял высокие характеристики производительности, несмотря на более высокий уровень переносимости. Хотя основные концепции ядра остались прежними, новый API предоставил множество значительных изменений по сравнению с предыдущими версиями L4, включая лучшую поддержку многопроцессорных систем, более слабые связи между потоками и адресными пространствами и введение управления потоками на уровне пользователя. блоки (UTCB) и виртуальные регистры. После выпуска нового L4 API (версия X.2, также известная как версия 4) в начале 2001 года, группа системной архитектуры в университете Карлсруэ реализовала новое ядро L4Ka :: Pistachio, полностью с нуля, теперь с сосредоточиться как на высокой производительности, так и на портативности. Он был выпущен под лицензией BSD с двумя пунктами.
Микроядро L4 / Fiasco также значительно улучшилось за эти годы. Теперь он поддерживает несколько аппаратных платформ от x86 до AMD64 до нескольких платформ ARM. Примечательно, что версия Fiasco (Fiasco-UX) может работать как приложение пользовательского уровня поверх Linux.
L4 / Fiasco реализует несколько расширений L4v2 API. IPC исключения позволяет ядру отправлять исключения ЦП приложениям-обработчикам на уровне пользователя. С помощью чужих потоков можно выполнять детальный контроль над системными вызовами. Добавлены UTCB в стиле X.2. Кроме того, Fiasco содержит механизмы для управления правами связи, а также потреблением ресурсов на уровне ядра. На вершине Fiasco разработан набор базовых сервисов пользовательского уровня (называемых L4Env), которые, среди прочего, используются для паравиртуализации текущей версии Linux (4.19 по состоянию на май 2019 года) (называемой L4Linux ).
Разработка также велась в Университете Нового Южного Уэльса (UNSW), где разработчики реализовали L4 на нескольких 64-битных платформах.. Их работа привела к созданию L4 / MIPS и L4 / Alpha, в результате чего исходная версия Лидтке была ретроспективно названа L4 / x86 . Как и исходные ядра Liedtke, ядра UNSW (написанные на смеси ассемблера и C) были непереносимыми, и каждое реализовывалось с нуля. С выпуском сверхпортативного L4Ka :: Pistachio группа UNSW отказалась от собственных ядер в пользу производства хорошо настроенных портов L4Ka :: Pistachio, включая самую быструю из когда-либо зарегистрированных реализаций передачи сообщений (36 циклов на Itanium архитектура). Группа также продемонстрировала, что драйверы устройств пользовательского уровня могут работать так же хорошо, как драйверы в ядре, и разработала Wombat, очень переносимую версию Linux на L4, которая работает на x86, Процессоры ARM и MIPS. На процессорах XScale Wombat демонстрирует затраты на переключение контекста, которые до 50 раз ниже, чем в родном Linux.
Позже группа UNSW в своем новом доме в NICTA, разветвил L4Ka :: Pistachio в новую версию L4 под названием NICTA :: L4-embedded . Как следует из названия, это было нацелено на использование в коммерческих встроенных системах, и, следовательно, компромиссы реализации благоприятствовали небольшому объему памяти и были направлены на снижение сложности. API был изменен так, чтобы почти все системные вызовы оставались достаточно короткими, чтобы им не требовались точки приоритетного прерывания для обеспечения высокой скорости реагирования в реальном времени.
В ноябре 2005 г. NICTA объявила, что Qualcomm развертывает версию L4 NICTA на своих чипсетах Mobile Station Modem. Это привело к использованию L4 в мобильных телефонах, продаваемых с конца 2006 года. В августе 2006 года лидер ERTOS и профессор UNSW Гернот Хайзер основал компанию под названием Open Kernel Labs (OK Labs) для поддержки коммерческих пользователей L4 и дальнейшей разработки L4 для коммерческого использования под торговой маркой OKL4 в тесном сотрудничестве с NICTA. OKL4 версии 2.1, выпущенной в апреле 2008 г., была первой общедоступной версией L4, которая обеспечивала безопасность на основе возможностей. OKL4 3.0, выпущенный в октябре 2008 года, был последней версией OKL4 с открытым исходным кодом. Более поздние версии имеют закрытый исходный код и основаны на переписывании для поддержки собственного варианта гипервизора, называемого микровизором OKL4. OK Labs также распространяла паравиртуализированный Linux под названием OK: Linux, потомок Wombat, а также паравиртуализированные версии SymbianOS и Android. OK Labs также приобрела права на seL4 у NICTA.
В начале 2012 года поставки OKL4 превысили 1,5 миллиарда, в основном это были микросхемы беспроводных модемов Qualcomm. Другие варианты развертывания включают автомобильные информационно-развлекательные системы.
Процессоры Apple серии A, начиная с A7, содержат сопроцессор Secure Enclave под управлением операционной системы L4 на базе на ядре со встроенным L4, разработанном в NICTA в 2006 году. Это означает, что L4 теперь поставляется на всех устройствах iOS, общий объем поставок которых оценивается в 310 миллионов на 2015 год.
В 2006 году группа NICTA начала с нуля разработку микроядра третьего поколения, названного seL4, с целью предоставления основа для высокозащищенных и надежных систем, подходящая для удовлетворения требований безопасности, таких как Common Criteria и выше. С самого начала разработка была направлена на формальную проверку ядра. Чтобы облегчить выполнение иногда противоречивых требований к производительности и проверке, команда использовала программный процесс среднего уровня, начиная с написанного на Haskell. seL4 использует управление доступом на основе возможностей для формального рассуждения о доступности объекта.
Формальное доказательство функциональной корректности было завершено в 2009 году. Доказательство обеспечивает гарантию того, что реализация ядра соответствует его спецификации, и подразумевает, что оно не содержит ошибок реализации, таких как взаимоблокировки, живые блокировки, переполнение буфера, арифметические исключения или использование неинициализированных переменных. seL4 считается первым в истории ядром операционной системы общего назначения, которое было проверено.
seL4 использует новый подход к управлению ресурсами ядра, экспортируя управление ресурсами ядра на уровень пользователя и подвергая их тот же контроль доступа на основе возможностей, что и пользовательские ресурсы. Эта модель, которая также была принята Barrelfish, упрощает рассуждения о свойствах изоляции и была средством для более поздних доказательств того, что seL4 обеспечивает соблюдение основных свойств безопасности, таких как целостность и конфиденциальность. Команда NICTA также подтвердила правильность перевода с C в исполняемый машинный код, изъяв компилятор из доверенной вычислительной базы seL4. Это означает, что для исполняемого файла ядра сохраняются доказательства высокого уровня безопасности. seL4 также является первым опубликованным ядром ОС защищенного режима с полным и надежным анализом времени выполнения (WCET) в наихудшем случае, что является предпосылкой для его использования в жестких системах реального времени.
29 июля 2014 года NICTA и General Dynamics C4 Systems объявили, что seL4, со сквозной проверкой, теперь выпускается под лицензиями с открытым исходным кодом. Исходный код ядра и доказательства находятся под GPLv2, а большинство библиотек и инструментов находятся под лицензией BSD с двумя пунктами.
Исследователи заявляют, что стоимость формальной верификации программного обеспечения ниже, чем стоимость разработки традиционного «высоконадежного» программного обеспечения, несмотря на то, что дает гораздо более надежные результаты. В частности, стоимость одной строки кода во время разработки seL4 оценивалась примерно в 400 долларов США по сравнению с 1000 долларов США для традиционных систем с высоким уровнем надежности.
В рамках DARPA Программа высоконадежных кибервоенных систем (HACMS), разработанная NICTA совместно с партнерами проекта Rockwell Collins, Galois Inc, Миннесотским университетом и Boeing беспилотный летательный аппарат с высоким уровнем надежности, основанный на seL4, наряду с другими инструментами и программным обеспечением для обеспечения гарантий, с планируемой передачей технологий на опционально пилотируемый автономный вертолет Unmanned Little Bird, разрабатываемый Boeing. Окончательная демонстрация технологии HACMS состоялась в Стерлинге, штат Вирджиния, в апреле 2017 года. DARPA также профинансировало несколько контрактов Small Business Innovative Research (SBIR), связанных с seL4 в рамках программы, начатой доктором Джоном Лаунчбери. Малые предприятия, получившие SBIR, связанные с seL4, включали: DornerWorks, Techshot, Wearable Inc, Real Time Innovations и Critical Technologies.
Osker, ОС, написанная на Haskell, ориентированный на спецификацию L4; хотя в этом проекте основное внимание уделялось использованию языка функционального программирования для разработки ОС, а не исследований микроядра как таковых.
CodeZero - это микроядро L4, ориентированное на встроенные системы с акцентом на виртуализацию и реализацию сервисов родной ОС. Существует версия с лицензией GPL и версия, которая была перелицензирована разработчиками как закрытый исходный код и разветвлена в 2010 году.
Микроядро F9, реализация L4 с лицензией BSD, предназначена для Процессоры ARM Cortex-M для глубоко встраиваемых устройств с защитой памяти.
Архитектура виртуализации ОС NOVA - это исследовательский проект, в котором основное внимание уделяется созданию безопасной и эффективной среды виртуализации с небольшой надежной вычислительной базой. NOVA состоит из микрогипервизора, монитора виртуальной машины пользовательского уровня и непривилегированной компонентной многосерверной пользовательской среды, работающей поверх него, которая называется NUL. NOVA работает на многоядерных системах на базе x86.
WrmOS - это операционная система реального времени, основанная на микроядре L4. Имеет собственные реализации ядра, стандартных библиотек и сетевого стека, поддерживающие архитектуры SPARC, ARM, x86 и x86_64. Поверх WrmOS работает паравиртуализированное ядро Linux (w4linux).
