stringtranslate.com

Микроядро

Структура монолитных и микроядерных операционных систем соответственно

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

Если оборудование обеспечивает несколько колец или режимов ЦП , микроядро может быть единственным программным обеспечением, выполняющимся на самом привилегированном уровне, который обычно называется режимом супервизора или ядра . Традиционные функции операционной системы, такие как драйверы устройств , стеки протоколов и файловые системы , обычно удаляются из самого микроядра и вместо этого запускаются в пространстве пользователя . [1]

С точки зрения размера исходного кода микроядра часто меньше монолитных ядер . Например, микроядро MINIX 3 имеет всего около 12 000 строк кода. [2]

История

Микроядра берут свое начало от датского пионера компьютеров Пера Бринка Хансена и его работы в датской компьютерной компании Regnecentralen , где он руководил разработкой программного обеспечения для компьютера RC 4000. [3] В 1967 году Regnecentralen устанавливала прототип RC 4000 на заводе по производству удобрений Zakłady Azotowe Puławy в Польше. Компьютер использовал небольшую операционную систему реального времени, адаптированную под нужды завода. Бринк Хансен и его команда были обеспокоены отсутствием универсальности и возможности повторного использования системы RC 4000. Они опасались, что для каждой установки потребуется другая операционная система, поэтому они начали исследовать новые и более общие способы создания программного обеспечения для RC 4000. [4] В 1969 году их усилия привели к завершению разработки мультипрограммной системы RC 4000 . Его ядро ​​обеспечивало межпроцессное взаимодействие на основе передачи сообщений для 23 непривилегированных процессов, из которых 8 одновременно были защищены друг от друга. Он также реализовал планирование временных интервалов программ, выполняемых параллельно, инициирование и управление выполнением программ по запросу других работающих программ и инициирование передачи данных на периферийные устройства или с них. Помимо этих элементарных механизмов, он не имел встроенной стратегии выполнения программ и распределения ресурсов. Эта стратегия должна была быть реализована иерархией работающих программ, в которой родительские процессы имели полный контроль над дочерними процессами и действовали как их операционные системы. [5] [6]

После работы Брича Хансена микроядра разрабатывались с 1970-х годов. [7] Сам термин микроядро впервые появился не позднее 1981 года. [8] Микроядра были задуманы как ответ на изменения в компьютерном мире и на несколько проблем адаптации существующих « моноядер » к этим новым системам. Новые драйверы устройств, стеки протоколов, файловые системы и другие низкоуровневые системы разрабатывались постоянно. Этот код обычно находился в монолитном ядре и, таким образом, требовал значительной работы и тщательного управления кодом для работы. Микроядра разрабатывались с идеей, что все эти службы будут реализованы как программы пользовательского пространства, как и любые другие, что позволит работать с ними монолитно и запускать и останавливать их, как любую другую программу. Это не только позволит более легко работать с этими службами, но и разделит код ядра, чтобы позволить его тонкую настройку, не беспокоясь о непреднамеренных побочных эффектах. Более того, это позволит «создавать» совершенно новые операционные системы на общем ядре, помогая исследованию ОС.

Микроядра были очень горячей темой в 1980-х годах, когда были введены первые пригодные для использования локальные сети . [ требуется цитата ] . Ядро AmigaOS Exec было ранним примером, представленным в 1986 году и использовавшимся в ПК с относительным коммерческим успехом. Отсутствие защиты памяти, считавшееся в других отношениях недостатком, позволило этому ядру иметь очень высокую производительность передачи сообщений, поскольку ему не нужно было копировать данные при обмене сообщениями между программами пользовательского пространства. [9]

Те же механизмы, которые позволили ядру быть распределенным в пространстве пользователя, также позволили системе быть распределенной по сетевым соединениям. Первые микроядра, в частности Mach , созданный Ричардом Рашидом , показали себя с разочаровывающей производительностью, но присущие им преимущества оказались настолько велики, что это стало основным направлением исследований в конце 1990-х годов. [10] Однако в это время скорость компьютеров значительно возросла по отношению к сетевым системам, и недостатки в производительности стали подавлять преимущества в плане разработки. [ необходима цитата ]

Было предпринято много попыток адаптировать существующие системы для повышения производительности, но накладные расходы всегда были значительными, и большинство этих усилий требовали перемещения программ пользовательского пространства обратно в ядро. К 2000 году большинство крупномасштабных усилий по созданию ядра Mach было прекращено, хотя macOS от Apple , выпущенная в 2001 году, по-прежнему использует гибридное ядро ​​под названием XNU , которое объединяет сильно модифицированное (гибридное) ядро ​​Mach OSF/1 ( ядро OSFMK 7.3) с кодом из BSD UNIX, [11] [12] и это ядро ​​также используется в iOS , tvOS и watchOS . Windows NT , начиная с NT 3.1 и продолжая Windows 11 , использует гибридную конструкцию ядра. По состоянию на 2012 год основанный на Mach GNU Hurd также функционален и включен в тестовые версии Arch Linux и Debian .

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

Микроядра тесно связаны с экзоядрами . [13] Они также имеют много общего с гипервизорами , [14] но последние не претендуют на минимальность и специализируются на поддержке виртуальных машин ; микроядро L4 часто находит применение в качестве гипервизора.

Введение

Ранние ядра операционных систем были довольно маленькими, отчасти из-за ограниченности памяти компьютера. По мере роста возможностей компьютеров росло и количество устройств, которыми ядро ​​должно было управлять. На протяжении всей ранней истории Unix ядра, как правило, были небольшими, хотя они содержали различные драйверы устройств и реализации файловой системы . Когда адресное пространство увеличилось с 16 до 32 бит, дизайн ядра больше не ограничивался аппаратной архитектурой, и ядра начали увеличиваться.

Berkeley Software Distribution ( BSD) Unix положил начало эпохе более крупных ядер. В дополнение к работе базовой системы, состоящей из ЦП, дисков и принтеров, BSD добавила полную сетевую систему TCP/IP и ряд «виртуальных» устройств, которые позволяли существующим программам работать «невидимо» по сети. Этот рост продолжался много лет, в результате чего ядра содержали миллионы строк исходного кода . В результате этого роста ядра стали подвержены ошибкам и их становилось все труднее поддерживать.

Микроядро было призвано решить эту проблему роста ядер и возникающих в результате этого трудностей. Теоретически, конструкция микроядра позволяет упростить управление кодом за счет его разделения на службы пользовательского пространства . Это также позволяет повысить безопасность и стабильность за счет уменьшения объема кода, работающего в режиме ядра . Например, если сетевая служба выйдет из строя из-за переполнения буфера , будет повреждена только память сетевой службы, а остальная часть системы останется работоспособной.

Межпроцессное взаимодействие

Межпроцессное взаимодействие (IPC) — это любой механизм, который позволяет отдельным процессам взаимодействовать друг с другом, обычно путем отправки сообщений . Общая память , строго говоря, также является механизмом межпроцессного взаимодействия, но аббревиатура IPC обычно относится только к передаче сообщений, и именно последнее особенно актуально для микроядер. IPC позволяет строить операционную систему из ряда меньших программ, называемых серверами, которые используются другими программами в системе, вызываемыми через IPC. Большая часть или вся поддержка периферийного оборудования обрабатывается таким образом, с серверами для драйверов устройств, стеков сетевых протоколов , файловых систем, графики и т. д.

IPC может быть синхронным или асинхронным. Асинхронный IPC аналогичен сетевому общению: отправитель отправляет сообщение и продолжает выполнение. Получатель проверяет ( опрашивает ) доступность сообщения или оповещается о нем с помощью некоторого механизма уведомлений. Асинхронный IPC требует, чтобы ядро ​​поддерживало буферы и очереди для сообщений, а также справлялось с переполнением буфера; он также требует двойного копирования сообщений (от отправителя в ядро ​​и ядра в получателя). В синхронном IPC первая сторона (отправитель или получатель) блокирует, пока другая сторона не будет готова выполнить IPC. Он не требует буферизации или множественных копий, но неявное рандеву может усложнить программирование. Большинство программистов предпочитают асинхронную отправку и синхронный прием.

Микроядра первого поколения обычно поддерживали как синхронные, так и асинхронные IPC и страдали от низкой производительности IPC. Йохен Лидтке предположил, что конструкция и реализация механизмов IPC являются основной причиной этой низкой производительности. В своем микроядре L4 он впервые применил методы, которые снизили затраты IPC на порядок . [ 15] К ним относится системный вызов IPC, который поддерживает как операцию отправки, так и операцию получения, делая все IPC синхронными и передавая как можно больше данных в регистрах. Кроме того, Лидтке представил концепцию прямого переключения процесса , когда во время выполнения IPC выполняется (неполное) переключение контекста от отправителя напрямую к получателю. Если, как в L4, часть или все сообщение передается в регистрах, это передает часть сообщения, находящуюся в регистре, без какого-либо копирования вообще. Кроме того, избегаются накладные расходы на вызов планировщика; это особенно полезно в общем случае, когда IPC используется в режиме удаленного вызова процедур (RPC) клиентом, вызывающим сервер. Другая оптимизация, называемая ленивым планированием , позволяет избежать обхода очередей планирования во время IPC, оставляя потоки, которые блокируются во время IPC, в очереди готовности. После вызова планировщика он перемещает такие потоки в соответствующую очередь ожидания. Поскольку во многих случаях поток разблокируется перед следующим вызовом планировщика, этот подход экономит значительную часть работы. Аналогичные подходы с тех пор были приняты QNX и MINIX 3. [ требуется цитата ]

В серии экспериментов Чен и Бершад сравнили циклы памяти на инструкцию (MCPI) монолитного Ultrix с циклами микроядра Mach в сочетании с сервером 4.3BSD Unix, работающим в пользовательском пространстве . Их результаты объяснили более низкую производительность Mach более высоким MCPI и продемонстрировали, что IPC сам по себе не отвечает за большую часть системных накладных расходов, предполагая, что оптимизации, сосредоточенные исключительно на IPC, будут иметь ограниченный эффект. [16] Позднее Лидтке уточнил результаты Чена и Бершада, сделав наблюдение, что большая часть разницы между Ultrix и Mach MCPI была вызвана промахами кэша емкости , и заключил, что радикальное сокращение рабочего набора кэша микроядра решит эту проблему. [17]

В системе клиент-сервер большая часть коммуникации по сути синхронная, даже если используются асинхронные примитивы, так как типичная операция — это вызов клиентом сервера и затем ожидание ответа. Поскольку это также поддается более эффективной реализации, большинство микроядер обычно следовали примеру L4 и предоставляли только синхронный примитив IPC. Асинхронный IPC можно было реализовать поверх с помощью вспомогательных потоков. Однако опыт показал, что полезность синхронного IPC сомнительна: синхронный IPC навязывает многопоточную конструкцию в других простых системах, что приводит к сложностям синхронизации. Более того, вызов сервера, подобный RPC, последовательно выполняет клиент и сервер, чего следует избегать, если они работают на отдельных ядрах. Поэтому версии L4, развернутые в коммерческих продуктах, сочли необходимым добавить механизм асинхронного уведомления для лучшей поддержки асинхронной коммуникации. Этот сигнальный механизм не переносит данные и, следовательно, не требует буферизации ядром. Имея две формы IPC, они тем не менее нарушили принцип минимальности. Другие версии L4 полностью перешли на асинхронный IPC. [18]

Поскольку синхронный IPC блокирует первую сторону до тех пор, пока другая сторона не будет готова, неограниченное использование может легко привести к тупикам. Более того, клиент может легко организовать атаку типа «отказ в обслуживании» на сервер, отправив запрос и не пытаясь получить ответ. Поэтому синхронный IPC должен предоставлять средства для предотвращения неопределенной блокировки. Многие микроядра предоставляют тайм-ауты для вызовов IPC, которые ограничивают время блокировки. На практике выбор разумных значений тайм-аутов затруднен, и системы почти неизбежно используют бесконечные тайм-ауты для клиентов и нулевые тайм-ауты для серверов. Как следствие, тенденция заключается в том, чтобы не предоставлять произвольные тайм-ауты, а только флаг, который указывает, что IPC должен немедленно выйти из строя, если партнер не готов. Этот подход фактически предоставляет выбор из двух значений тайм-аута: ноль и бесконечность. Последние версии L4 и MINIX пошли по этому пути (старые версии L4 использовали тайм-ауты). QNX избегает этой проблемы, требуя от клиента указывать буфер ответа как часть вызова отправки сообщения. Когда сервер отвечает, ядро ​​копирует данные в буфер клиента, не дожидаясь, пока клиент получит ответ явно. [19]

Серверы

Серверы микроядра по сути являются демоническими программами, как и любые другие, за исключением того, что ядро ​​предоставляет некоторым из них привилегии для взаимодействия с частями физической памяти, которые в противном случае недоступны большинству программ. Это позволяет некоторым серверам, в частности драйверам устройств, напрямую взаимодействовать с оборудованием.

Базовый набор серверов для микроядра общего назначения включает серверы файловой системы, серверы драйверов устройств, сетевые серверы, серверы отображения и серверы устройств пользовательского интерфейса. Этот набор серверов (взятый из QNX ) обеспечивает примерно набор служб, предлагаемых монолитным ядром Unix . Необходимые серверы запускаются при запуске системы и предоставляют службы, такие как доступ к файлам, сети и устройствам, обычным прикладным программам. При работе таких серверов в среде пользовательского приложения разработка сервера похожа на обычную разработку приложений, а не на процесс сборки и загрузки, необходимый для разработки ядра.

Кроме того, многие «сбои» можно исправить, просто остановив и перезапустив сервер . Однако часть состояния системы теряется вместе с отказавшим сервером, поэтому этот подход требует, чтобы приложения справлялись со сбоем. Хорошим примером является сервер, отвечающий за соединения TCP/IP : если этот сервер перезапустить, приложения столкнутся с «потерянным» соединением, что является нормальным явлением в сетевой системе. Для других служб сбой менее ожидаем и может потребовать внесения изменений в код приложения. Для QNX возможность перезапуска предлагается как QNX High Availability Toolkit. [20]

Драйверы устройств

Драйверы устройств часто выполняют прямой доступ к памяти (DMA) и, следовательно, могут записывать данные в произвольные области физической памяти, включая различные структуры данных ядра. Поэтому таким драйверам нужно доверять. Распространено заблуждение, что это означает, что они должны быть частью ядра. Фактически, драйвер не является изначально более или менее надежным, будучи частью ядра.

Хотя запуск драйвера устройства в пользовательском пространстве не обязательно уменьшает ущерб, который может нанести некорректно работающий драйвер, на практике это полезно для стабильности системы при наличии ошибочных (а не вредоносных) драйверов: нарушения доступа к памяти самим кодом драйвера (в отличие от устройства) все еще могут быть обнаружены аппаратным обеспечением управления памятью. Кроме того, многие устройства не поддерживают DMA, их драйверы можно сделать ненадежными, запустив их в пользовательском пространстве. В последнее время все большее число компьютеров оснащены IOMMU , многие из которых могут использоваться для ограничения доступа устройства к физической памяти. [21] Это также позволяет драйверам пользовательского режима стать ненадежными.

Драйверы пользовательского режима на самом деле появились раньше микроядер. Michigan Terminal System (MTS) в 1967 году поддерживала драйверы пользовательского пространства (включая поддержку файловой системы), первая операционная система, разработанная с такой возможностью. [22] Исторически драйверы были меньшей проблемой, поскольку число устройств было небольшим и в любом случае надежным, поэтому наличие их в ядре упрощало дизайн и позволяло избегать потенциальных проблем с производительностью. Это привело к традиционному стилю драйвера в ядре в Unix, [23] Linux и Windows NT. С распространением различных видов периферийных устройств объем кода драйвера увеличился и в современных операционных системах по размеру кода превосходит ядро.

Необходимые компоненты и минимальность

Поскольку микроядро должно позволять создавать произвольные службы операционной системы поверх, оно должно предоставлять некоторую базовую функциональность. Как минимум, это включает:

Этот минимальный дизайн был впервые использован в Nucleus Бринча Хансена и гипервизоре VM IBM. С тех пор он был формализован в принципе минимальности Лидтке :

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

Все остальное можно сделать в программе пользовательского режима, хотя драйверы устройств, реализованные в виде пользовательских программ, на некоторых архитектурах процессоров могут требовать специальных привилегий для доступа к оборудованию ввода-вывода.

С принципом минимальности связано и не менее важно для проектирования микроядра разделение механизма и политики , это то, что позволяет строить произвольные системы поверх минимального ядра. Любая политика, встроенная в ядро, не может быть перезаписана на уровне пользователя и, следовательно, ограничивает общность микроядра. [13] Политика, реализованная на серверах пользовательского уровня, может быть изменена путем замены серверов (или предоставления приложению возможности выбирать между конкурирующими серверами, предлагающими аналогичные услуги).

Для эффективности большинство микроядер содержат планировщики и управляют таймерами, что нарушает принцип минимальности и принцип разделения политики и механизма.

Запуск ( booting ) системы на основе микроядра требует драйверов устройств , которые не являются частью ядра. Обычно это означает, что они упакованы с ядром в загрузочном образе, и ядро ​​поддерживает протокол начальной загрузки, который определяет, как драйверы находятся и запускаются; это традиционная процедура начальной загрузки микроядер L4 . Некоторые микроядра упрощают это, помещая некоторые ключевые драйверы внутрь ядра (в нарушение принципа минимальности), LynxOS и оригинальный Minix являются примерами. Некоторые даже включают файловую систему в ядро ​​для упрощения загрузки. Система на основе микроядра может загружаться через совместимый с мультизагрузкой загрузчик. Такие системы обычно загружают статически связанные серверы для выполнения начальной начальной загрузки или монтируют образ ОС для продолжения начальной загрузки.

Ключевым компонентом микроядра является хорошая система IPC и дизайн менеджера виртуальной памяти, который позволяет безопасно реализовать обработку сбоев страниц и подкачку на серверах пользовательского режима. Поскольку все службы выполняются программами пользовательского режима, эффективные средства связи между программами имеют существенное значение, гораздо большее, чем в монолитных ядрах. Дизайн системы IPC создает или разрушает микроядро. Чтобы быть эффективной, система IPC должна не только иметь низкие накладные расходы, но и хорошо взаимодействовать с планированием ЦП.

Производительность

На большинстве основных процессоров получение сервиса по своей сути более затратно в системе на основе микроядра, чем в монолитной системе. [13] В монолитной системе сервис получается одним системным вызовом, который требует двух переключений режима (изменения кольца процессора или режима ЦП ). В системе на основе микроядра сервис получается путем отправки сообщения IPC на сервер и получения результата в другом сообщении IPC с сервера. Для этого требуется переключение контекста , если драйверы реализованы как процессы, или вызов функции, если они реализованы как процедуры. Кроме того, передача фактических данных на сервер и обратно может повлечь за собой дополнительные накладные расходы на копирование, в то время как в монолитной системе ядро ​​может напрямую обращаться к данным в буферах клиента.

Таким образом, производительность является потенциальной проблемой в микроядерных системах. Опыт микроядер первого поколения, таких как Mach и ChorusOS, показал, что системы на их основе работали очень плохо. [16] Однако Йохен Лидтке показал, что проблемы производительности Mach были результатом плохого проектирования и реализации, в частности, чрезмерного объема кэша Mach . [17] Лидтке продемонстрировал с помощью своего собственного микроядра L4 , что посредством тщательного проектирования и реализации, и особенно следования принципу минимальности, затраты на IPC могут быть снижены более чем на порядок по сравнению с Mach. Производительность IPC L4 по-прежнему непревзойденна в ряде архитектур. [24] [25] [26]

Хотя эти результаты показывают, что низкая производительность систем, основанных на микроядрах первого поколения, не является репрезентативной для ядер второго поколения, таких как L4, это не является доказательством того, что системы на основе микроядра могут быть построены с хорошей производительностью. Было показано, что монолитный сервер Linux, перенесенный на L4, демонстрирует лишь несколько процентов накладных расходов по сравнению с собственным Linux. [27] Однако такая односерверная система демонстрирует лишь немногие, если вообще демонстрирует, преимущества, которые микроядра должны предоставлять, структурируя функциональность операционной системы на отдельных серверах.

Существует ряд коммерческих многосерверных систем, в частности, системы реального времени QNX и Integrity . Для этих многосерверных систем не было опубликовано всеобъемлющего сравнения производительности относительно монолитных систем. Более того, производительность, похоже, не является первостепенной проблемой для этих коммерческих систем, которые вместо этого подчеркивают надежное быстрое время отклика обработки прерываний (QNX) и простоту ради надежности. Попыткой создания высокопроизводительной многосерверной операционной системы был проект IBM Sawmill Linux. [28] Однако этот проект так и не был завершен.

В то же время было показано, что драйверы устройств пользовательского уровня могут приблизиться по производительности к драйверам ядра даже для таких высокопроизводительных устройств с большим количеством прерываний, как Gigabit Ethernet. [29] Это, по-видимому, подразумевает, что возможны высокопроизводительные многосерверные системы.

Безопасность

Преимущества безопасности микроядер часто обсуждались. [30] [31] В контексте безопасности принцип минимальности микроядер является, как утверждают некоторые, прямым следствием принципа наименьших привилегий , согласно которому весь код должен иметь только привилегии, необходимые для предоставления требуемой функциональности. Минимальность требует, чтобы доверенная вычислительная база системы (TCB) поддерживалась минимальной. Поскольку ядро ​​(код, который выполняется в привилегированном режиме оборудования) имеет неконтролируемый доступ к любым данным и, таким образом, может нарушить их целостность или конфиденциальность, ядро ​​всегда является частью TCB. Минимизация его является естественной в дизайне, ориентированном на безопасность.

Следовательно, микроядерные конструкции использовались для систем, разработанных для приложений с высокой степенью безопасности, включая KeyKOS , EROS и военные системы. Фактически, общие критерии (CC) на самом высоком уровне гарантии ( уровень гарантии оценки (EAL) 7) имеют явное требование, чтобы цель оценки была «простой», что является признанием практической невозможности установления истинной надежности для сложной системы. Опять же, термин «простой» вводит в заблуждение и плохо определен. По крайней мере, Критерии оценки доверенных компьютерных систем Министерства обороны ввели несколько более точную формулировку для классов B3/A1:

«TCB должен [реализовывать] полные, концептуально простые механизмы защиты с точно определенной семантикой. Значительная часть системной инженерии должна быть направлена ​​на минимизацию сложности TCB, а также на исключение из TCB тех модулей, которые не являются критически важными для защиты».

—  Критерии оценки доверенных компьютерных систем Министерства обороны

В 2018 году в докладе, представленном на Азиатско-Тихоокеанской системной конференции, утверждалось, что микроядра были явно безопаснее монолитных ядер, путем исследования всех опубликованных критических CVE для ядра Linux на тот момент. Исследование пришло к выводу, что 40% проблем вообще не могли возникнуть в формально проверенном микроядре, и только 4% проблем остались бы полностью неустраненными в такой системе. [32]

Третье поколение

Более поздняя работа над микроядрами была сосредоточена на формальных спецификациях API ядра и формальных доказательствах свойств безопасности API и корректности реализации. Первым примером этого является математическое доказательство механизмов ограничения в EROS, основанное на упрощенной модели API EROS. [33] Совсем недавно (в 2007 году) был выполнен полный набор машинно-проверенных доказательств свойств модели защиты seL4 , версии L4. [34]

Это привело к тому, что называется микроядрами третьего поколения , [35] характеризующимися API, ориентированным на безопасность, с доступом к ресурсам, контролируемым возможностями , виртуализацией как первоклассной заботой, новыми подходами к управлению ресурсами ядра, [36] и целью проектирования пригодности для формального анализа , помимо обычной цели высокой производительности. Примерами являются Coyotos, seL4 , Nova, [37] [38] Redox и Fiasco.OC. [37] [39]

В случае seL4 была достигнута полная формальная проверка реализации, [35] т. е. математическое доказательство того, что реализация ядра соответствует его формальной спецификации. Это дает гарантию того, что свойства, доказанные для API, действительно сохраняются для реального ядра, степень уверенности, которая выходит даже за рамки CC EAL7. За этим последовали доказательства свойств обеспечения безопасности API и доказательство, демонстрирующее, что исполняемый двоичный код является корректным переводом реализации C, выводя компилятор из TCB. Взятые вместе, эти доказательства устанавливают сквозное доказательство свойств безопасности ядра. [40]

Примеры

Вот некоторые примеры микроядер:

Наноядро

Термин «наноядро» или «пикоядро» исторически относился к:

Также существует по крайней мере один случай, когда термин «наноядро» используется не для обозначения небольшого ядра, а для такого, которое поддерживает наносекундное разрешение часов. [41]

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

Ссылки

  1. ^ Гердер, Йоррит Н. (23 февраля 2005 г.). «К настоящей микроядерной операционной системе» (PDF) . minix3.org . Получено 22 июня 2015 г. .
  2. ^ "read-more" . Получено 20 декабря 2016 .
  3. ^ "Пер Бринч Хансен". Компьютерное общество IEEE . Проверено 13 сентября 2016 г.
  4. ^ Brinch Hansen, Per (2004). История программиста: жизнь пионера в области компьютеров . Получено 13 сентября 2016 г.
  5. ^ Brinch Hansen, Per (апрель 1969). RC 4000 Software: Multiprogramming System (PDF) (Технический отчет). Regnecentralen . Получено 13 сентября 2016 г.
  6. ^ Brinch Hansen, Per (1970). «Ядро мультипрограммной операционной системы» (PDF) . Communications of the ACM . 13 (4): 238–250. CiteSeerX 10.1.1.105.4204 . doi :10.1145/362258.362278. S2CID  9414037. 
  7. ^ . Вульф, Уильям; Коэн, Эллис; Корвин, Уильям; Джонс, Анита; Левин, Рой; Пирсон, К.; Поллак, Фред (июнь 1974 г.). «HYDRA: Ядро многопроцессорной операционной системы». Communications of the ACM . 17 (6): 337–345. doi : 10.1145/355616.364017 . S2CID  8011765.
  8. ^ Рашид, Ричард; Робертсон, Джордж (декабрь 1981 г.). «Акцент: ядро ​​сетевой операционной системы, ориентированное на связь». Труды восьмого симпозиума ACM по принципам операционных систем SOSP '81 . Пасифик-Гроув, Калифорния, США. С. 64–75. doi :10.1145/800216.806593.
  9. ^ Сассенрат, Карл (1986). Справочное руководство по ядру ПЗУ Amiga . Exec.{{cite book}}: CS1 maint: отсутствует местоположение издателя ( ссылка )
  10. ^ "CMU CS Project Mach Home Page". www.cs.cmu.edu . Carnegie Mellon University . Получено 8 августа 2024 г. .
  11. ↑ Джим Маги. WWDC 2000, сессия 106 — Mac OS X: ядро. 14 минут. Архивировано из оригинала 11 декабря 2021 г.
  12. ^ "Перенос приложений UNIX/Linux на Mac OS X". Apple . Получено 26 апреля 2011 г.
  13. ^ abc Liedtke, Jochen (сентябрь 1996 г.). «К настоящим микроядрам». Сообщения ACM . 39 (9): 70–77. doi : 10.1145/234215.234473 . S2CID  2867357.
  14. ^ Heiser, Gernot ; Uhlig, Volkmar; LeVasseur, Joshua (январь 2006 г.). «Are Virtual-Machine Monitors Microkernels Done Right?». Обзор операционных систем ACM SIGOPS . 40 (1). ACM: 95–99. doi :10.1145/1113361.1113363. S2CID  7414062. Архивировано из оригинала 13 января 2014 г. . Получено 13 января 2014 г. .
  15. ^ Лидтке, Йохен (декабрь 1993 г.). Улучшение IPC с помощью проектирования ядра . 14-й симпозиум ACM по принципам операционных систем. Эшвилл, Северная Каролина, США. С. 175–88. CiteSeerX 10.1.1.40.1293 . 
  16. ^ ab Chen, J. Bradley; Bershad, Brian N. (декабрь 1993 г.). «Влияние структуры операционной системы на производительность системы памяти» (PDF) . Труды SOSP '93 четырнадцатого симпозиума ACM по принципам операционных систем . Эшвилл, Северная Каролина, США. стр. 120–133. doi :10.1145/168619.168629.
  17. ^ abc Liedtke, Jochen (декабрь 1995 г.). «О построении µ-ядра». SOSP '95 Труды пятнадцатого симпозиума ACM по принципам операционных систем . Copper Mountain Resort, CO, США. стр. 237–250. doi : 10.1145/224056.224075 .
  18. ^ Elphinstone, Kevin; Heiser, Gernot (ноябрь 2013 г.). «От L3 к seL4: чему мы научились за 20 лет существования микроядер L4?». Труды SOSP '13 двадцать четвертого симпозиума ACM по принципам операционных систем . Фармингтон, Пенсильвания, США. стр. 133–150. doi : 10.1145/2517349.2522720 .
  19. ^ "Synchronous Message Passing" . Получено 3 сентября 2024 г. .
  20. ^ "The QNX High Availability Toolkit" (PDF) . Архивировано из оригинала (PDF) 24 августа 2005 г.
  21. ^ Вонг, Уильям (27 апреля 2007 г.). «I/O, I/O, It's Off to Virtual Work We Go». Electronic Design . Получено 8 июня 2009 г.
  22. ^ Александр, Майкл Т. (1971). «Организация и особенности системы терминалов Мичигана». Труды 16–18 ноября 1971 г., Осенняя объединенная компьютерная конференция . Том 40. С. 589–591. doi : 10.1145/1478873.1478951 . S2CID  14614148.
  23. ↑ Lions, John (1 августа 1977 г.). Комментарий Lions к UNIX 6-го издания с исходным кодом . Одноранговые коммуникации. ISBN 978-1-57398-013-5.
  24. ^ Лидтке, Йохен ; Эльфинстон, Кевин; Шёнберг, Себастьян; Хартиг, Герман; Хайзер, Гернот ; Ислам, Наим; Джагер, Трент (май 1997 г.). Достигнутая производительность IPC (по-прежнему является основой расширяемости) . 6-й семинар по актуальным темам операционных систем. Кейп-Код, Массачусетс, США: IEEE. стр. 28–31. дои : 10.1109/HOTOS.1997.595177.
  25. ^ Грей, Чарльз; Чепмен, Мэтью; Чабб, Питер; Мосбергер-Танг, Дэвид; Хейзер, Гернот (апрель 2005 г.). Itanium — история разработчика систем. Ежегодная техническая конференция USENIX. Аннахайм, Калифорния, США. С. 264–278.
  26. ^ ван Шайк, Карл; Хейзер, Гернот (январь 2007 г.). Высокопроизводительные микроядра и виртуализация на ARM и сегментированных архитектурах. 1-й международный семинар по микроядрам для встраиваемых систем. Сидней, Австралия: NICTA. стр. 11–21. Архивировано из оригинала 26 апреля 2007 г. . Получено 1 апреля 2007 г. .
  27. ^ Härtig, Hermann; Hohmuth, Michael; Liedtke, Jochen ; Schönberg, Sebastian (октябрь 1997 г.). "Производительность систем на базе μ-ядра". Труды шестнадцатого симпозиума ACM по принципам операционных систем - SOSP '97 . Том 31. С. 66–77. doi :10.1145/268998.266660. ISBN 0-89791-916-5. S2CID  1706253.
  28. ^ Жеффло, Ален; Джагер, Трент; Пак, Юнхо; Лидтке, Йохен ; Эльфинстон, Кевин Дж.; Улиг, Фолькмар; Тидсвелл, Джонатон Э.; Деллер, Люк; и др. (2000). Многосерверный подход Sawmill . 9-й Европейский семинар ACM SIGOPS. Колдинг, Дания. стр. 109–114. CiteSeerX 10.1.1.25.8376 . 
  29. ^ Лесли, Бен; Чабб, Питер; Фицрой-Дейл, Николас; Гётц, Стефан; Грей, Чарльз; Макферсон, Люк; Поттс, Дэниел; Шен, Юетинг; Элфинстоун, Кевин; Хейзер, Гернот (сентябрь 2005 г.). «Драйверы устройств пользовательского уровня: достигнутая производительность». Журнал компьютерной науки и технологий . 20 (5): 654–664. doi :10.1007/s11390-005-0654-4. S2CID  1121537.
  30. ^ Таненбаум, Эндрю С. «Дебаты Таненбаума-Торвальдса, часть II».
  31. ^ Таненбаум, А., Гердер, Дж. и Бос, Х. (май 2006 г.).
  32. ^ Биггс, Саймон; Ли, Дэймон; Хейзер, Гернот (2018). «Присяжные: дизайн монолитной ОС несовершенен: дизайн на основе микроядра улучшает безопасность». Труды 9-го Азиатско-Тихоокеанского семинара по системам . Остров Чеджудо, Республика Корея: Ассоциация вычислительной техники. стр. 1–7. doi :10.1145/3265723.3265733.
  33. ^ Шапиро, Джонатан С.; Вебер, Сэмюэл. Проверка механизма ограничения EROS. Конференция IEEE по безопасности и конфиденциальности. Архивировано из оригинала 3 марта 2016 г.
  34. ^ Elkaduwe, Dhammika; Klein, Gerwin; Elphinstone, Kevin (2007). Verified Protection Model of the seL4 Microkernel. отправлено для публикации. Архивировано из оригинала 29 ноября 2011 г. Получено 10 октября 2007 г.
  35. ^ ab Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (октябрь 2009 г.). seL4: Формальная верификация ядра ОС (PDF) . 22-й симпозиум ACM по принципам операционных систем. Биг-Скай, Монтана, США.
  36. ^ Elkaduwe, Dhammika; Derrin, Philip; Elphinstone, Kevin (апрель 2008 г.). Проектирование ядра для изоляции и обеспечения физической памяти. 1-й семинар по изоляции и интеграции во встраиваемых системах. Глазго, Великобритания. doi :10.1145/1435458. Архивировано из оригинала 24 апреля 2010 г. . Получено 17 августа 2009 г. .
  37. ^ ab "TUD Home: Operating Systems: Research: Microkernel & Hypervisor". Факультет компьютерных наук . Технический университет Дрездена. 12 августа 2010 г. Архивировано из оригинала 6 апреля 2012 г. Получено 5 ноября 2011 г.
  38. ^ Steinberg, Udo; Kauer, Bernhard (апрель 2010 г.). NOVA: безопасная архитектура виртуализации на основе микрогипервизора . Eurosys 2010. Париж, Франция. стр. 209–222. doi :10.1145/1755913.1755935.
  39. ^ Лакожински, Адам; Варг, Александр (март 2009 г.). Укрощение подсистем – возможности как универсального контроля доступа к ресурсам в L4. IIES'09: Второй семинар по изоляции и интеграции во встроенных системах. Нюрнберг , Германия. CiteSeerX 10.1.1.629.9845 . 
  40. ^ Кляйн, Гервин; Андроник, Джун; Элфинстоун, Кевин; Мюррей, Тоби; Сьюэлл, Томас; Колански, Рафал; Хейзер, Гернот (февраль 2014 г.). «Комплексная формальная проверка микроядра ОС». ACM Transactions on Computer Systems . 32 (1): 2:1–2:70. doi :10.1145/2560537. S2CID  4474342.
  41. ^ Дэвид Л. Миллс и Пол-Хеннинг Камп (28 ноября 2000 г.). "The Nanokernel" (PDF) . Получено 28 августа 2017 г.

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