Предлагаю вашему вниманию перевод seL4 Whitepaper, который является хорошим введением в одно из самых известных микроядер для ОС — seL4 (лицензия GPLv2).
Здесь не только специфика seL4 и микроядер вообще, но и много полезного материала в целом по ОС, ИТ-безопасности, формальной верификации и системам жёсткого реального времени. Перевод был несколько сокращён: удалены “технические блоки” (углубление в детали), кроме блока про “Linux capabilities”; а также части про фреймворки над микроядром (Microkit и другие) и тема про SeLinux.
В конце даны полезные ссылки. Некоторые особенности перевода:
threadвезде переводится буквально —нить. Это поможет избежать путаницы сflowиstream.capability— один из ключевых терминов. Оставлено без перевода, за исключением пары мест, где это слово употребляется в обычном смысле и переведено какспособность.-
secureвезде —безопасный. Происходит от латинскогоse cura— без тревоги, без заботы.safe— однокоренное с глаголомsave(спасать). От латинскогоsalvus— невредимый, сохранный, целый. В ОСsafeпо смыслу чаще всего означает “функционально безопасный”. Частоsafeпереводят какбезопасный(так же, как иsecure). Но чтобы не создавать путаницы сsecure, в данном текстеsafeвезде переводится по-другому (по-разному, в зависимости от контекста). IPC. Употребляется в двух смыслах:
4.1 Instruction per second, число целочисленных инструкций в секунду.
4.2 Основной смысл — Inter Process Communication, межпроцессное взаимодействие. На самом деле процессов в самом seL4 нет (эту абстракцию можно сделать на более высоком уровне, она есть во фреймворках). Правильнее название “ITC” (меж-нитевое взаимодействие). “IPC” сложился исторически, чему способствовал большой функционал этого взаимодействия (во многом близкий к настоящим IPC).
Gernot Heiser. The seL4 Microkernel — An Introduction. White paper. The seL4 Foundation, Revision 1.4 of 2025-01-08.
The seL4 Microkernel: An Introduction
Аннотация
В этом техническом документе представлено введение и обзор seL4. Мы объясняем, что такое seL4 (и чем он не является), и исследуем его определяющие особенности. Мы объясняем, что делает seL4 уникально подходящим ядром операционной системы для систем, критичных по безопасности (security- and safety-critical), а также для встраиваемых и кибер-физических систем в целом. В частности, мы объясняем аспекты обоснования доверия к seL4 (assurance story), его особенности, значимые для функциональной безопасности (safety-relevant features), а также его эталонную производительность. Мы также обсуждаем типичные сценарии использования, включая инкрементальный кибер-ретрофит (cyber retrofit) устаревших систем.
Понятия CCS
Разработка программного обеспечения и его инженерия → Операционные системы
Безопасность (Security) и приватность (Privacy) → Системная безопасность
Безопасность (Security) и приватность (Privacy) → Формальные методы и теория безопасности
Организация компьютерных систем → Системы реального времени → Операционные системы реального времени (Real-time operating systems)
Организация компьютерных систем → Системы реального времени → Надежные и отказоустойчивые системы и сети (Dependable and fault-tolerant systems and networks)
Глава 1. Что такое seL4?
seL4 — это микроядро (microkernel) операционной системы
Операционная система (ОС) — это низкоуровневое системное программное обеспечение, которое управляет ресурсами компьютерной системы и обеспечивает безопасность (enforces security). В отличие от прикладного программного обеспечения, ОС имеет исключительный доступ к более привилегированному режиму выполнения процессора (режим ядра), который дает ей прямой доступ к аппаратному обеспечению. Приложения всегда выполняются только в пользовательском режиме и могут получать доступ к аппаратному обеспечению только с разрешения ОС.
Микроядро ОС — это минимальное ядро ОС, сводящее к минимуму код, выполняющийся с более высокими привилегиями. seL4 является членом семейства микроядер L4, которое берет начало в середине 1990-х годов. (И нет, seL4 не имеет ничего общего с seLinux.)
seL4 также является гипервизором (hypervisor)
seL4 поддерживает виртуальные машины, которые могут запускать полноценную гостевую ОС, такую как Linux. При соблюдении контроля каналов связи, обеспечиваемого seL4, гости и их приложения могут взаимодействовать друг с другом, а также с нативными приложениями.
Узнайте больше о том, что значит, что seL4 является микроядром, и о его использовании в качестве гипервизора в Главе 2. А о реальных сценариях развертывания, включая подходы к модернизации безопасности устаревших систем, узнайте в Главе 7.
seL4 доказано корректным
seL4 доказано корректным (proved correct). seL4 поставляется с формальным, математическим, машинно-проверенным доказательством корректности реализации (proof of implementation correctness), что означает, что ядро в очень сильном смысле “не содержит ошибок” по отношению к его спецификации. Фактически, seL4 — это первое в мире ядро ОС с таким доказательством на уровне кода [Klein et al., 2009].
seL4 является доказуемо безопасным
seL4 является доказуемо безопасным. Помимо корректности реализации, seL4 поставляется с дополнительными доказательствами обеспечения безопасности (security enforcement) [Klein et al., 2014]. Они гласят, что в правильно сконфигурированной системе на основе seL4 ядро гарантирует классические свойства безопасности: конфиденциальность, целостность и доступность. Подробнее об этих доказательствах в Главе 3.
seL4 повышает безопасность с помощью детализированного контроля доступа через capabilities
Capabilities — это токены доступа, которые обеспечивают очень детализированный контроль над тем, кто (какая сущность) может получить доступ к тому или иному ресурсу в системе. Они поддерживают строгую безопасность в соответствии с принципом наименьших привилегий (principle of least privilege, также называемым принципом наименьших полномочий — POLA (Principle of Least Authority)). Это основной принцип проектирования высокозащищенных систем, и его невозможно достичь с помощью контроля доступа, реализованного в основных операционных системах, таких как Linux или Windows.
seL4 по-прежнему является единственной в мире ОС, которая одновременно основана на capabilities и формально верифицирована, и как таковая имеет обоснованное право называться самой безопасной ОС в мире. Подробнее о capabilities в Главе 4.
seL4 обеспечивает функциональную безопасность систем, критичных по времени
seL4 — это единственное в мире ядро ОС (по крайней мере, в открытой литературе), для которого был проведен полный и обоснованный анализ наихудшего времени выполнения (WCET — Worst-Case Execution Time) [Blackham et al., 2011, Sewell et al., 2017]. Это означает, что если ядро сконфигурировано соответствующим образом, все операции ядра ограничены по времени, и эта граница известна. Это обязательное условие для построения систем жёсткого реального времени, где неспособность отреагировать на событие в строго ограниченный период времени является катастрофической.
seL4 — самая передовая в мире ОС со смешанной критичностью
seL4 обеспечивает мощную поддержку систем со смешанной критичностью реального времени (mixed-criticality real-time systems, MCS), где своевременность критических действий должна быть обеспечена, даже если они сосуществуют с менее надежным кодом, выполняющимся на той же платформе. seL4 достигает этого с помощью гибкой модели, которая сохраняет хорошую утилизацию ресурсов, в отличие от более устоявшихся ОС MCS, которые используют строгое (и негибкое) временное и пространственное разделение [Lyons et al., 2018]. Подробнее о поддержке реального времени и MCS в seL4 в Главе 5.
seL4 — самое быстрое микроядро в мире
seL4 — самое быстрое микроядро в мире. Традиционно системы либо (более-менее) безопасны, либо быстры. seL4 уникален тем, что он и то, и другое. seL4 спроектирован для поддержки широкого круга реальных случаев использования, независимо от того, являются ли они критическими с точки зрения безопасности (security или safety) или нет, и отличная производительность является обязательным требованием. Подробнее о производительности seL4 в Главе 6.
seL4 произносится как “эс-и-эл-фо”
Произношение “сэл-фо” устарело.
Как читать этот документ
Этот документ предназначен для широкой аудитории. Однако для полноты картины мы добавим некоторые более глубокие технические детали.
Глава 2
Микроядро seL4
2.1 Монолитные ядра против микроядер
Чтобы понять разницу между основной ОС, такой как Linux, и микроядром, таким как seL4, давайте посмотрим на Рисунок 2.1.
Рисунок 2.1: Структура операционной системы: Монолитное ядро (слева) против микроядра (справа).
Конечно, программные ошибки (bugs) — в значительной степени факт жизни, и ОС не исключение. Например, ядро Linux содержит порядка 20 миллионов строк исходного кода (20 MSLOC); можно оценить, что оно содержит буквально десятки тысяч ошибок [Biggs et al., 2018]. Это, очевидно, огромная поверхность атаки (attack surface)! Эта идея описывается тем, что Linux имеет большую доверенную вычислительную базу (trusted computing base, TCB), которая определяется как подмножество всей системы, которое должно быть надежным для корректной работы, чтобы система была безопасной.
Идея, лежащая в основе конструкции микроядра, состоит в том, чтобы радикально сократить TCB и, следовательно, поверхность атаки. Как схематично показано справа на Рисунке 2.1, ядро, т.е. часть системы, выполняющаяся в привилегированном режиме, намного меньше. В правильно спроектированном микроядре, таком как seL4, оно составляет порядка десяти тысяч строк исходного кода (10 kSLOC). Это буквально на три порядка меньше, чем ядро Linux, и поверхность атаки соответственно уменьшается (возможно, даже больше, так как плотность ошибок, вероятно, растет более чем линейно с размером кода).
Очевидно, что невозможно обеспечить ту же функциональность с точки зрения сервисов ОС в такой маленькой кодовой базе. Фактически, микроядро предоставляет очень мало сервисов: это просто тонкая обертка вокруг аппаратного обеспечения, достаточная для безопасного мультиплексирования аппаратных ресурсов. Что микроядро в основном предоставляет, так это изоляцию, песочницы, в которых программы могут выполняться без помех со стороны других программ. И, что критически важно, оно предоставляет механизм защищенного вызова процедур (protected procedure call, PPC), который является формой межпроцессного взаимодействия (IPC). По историческим причинам термин IPC сохранился, но я рекомендую избегать его, так как он приводит к неверным представлениям, которые ведут к плохим архитектурным решениям.
Для более глубокого объяснения того, что такое IPC в seL4 и чем он не является, рекомендую прочитать мой блог “Как использовать IPC в seL4 (и как не надо)”.
Механизм PPC позволяет одной программе безопасно вызывать функцию в другой программе, при этом микроядро передает входные и выходные данные функции между программами и, что важно, обеспечивает контроль интерфейсов: “удаленная” (находящаяся в другой песочнице) функция может быть вызвана только через экспортированную точку входа и только явно авторизованными клиентами (которым была выдана соответствующая capability, см. Главу 4).
Система на основе микроядра использует этот подход для предоставления сервисов, которые монолитная ОС реализует в ядре. В мире микроядра эти сервисы являются просто программами, ничем не отличающимися от приложений, которые работают в своих собственных песочницах и предоставляют PPC-интерфейс для вызовов со стороны приложений. Если сервер будет скомпрометирован, эта компрометация будет ограничена сервером: его песочница защищает остальную часть системы. Это резко контрастирует с монолитным случаем, где компрометация сервиса ОС компрометирует всю систему.
Этот эффект может быть количественно оценен: Наше недавнее исследование показывает, что из известных компрометаций Linux, классифицированных как критические (т.е. наиболее серьезные), 29% были бы полностью устранены микроядерной архитектурой, а еще 55% были бы смягчены настолько, что больше не квалифицировались бы как критические [Biggs et al., 2018].
Рисунок 2.2: Древо семейства микроядер L4.
2.2 seL4 — это микроядро, а не ОС
seL4 — это микроядро, спроектированное для универсальности при минимизации TCB. Оно является членом семейства микроядер L4, которое берет начало в середине 90-х годов; Рисунок 2.2 показывает происхождение seL4. Он был разработан нашей группой в UNSW/NICTA, ныне известной как Trustworthy Systems (TS). В то время у нас было 15 лет опыта разработки высокопроизводительных микроядер и послужной список реальных развертываний: наше микроядро OKL4 поставлялось на миллиардах чипов модемов Qualcomm, а наше ядро L4-embedded середины 2000-х годов работает на защищенном анклаве (secure enclave) всех последних устройств iOS (iPhone и т.д.).
Будучи микроядром, seL4 не содержит обычных сервисов ОС; такие сервисы предоставляются программами, работающими в пользовательском режиме. Помимо огромных преимуществ, изложенных выше, у конструкции микроядра есть и недостатки: эти компоненты должны откуда-то взяться. Некоторые могут быть портированы из ОС с открытым исходным кодом, таких как FreeBSD или Linux, или они могут быть написаны с нуля. Но в любом случае, это значительная работа.
Для масштабирования нам нужна помощь сообщества, и Фонд seL4 (seL4 Foundation) является ключевым механизмом, позволяющим сообществу сотрудничать и разрабатывать или портировать такие сервисы для систем на основе seL4. Наиболее важными из них являются драйверы устройств, сетевые протокольные стеки и файловые системы. У нас есть некоторое количество таких, но требуется гораздо больше.
Даже по сравнению с другими микроядрами, API seL4 очень низкоуровневый, с минимальной абстракцией, необходимой для безопасного управления аппаратным обеспечением. Как таковое, построение систем на seL4 особенно сложно. На это можно смотреть как на то, что seL4 — это “язык ассемблера операционных систем”: очень примитивный.
Ни один здравомыслящий человек не стал бы писать сложную систему, скажем, базу данных или веб-сервер, на языке ассемблера; для этого мы используем языки программирования более высокого уровня. Они упрощают задачу, предоставляя конструкции и абстракции более высокого уровня, ценой потери некоторой мощности, предоставляемой аппаратным обеспечением. Почти во всех случаях это выигрышный компромисс. Аналогично, не следует пытаться строить сложную систему непосредственно на seL4, вместо этого следует использовать фреймворк более высокого уровня, который предоставляет более подходящие абстракции, ценой внесения некоторой политики (policy) и обуздания мощи seL4.
Существуют три основных компонентных фреймворка для seL4, все с открытым исходным кодом: Microkit, CAMkES и Genode.
2.3 seL4 также является гипервизором
seL4 — это микроядро, но также и гипервизор (hypervisor): возможно запускать виртуальные машины на seL4, а внутри виртуальной машины (VM) — основную ОС, такую как Linux.
Это позволяет альтернативный способ предоставления системных сервисов, используя Linux VM для их предоставления. Такая настройка показана на Рисунке 2.3, который показывает, как некоторые сервисы берутся из нескольких экземпляров Linux, работающих в качестве гостевых ОС в отдельных VM.
Рисунок 2.3: Использование виртуализации для интеграции нативных сервисов ОС с сервисами, предоставляемыми Linux.
В этом примере мы предоставляем два системных сервиса: сетевой и хранения данных. Сеть обеспечивается нативным протокольным стеком, работающим непосредственно на seL4, часто используются стеки lwIP или PicoTCP. Вместо портирования сетевого драйвера, мы берем его из Linux, запуская VM с урезанным гостевым Linux, который имеет не намного больше, чем драйвер NIC. Протокольный стек взаимодействует с Linux через канал, предоставляемый seL4, и приложение аналогичным образом получает сетевые сервисы, взаимодействуя с протокольным стеком. Обратите внимание, что в настройке, показанной на рисунке, приложение не имеет канала к VM драйвера NIC и, следовательно, не может взаимодействовать с ним напрямую, только через стек NW; это обеспечивается защитой на основе capabilities seL4 (см. Главу 4).
Аналогичная настройка показана для сервиса хранения данных; на этот раз файловая система является Linux, работающей в VM, в то время как драйвер хранения данных является нативным. Опять же, взаимодействие между компонентами ограничено явно предоставленными каналами. В частности, приложение не может взаимодействовать с драйвером хранения данных (кроме как через файловую систему), и две системы Linux не могут взаимодействовать друг с другом.
При использовании в качестве гипервизора seL4 работает в соответствующем режиме гипервизора (hypervisor mode) (EL2 на Arm, Root Ring-0 на x86, HS на RISC-V), который является уровнем привилегий более высоким, чем у гостевой операционной системы. Так же, как и при работе в качестве ядра ОС, он выполняет только минимум работы, который должен быть выполнен в привилегированном (гипервизорном) режиме, и оставляет все остальное пользовательскому режиму.
В частности, это означает, что seL4 выполняет переключение миров (world switches), то есть переключает состояние виртуальной машины, когда время выполнения VM истекло или VM должны быть переключены по какой-либо другой причине. Он также перехватывает события выхода из виртуальной машины (“VM exits” в терминологии Intel) и передает их обработчику пользовательского уровня, называемому монитором виртуальной машины (virtual machine monitor, VMM). Затем VMM отвечает за выполнение любых необходимых операций эмуляции.
Каждая VM имеет свою собственную копию VMM, изолированную от гостевой ОС, а также от других VM, как показано на Рисунке 2.4. Это означает, что VMM не может нарушить изоляцию и, следовательно, не является более доверенным, чем сама гостевая ОС. В частности, это означает, что нет необходимости верифицировать VMM, так как это не добавило бы реальной уверенности (assurance), пока гостевая ОС (обычно Linux) не верифицирована.
Рисунок 2.4: Поддержка виртуализации seL4 с VMM в пользовательском режиме (usermode VMMs).
2.4 seL4 — это не seLinux
…
Глава 3
История верификации seL4
В 2009 году seL4 стало первым в мире ядром ОС с машинно-проверенным доказательством функциональной корректности (machine-checked functional correctness proof) на уровне исходного кода. Это доказательство состояло из 200 000 строк скрипта доказательства на тот момент, что было одним из самых больших (мы думаем, что тогда оно было вторым по величине). Оно показало, что функционально корректное ядро ОС возможно, что до тех пор считалось неосуществимым.
С тех пор мы расширили объем верификации на свойства более высокого уровня; Рисунок 3.1 показывает цепочку доказательств, которые объясняются ниже. Важно, что мы поддерживали доказательства в ходе непрерывной эволюции ядра: коммиты в основную ветку (mainline) исходного кода ядра допускаются только в том случае, если они не нарушают доказательства, в противном случае доказательства также обновляются. Эта инженерия доказательств (proof engineering) также является новшеством. Наши доказательства seL4 составляют самую большую базу доказательств, которая активно сопровождается. Набор доказательств к настоящему времени вырос до более чем миллиона строк, в основном написанных вручную и затем проверенных машинно.
Рисунок 3.1: Цепочка доказательств seL4.
3.1 Корректность и обеспечение безопасности (security enforcement)
Функциональная корректность (Functional correctness)
Ядром верификации seL4 является доказательство функциональной корректности (functional correctness proof), которое гласит, что реализация на C свободна от дефектов реализации. Точнее, существует формальная спецификация (formal specification) функциональности ядра, выраженная на математическом языке, называемом логикой высшего порядка (higher-order logic, HOL). Она представлена блоком, помеченным как абстрактная модель на рисунке. Затем доказательство функциональной корректности утверждает, что реализация на C является уточнением (refinement) абстрактной модели, то есть возможные поведения C-кода являются подмножеством поведений, разрешенных абстрактной моделью.
Верификация трансляции (Translation validation)
Наличие безошибочной (bug-free) реализации на C — это замечательно, но все равно оставляет нас во власти C-компилятора. Эти компиляторы (мы используем GCC) сами по себе являются большими, сложными программами, в которых есть ошибки. Таким образом, у нас может быть безошибочное ядро, которое компилируется в ошибочный бинарный код.
В области, критичной к безопасности (security-critical), ошибки компилятора — не единственная проблема. Компилятор может быть откровенно вредоносным (malicious), содержать троян, который автоматически встраивает черный ход (back door) при компиляции ОС. Троян может быть расширен для автоматического добавления себя при компиляции компилятора, что делает его почти невозможным для обнаружения, даже если компилятор имеет открытый исходный код! Кен Томпсон объяснил эту атаку в своей Тьюринговской лекции [Thompson, 1984].
Чтобы защититься от дефектных или вредоносных компиляторов, мы дополнительно верифицируем исполняемый двоичный файл (executable binary), который создается компилятором и компоновщиком (linker). В частности, мы доказываем, что бинарный файл является корректной трансляцией (correct translation) (доказанно корректного) C-кода и, следовательно, что бинарный файл уточняет абстрактную спецификацию.
Рисунок 3.2: Цепочка доказательств верификации трансляции (Translation validation proof chain).
В отличие от верификации C-кода, это доказательство выполняется не вручную, а с помощью автоматического инструментария (automatic tool chain). Он состоит из нескольких этапов, как показано на Рисунке 3.2. Формальная модель системы команд处理器 (instruction set architecture, ISA) формализует бинарный код в доказывателе теорем; мы используем L3-формализацию ISA RISC-V, а также широко протестированную L3-формализацию ISA Arm от Fox и Myreen [2010].
Затем дизассемблер (disassembler), написанный на доказывателе теорем HOL4, преобразует это низкоуровневое представление в более высокоуровневое представление на графовом языке, который в основном представляет поток управления (control flow). Это преобразование является доказуемо корректным.
Формализованная программа на C преобразуется в тот же графовый язык с помощью доказуемо корректных преобразований в доказывателе теорем Isabelle/HOL. Затем у нас есть две программы в одном представлении, эквивалентность которых нам нужно показать. Это немного сложно, так как компиляторы применяют ряд эвристических преобразований для оптимизации кода. Мы применяем ряд таких преобразований с помощью правил перезаписи к графовому представлению программы на C (все еще в доказывателе теорем и, следовательно, доказуемо корректных).
В итоге мы имеем две программы, которые довольно похожи, но не одинаковы, и нам нужно доказать, что они имеют одинаковую семантику. Теоретически это эквивалентно проблеме остановки и, как таковое, неразрешимо. На практике то, что делает компилятор, достаточно детерминировано, чтобы сделать проблему разрешимой. Мы делаем это, передавая программы (небольшими частями) множеству SMT-решателей (SMT solvers). Если один из них может доказать, что все соответствующие части имеют одинаковую семантику, то мы знаем, что две программы эквивалентны.
Обратите также внимание, что программа на C, которая, как доказано, уточняет абстрактную спецификацию, и программа на C, которая, как доказано, эквивалентна бинарному файлу, являются одной и той же формализацией в Isabelle/HOL. Это означает, что наши допущения о семантике C выпадают из допущений, сделанных доказательствами. В совокупности доказательства не только показывают, что компилятор не внес ошибок, но и что его семантика для подмножества C совпадает с той, которую мы предполагали для верификации C кода.
Свойства безопасности
На Рисунке 3.1 также показаны доказательства связи между абстрактной спецификацией и высокоуровневыми свойствами безопасности: конфиденциальностью, целостностью и доступностью (их обычно называют свойствами CIA). Они утверждают, что абстрактная спецификация действительно полезна для безопасности: они доказывают, что в правильно сконфигурированной системе ядро будет обеспечивать эти свойства.
Конкретно, seL4 обеспечивает:
конфиденциальность: seL4 не позволит сущности читать (или иным образом извлекать) данные, если ей явно не были предоставлены права на чтение этих данных;
целостность: seL4 не позволит сущности изменять данные, если ей явно не были предоставлены права на запись в эти данные;
доступность: seL4 не позволит сущности препятствовать авторизованному использованию ресурсов другой сущностью.
Эти доказательства в настоящее время не охватывают свойства, связанные со временем. Наши доказательства конфиденциальности исключают скрытые каналы хранения (covert storage channels), но пока не исключают скрытые временные каналы (covert timing channels), которые используются в таких атаках, как Spectre. Предотвращение временных каналов — это то, над чем мы работаем [Heiser et al., 2019]. Аналогично, доказательства целостности и доступности в настоящее время не охватывают своевременность (timeliness), но наша новая модель MCS [Lyons et al., 2018] предназначена для покрытия этих аспектов (см. Раздел 5.2).
Допущения
Все рассуждения о корректности основаны на допущениях — будь то формальные рассуждения, как в случае seL4, или неформальные, когда кто-то размышляет о том, почему его программа может быть «корректной». Каждая программа выполняется в некотором контексте, и её корректное поведение неизбежно зависит от некоторых допущений об этом контексте.
Одно из преимуществ машинно-проверяемых формальных рассуждений заключается в том, что они заставляют людей делать эти допущения явными. Невозможно сделать недекларированное допущение: доказательства просто не сойдутся, если они зависят от допущений, которые чётко не сформулированы. В этом смысле формальные рассуждения защищают от забывания допущений или от неясности в их формулировке; само по себе это уже значительное преимущество формальности.
Верификация seL4 опирается на три допущения:
Аппаратное обеспечение работает так, как ожидается. Это должно быть очевидным. Ядро находится во власти лежащего в его основе оборудования, и если оборудование содержит ошибки (или, что хуже, трояны), то все ставки сняты — независимо от того, работает ли у вас верифицированный seL4 или любая неверифицированная ОС. Верификация оборудования выходит за рамки seL4 (и компетенции TS); другие люди работают над этим.
Спецификация соответствует ожиданиям. Это сложный пункт, потому что никогда нельзя быть уверенным, что формальная спецификация означает то, что, как мы думаем, она должна означать. Конечно, та же проблема существует и при отсутствии формальной спецификации: если спецификация неформальна или не существует, то, очевидно, невозможно точно рассуждать о корректном поведении.
Можно уменьшить этот риск, доказывая свойства спецификации, как мы сделали с нашими доказательствами безопасности, которые показывают, что seL4 способен обеспечивать определённые свойства безопасности. Тогда проблема смещается на спецификацию этих свойств. Они гораздо проще, чем спецификация ядра, что снижает риск недопонимания.
Но в конечном итоге всегда существует разрыв между миром математики и физическим миром, и никакое количество рассуждений (формальных или неформальных) не может полностью его устранить. Преимущество формальных рассуждений в том, что вы точно знаете, каков этот разрыв.
Доказыватель теорем корректен. Это звучит как серьёзная проблема, учитывая, что доказыватели теорем сами по себе являются большими и сложными программами. Однако в реальности это наименее тревожное из трёх допущений. Причина в том, что доказыватель теорем Isabelle/HOL имеет небольшое ядро (несколько десятков тысяч строк исходного кода), которое проверяет все доказательства на соответствие аксиомам логики. И это ядро проверило множество доказательств — малых и больших — из широкой области формальных рассуждений, поэтому вероятность того, что оно содержит критичную для корректности ошибку, крайне мала.
Статус и покрытие доказательств
seL4 был или верифицируется для нескольких архитектур: Arm, x86 и RISC-V. Некоторые из них более полны, чем другие, но недостающие части, как правило, находятся в разработке или ожидают финансирования. Пожалуйста, обратитесь к странице статуса проекта seL4 для получения подробной информации.
3.2 seL4 Microkit
…
Глава 4
О capabilities
Мы столкнулись с capabilities в Главе 1, отметив, что это токены доступа. Теперь мы рассмотрим эту концепцию более подробно.
4.1 Что такое capabilities?
Рисунок 4.1: capability — это ключ, предоставляющий определенные права на конкретный объект.
Как показано на Рисунке 4.1, capability — это ссылка на объект; в этом смысле она похожа на указатель (pointer) (и реализацию capabilities часто называют “толстыми (fat) указателями”). Это неизменяемые (immutable) указатели, в том смысле, что capability всегда будет ссылаться на тот же самый объект, поэтому каждая capability уникально определяет конкретный объект.
В дополнение к указателям, capability также кодирует права доступа (access rights); фактически, capability является инкапсуляцией ссылки на объект и прав, которые она предоставляет на этот объект. В системе, основанной на capabilities, такой как seL4, вызов capability — это единственный способ выполнения операции над объектом системы. Фактически, системный вызов в seL4 — это вызов capability с аргументами, указывающими, какая операция должна быть выполнена над объектом, на который ссылается вызванная capability. Затем ядро проверит, авторизует ли capability запрошенную операцию, и немедленно прервет операцию, если она не авторизована.
Например, операцией может быть вызов функции в компоненте. Ссылка на объект, встроенная в capability, тогда указывает на интерфейс этого объекта и предоставляет право вызывать эту функцию (т.е. конкретный метод объекта-компонента). capability может также предоставлять или не предоставлять одновременно право передавать другую capability в качестве аргумента функции (делегирование компоненту права использовать объект, на который ссылается аргумент-capability).
Именно эта детализированная, объектно-ориентированная природа (fine-grained, object-oriented nature) делает capabilities механизмом контроля доступа выбора для систем, ориентированных на безопасность (security-oriented). Права, предоставленные компоненту, могут быть ограничены абсолютным минимумом, необходимым ему для выполнения своей работы, как того требует принцип наименьших привилегий.
Обратите внимание, что это понятие объектных capabilities сильно отличается от (и гораздо мощнее) того, что Linux называет “capabilities”, которые на самом деле являются списками контроля доступа (access-control lists, ACLs) с гранулярностью системных вызовов. Linux capabilities, как и все схемы ACL, страдают от проблемы запутанного заместителя / запутанного посредника (confused deputy problem), которая лежит в основе многих нарушений безопасности (security breaches) и объясняется в следующем разделе. capabilities seL4 не имеют этой проблемы.
capabilities seL4 также не подвержены атаке Боберта [Boebert, 1984]; эта атака применима к capabilities, непосредственно реализованным в аппаратном обеспечении, в то время как capabilities seL4 реализованы и защищены ядром.
Существует десять типов объектов seL4, на все ссылаются capabilities:
Endpoints (конечные точки) используются для выполнения защищенных вызовов функций;
Reply Objects (объекты ответа) представляют путь возврата из вызова защищенной процедуры;
Address Spaces (адресные пространства) обеспечивают песочницы (sandboxes) вокруг компонентов (тонкие обертки, абстрагирующие аппаратные таблицы страниц);
Cnodes (C-узлы) хранят capabilities, представляющие права доступа компонента;
Thread Control Blocks (блоки управления нитями) представляют нити (threads) выполнения;
Scheduling Contexts (контексты планирования) представляют право доступа к определенной доле времени выполнения на ядре;
Notifications (уведомления) являются объектами синхронизации (похожи на семафоры);
Frames (фреймы) представляют физическую память, которая может быть отображена в адресные пространства;
Interrupt objects (объекты прерываний) предоставляют доступ к обработке прерываний; и
Untyped (нетипизированные) — неиспользуемая (свободная) физическая память, которая может быть преобразована (“перетипирована”) в любой другой тип.
4.2 Зачем нужны capabilities
Детализированный контроль доступа (Fine-grained access control)
Как отмечено выше, capabilities обеспечивают детализированный контроль доступа в соответствии с принципом безопасности “наименьших привилегий” (также называемым принципом наименьших полномочий, POLA (Principle of Least Authority)). Это контрастирует с более традиционной моделью контроля доступа на основе списков контроля доступа (ACL), которые используются в основных системах, таких как Linux или Windows, а также в коммерческих, якобы безопасных системах, таких как INTEGRITY или PikeOS.
Чтобы понять разницу, рассмотрим, как контроль доступа работает в Linux: Файл (и файловая модель применима к большинству других объектов Linux) имеет связанный с ним набор битов режима доступа (access-mode bits). Некоторые из этих битов определяют, какие операции его владелец (owner) может выполнять с файлом, другие представляют операции, разрешенные каждому члену “группы” файла, и последний набор дает права по умолчанию всем остальным. Это субъектно-ориентированная схема (subject-oriented scheme): это свойство субъекта (процесса, который пытается получить доступ) определяет допустимость доступа, и все субъекты с одинаковым значением этого свойства (ID пользователя или ID группы) имеют одинаковые права. Более того, эти субъекты имеют одинаковые права на все файлы с одинаковыми настройками свойств доступа.
Это очень грубый (coarse-grain) вид контроля доступа и является фундаментальным ограничением того, какие политики безопасности (security policies) могут быть обеспечены. Типичный сценарий: пользователь хочет запустить недоверенную программу (загруженную из интернета) для обработки определенного файла, но хочет предотвратить доступ программы к любым другим файлам, к которым у пользователя есть доступ. Это называется сценарием изоляции (confinement scenario), и в Linux нет чистого способа сделать это, поэтому люди придумали громоздкие обходные пути (я называю их “хакерскими ухищрениями”), такие как “chroot-изоляция (chroot jails)”, контейнеры и т.д.
С capabilities эта проблема решается просто, поскольку capabilities обеспечивают объектно-ориентированную форму контроля доступа. В частности, ядро разрешит операцию тогда и только тогда, когда субъект, запрашивающий операцию, предъявляет capability, которая уполномочивает его выполнить эту операцию. В сценарии изоляции недоверенное приложение может получить доступ только к тем файлам, на которые ему была выдана capability. Итак, Алиса вызывает программу, передавая ей capability на один файл, который программе разрешено читать, плюс capability на файл, в который программа может записать свой вывод, и программа не может получить доступ ни к чему другому — правильные наименьшие привилегии.
Интерпозиция (Interposition) и делегирование (Delegation)
capabilities имеют дополнительные полезные свойства. Одним из них является интерпозиция доступа, что является следствием того факта, что они являются непрозрачными ссылками на объекты (opaque object references). Если Алисе дана capability на объект, она не имеет возможности узнать, чем этот объект на самом деле является. Все, что она может делать, это вызывать методы объекта.
Например, разработчик системы может притвориться, что capability, данная Алисе, ссылается на файл, когда на самом деле она ссылается на канал связи с монитором безопасности (security monitor), который, в свою очередь, хранит фактическую capability на файл. Монитор может проверять запрошенные Алисой операции и, если они допустимы, выполнять их с файлом от ее имени, игнорируя недопустимые. Монитор, по сути, виртуализирует (virtualises) файл.
Интерпозиция имеет применение помимо обеспечения политик безопасности; этот подход может использоваться для фильтрации пакетов, отслеживания потоков информации (information-flow tracing) и многого другого. Отладчик может прозрачно интерпозировать и виртуализировать вызовы объектов. Это даже может быть использовано для ленивого создания объектов (create objects lazily): вместо ссылки на объект Алисе дается capability на конструктор, который затем заменяет capability после того, как объект будет создан.
Еще одним преимуществом capabilities является то, что они поддерживают неопасное (safe), а также эффективное делегирование привилегий (safe and efficient delegation of privilege). Если Алиса хочет дать Бобу доступ к одному из своих объектов, она может создать (“отчеканить” - mint в терминологии seL4) новую capability на объект и передать ее Бобу. Затем Боб может использовать эту capability для работы с объектом, не обращаясь обратно к Алисе. (Если, вместо этого, Алиса хочет оставаться в курсе, она может использовать виртуализацию, как объяснялось выше).
Новая capability может иметь уменьшенные права (diminished rights); Алиса может использовать это, чтобы дать Бобу только доступ на чтение к файлу. И Алиса может в любой момент отозвать (revoke) доступ Боба, уничтожив производную capability, которую она передала Бобу.
Делегирование является мощным и не может быть легко и неопасно (safe) выполнено в системах с ACL. Типичным случаем его использования является создание подсистем (sub-systems), которые автономно управляют ресурсами. Когда система запускается, начальный процесс обладает полномочиями на все ресурсы в системе (кроме небольшого и фиксированного объема, который ядро использует само). Этот начальный менеджер ресурсов (resource manager) может затем разделить (partition) систему, создавая новые процессы (вторичные менеджеры ресурсов) и передавая им полномочия на непересекающиеся подмножества системных ресурсов.
Затем подсистемы могут автономно (без обращения обратно к исходному менеджеру) управлять своим подмножеством ресурсов, не имея возможности вмешиваться друг в друга. Только если они хотят изменить первоначальное распределение ресурсов, им нужно привлечь исходного менеджера.
Окружающие полномочия (Ambient authority) и “запутанный заместитель”
Рисунок 4.2: Компилятор как “запутанный заместитель” (confused deputy).
ACL имеют неразрешимую проблему, обычно называемую проблемой запутанного заместителя / запутанного посредника. Давайте посмотрим на C-компилятор. Он принимает исходный C-файл и создает выходной файл объектного кода; имена файлов передаются в качестве аргументов. Чтобы запустить компилятор, пользователь, Алиса, должна иметь право на выполнение (execute permission) компилятора, как показано на Рисунке 4.2.
Предположим, что компилятор также создает запись в общесистемном файле журнала (system-wide log file) для целей аудита. Файл журнала недоступен обычным пользователям, поэтому компилятор должен выполняться с повышенными привилегиями, чтобы иметь возможность записывать в файл журнала (традиционно это делается путем превращения его в setuid-программу).
Если Алиса злоумышленница, она может обмануть компилятор, заставив его делать то, что он не должен делать. Например, Алиса может указать файл паролей (password file) в качестве выходного файла при вызове компилятора. Компилятор, если он не написан очень тщательно, чтобы избежать любого потенциального злоупотребления, просто откроет выходной файл (файл паролей) и перезапишет его скомпилированным объектным кодом. Алисе не нужно много навыков, чтобы написать программу, которая скомпилируется так, что вновь созданный файл паролей предоставит ей привилегии, которых у нее быть не должно.
Фундаментальная проблема здесь заключается в том, что системы на основе ACL используют окружающие полномочия (ambient authority) для определения прав доступа. Когда компилятор открывает свой выходной файл для записи, ОС определяет допустимость доступа, проверяя идентификатор субъекта (subject ID) компилятора, чтобы определить, имеет ли он доступ к объекту. Компилятор решает, является ли операция допустимой, что делает компилятор частью TCB системы, то есть ему необходимо полностью доверять, чтобы он поступал правильно при любых обстоятельствах.
Системы на основе ACL могут использовать ряд обходных путей для смягчения этой конкретной проблемы, например, гарантируя, что файл паролей и файл журнала находятся в разных доменах безопасности (security domains) (что не остановит Алису от порчи файла журнала, что само по себе полезно для злоумышленника, заметающего следы). Это затем запускает обычную гонку вооружений (arms race) между атаками и обходными путями, что всегда является проигрышной позицией для хороших парней.
Путаница возникает из-за окружающих полномочий: допустимость операции определяется состоянием безопасности агента (компилятора), который в данном случае является заместителем (deputy), действующим от имени исходного агента (Алисы). Для надлежащей безопасности доступ должен определяться состоянием безопасности Алисы. Это означает, что обозначение (denomination) (ссылка на файл) и полномочие (authority) (право выполнять операции с файлом) должны быть связаны — принцип, называемый “нет обозначения без полномочия (no designation without authority)”. Если это так, то компилятор вызывает обозначенный объект (выходной файл) с полномочием, которое приходит с обозначением (от Алисы), и Алиса больше не может запутать заместителя.
Это именно то, что обеспечивает система на основе capabilities. В такой системе Алисе нужно иметь три capabilities: capability на выполнение компилятора, capability на чтение входного файла и capability на запись в выходной файл. Она вызывает компилятор с capability на выполнение и передает две другие в качестве аргументов. Когда компилятор затем открывает выходной файл, он делает это с capability, предоставленной Алисой, и дальнейшая путаница невозможна. Компилятор использует отдельную capability, которой он владеет, для открытия файла журнала, сохраняя два файла хорошо разделенными. В частности, невозможно, чтобы Алиса обманом заставила компилятор записать в файл, к которому она сама не имеет доступа.
Проблема “запутанного заместителя” — это “киллер-приложение” для capabilities, поскольку эта проблема неразрешима с помощью ACL. Поэтому, в следующий раз, когда кто-то попытается продать вам “безопасную” ОС, спросите не только о наличии у них доказательства корректности ОС, но и о том, использует ли она контроль доступа на основе capabilities. Если ответ на любой из вопросов “нет”, значит, вам предлагают змеиное масло (snake oil).
Глава 5
Поддержка систем жёсткого реального времени
seL4 спроектирован как защищенная ОС реального времени (protected-mode real-time OS). Это означает, что, в отличие от классических RTOS, seL4 сочетает способность работы в реальном времени с защитой памяти для безопасности (security), а также как часть своей поддержки систем со смешанной критичностью.
5.1 Общая поддержка реального времени
seL4 имеет простую политику планирования на основе приоритетов (priority-based scheduling policy), которую легко понять и анализировать — основное требование для систем жёсткого реального времени. Ядро никогда само не изменяет приоритеты, поэтому пользователь контролирует их.
Другим требованием являются ограниченные латентности прерываний (bounded interrupt latencies). seL4, как и большинство членов семейства микроядер L4, выполняется с отключенными прерываниями (interrupts disabled) в режиме ядра. Это проектное решение значительно упрощает разработку и реализацию ядра, поскольку ядру (на одноядерном процессоре) не требуется контроль конкурентности (concurrency control). Формальная верификация seL4 в противном случае была бы невозможна, но этот дизайн также способствует отличной производительности в среднем.
Существует широко распространенное мнение, что ОС реального времени должна быть вытесняемой (preemptible), за исключением коротких критических секций, чтобы поддерживать низкую латентность прерываний. Хотя это верно для традиционных незащищенных RTOS, работающих на простых микроконтроллерах, это мнение ошибочно для системы с защищенным режимом, такой как seL4. Причина в том, что при работе на мощном микропроцессоре с включенной защитой памяти время входа в ядро, переключения контекста и выхода из ядра является значительным и ненамного меньше, чем системный вызов seL4. С точки зрения латентности прерываний, вытесняемый дизайн дал бы мало преимуществ, но стоимость в виде сложности была бы очень высокой, что делает вытесняемый дизайн неоправданным.
Это работает, пока все системные вызовы являются короткими. В seL4 они в целом короткие, но есть исключения. Особенно отзыв capability может быть длительной операцией. seL4 справляется с этой ситуацией, разбивая такие операции на короткие подоперации (sub-operations) и обеспечивая возможность прервать и перезапустить всю операцию после каждой подоперации, если есть ожидающее прерывание.
Этот подход называется инкрементальной согласованностью (incremental consistency). Каждая подоперация преобразует ядро из одного согласованного состояния в другое согласованное состояние. Операция структурирована таким образом, что после прерывания операция может быть перезапущена без повторения подопераций, которые были успешно завершены до прерывания. Ядро проверяет наличие ожидающих прерываний после каждой подоперации. Если они есть, оно прерывает текущую операцию, в этот момент прерывание вызывает повторный вход в ядро, которое обрабатывает прерывание. После завершения исходный системный вызов перезапускается, который затем продолжается с того места, где он был прерван, гарантируя прогресс.
Мы провели полный и обоснованный анализ наихудшего времени выполнения (WCET — Worst-Case Execution Time) seL4, который является единственным задокументированным для защищённой ОС [Blackham et al., 2011, Sewell et al., 2016]. Это означает, что мы получили доказуемые жесткие верхние границы для всех задержек системных вызовов и, как следствие, наихудших задержек прерываний.
Этот анализ WCET является обязательным условием для поддержки систем жёсткого реального времени, а также особенностью, которая выделяет seL4 среди конкурентов. В то время как полный и обоснованный анализ WCET был выполнен для незащищенных RTOS, отраслевой стандарт (industry-standard approach) для систем с защищенным режимом заключается в том, чтобы подвергнуть ядро высокой нагрузке, измерить задержки, взять наихудшее наблюденное значение и добавить запас надёжности (safety factor). Нет никакой гарантии, что достоверная граница (safe bound), полученная этим подходом, является безопасной, и он непригоден для систем, критичных по функциональной безопасности (safety-critical systems).
Мы провели анализ WCET seL4 для процессоров Arm v6. С тех пор он был прекращен, поскольку Arm перестала предоставлять необходимую информацию о наихудших задержках команд, а Intel никогда не предоставляла их для своей архитектуры. Однако с появлением процессоров RISC-V с открытым исходным кодом мы сможем повторить этот анализ.
5.2 Системы со смешанной критичностью
Что такое система со смешанной критичностью?
Критичность (Criticality) — это термин из области функциональной безопасности (safety domain), относящийся к серьезности отказа компонента. Например, авиационные стандарты классифицируют отказы от “без последствий” (для безопасности полета) до “катастрофические” (гибель людей). Чем более критичен компонент, тем более обширной (и дорогой) является требуемая уверенность (assurance), поэтому существует сильный стимул поддерживать критичность на низком уровне.
Система со смешанной критичностью (MCS) состоит из (взаимодействующих) компонентов с разной критичностью. Ее ключевое требование функциональной безопасности (core safety requirement) заключается в том, что отказ компонента не должен влиять на более критические компоненты, поэтому критические компоненты могут быть заверены независимо от менее критичных.
Тенденция к MCS является результатом желания консолидации (consolidate). Традиционно критические системы использовали бы выделенный микроконтроллер для каждой функции, т.е. изоляцию с помощью воздушного зазора (air-gapping). С ростом функциональности этот подход приводит к разрастанию процессоров (и их упаковки и проводки), что вызывает проблемы с пространством, весом и энергопотреблением (space, weight and power, SWaP), которые MCS призваны преодолеть.
Это похоже на концепцию безопасности (security) наличия доверенных и недоверенных компонентов в одной системе, и основным требованием к ОС в обоих случаях является сильная изоляция (strong isolation). Проблема в области функциональной безопасности (safety domain) заключается в том, что функциональная безопасность (safety) зависит не только от функциональной корректности, но и от своевременности (timeliness). Критические компоненты обычно имеют требования реального времени, что означает, что они должны отреагировать на событие к крайнему сроку (deadline).
Традиционный подход к MCS
Традиционные ОС MCS полностью изолируют компоненты временно и пространственно (temporally and spatially) — подход, называемый строгим временным и пространственным разделением (strict time and space partitioning, TSP), примером которого служит авиационный стандарт ARINC 653 [ARINC]. Это означает, что каждому компоненту статически назначается фиксированная область памяти, и разделы (partitions) выполняются в соответствии с предопределенным расписанием (pre-determined schedule) с фиксированными временными квантами.
Подход TSP гарантирует изоляцию, но имеет серьезные недостатки. Наиболее очевидный из них — плохая утилизация ресурсов (poor resource utilisation). Каждый компонент реального времени должен иметь возможность завершить свою работу в пределах своего временного кванта, поэтому временной квант должен быть не меньше, чем наихудшее время выполнения (WCET) компонента. WCET компонента может быть на порядки больше типичного времени выполнения, поскольку он должен учитывать исключительные обстоятельства.
Кроме того, определение достоверной границы (safe bound) для WCET, как правило, сложно. Для критических компонентов это должно быть сделано очень консервативно, чтобы убедить скептически настроенный орган сертификации (certification authority), что обычно приводит к большим переоценкам (over-estimates). Это означает, что обычно процессор сильно недоиспользуется (greatly under-utilised). Но из-за строгого разделения резервное время (slack time) не может быть использовано другими компонентами, поэтому плохая утилизация является неотъемлемой проблемой. По сути, сохраняя сильную изоляцию воздушного зазора (air-gapping), TSP также сохраняет его плохое использование ресурсов.
Другим большим недостатком TSP является то, что латентность прерываний (interrupt latencies) неотъемлемо высока. Возьмем пример Рисунка 5.1, который может представлять (сильно упрощенный) автономный транспорт (autonomous vehicle). Критическим компонентом является управляющий цикл (control loop), который выполняется один раз каждые 5 мс для обработки данных датчиков и отправки команд исполнительным устройствам (actuators). Его WCET и, следовательно, временной квант составляют 3 мс. Транспортное средство также взаимодействует с наземной станцией, которая может обновлять путевые точки (way points). Поскольку система работает с периодом 5 мс, это латентность, с которой могут обрабатываться сетевые прерывания, что сильно ограничивает пропускную способность сети и, в целом, реагирование на внешние события.
Рисунок 5.1: Упрощенный пример системы со смешанной критичностью.
Поддержка MCS в seL4
Основная проблема MCS заключается в том, что ОС должна обеспечивать сильную изоляцию ресурсов (strong resource isolation), но TSP является чрезмерно упрощенным (и, следовательно, негибким). С точки зрения пространственных ресурсов, seL4 уже имеет гибкую, мощную и доказуемо безопасную модель: объектные capabilities (см. Главу 4). Поддержка MCS расширяет это и на время (time). Доступ к процессору теперь также контролируется с помощью capabilities.
capabilities seL4 для процессорного времени называются capabilities контекста планирования (scheduling context). Компонент может получить процессорное время только в том случае, если он владеет такой capability, и количество процессорного времени, которое он может использовать, закодировано в capability (encoded in the capability). Это аналогично тому, как работают права доступа к пространственным объектам.
В традиционном seL4 (как и в большинстве предшествующих ядер L4) нить (thread) имела два основных параметра планирования: приоритет (priority) и квант времени (time slice), которые определяют доступ к процессору. Приоритет определяет, когда нить может выполняться: она может выполняться, если нет готовой к выполнению нити с более высоким приоритетом. Квант времени определяет, как долго ядро позволит нити выполняться перед вытеснением (если только она не будет вытеснена раньше появлением нити с более высоким приоритетом). Когда квант времени исчерпан, планировщик снова выберет готовую нить с наивысшим приоритетом (которая может быть только что вытесненной нитью) с политикой циклического планирования (round-robin) в пределах уровней приоритета.
MCS-версия seL4 заменяет квант времени на capability к объекту контекста планирования, который выполняет аналогичную функцию, но более точным способом, являющимся ключом к изоляции. Контекст планирования содержит два основных атрибута: (1) бюджет времени (time budget), который похож на старый квант времени и ограничивает время, в течение которого нить может выполняться до вытеснения. (2) период времени (time period), который определяет, как часто может использоваться бюджет: нить не получит больше времени, чем один бюджет за период, что предотвращает монополизацию CPU независимо от ее приоритета.
Контексты планирования поддерживают рассуждения о количестве времени, которое может потреблять нить, и, следовательно, о том, сколько времени осталось. В частности, они могут использоваться для предотвращения монополизации процессора высокоприоритетной нитью.
Применительно к приведенному выше примеру, это означает, что мы можем дать (менее критичному) драйверу устройства более высокий приоритет, чем (критическому) управляющему компоненту. Это позволяет драйверу вытеснять (preempt) управление, что приводит к высокой отзывчивости. Но ограничение бюджета (budget limit) остановит драйвер от монополизации CPU.
Например, мы даем контроллеру бюджет 3 мс (его WCET) и период 5 мс (соответствующий частоте его работы). И мы даем высокоприоритетному драйверу небольшой бюджет в 3 мкс с периодом 10 мкс, что означает, что он ни при каких обстоятельствах не может потреблять более 30% общего времени процессора, но при этом может выполняться достаточно часто, чтобы обеспечить хорошую отзывчивость. Важно, что мы можем гарантировать, что управление, которому требуется не более 60% доступного времени процессора, получит достаточно времени для соблюдения своего крайнего срока.
Гарантируя соблюдение критического крайнего срока независимо от поведения драйвера, мы изолируем (isolate) управление от недоверенного драйвера в соответствии с основным требованием MCS. В частности, драйвер не обязательно должен быть сертифицирован как функционально безопасный (safety-critical).
Модель временных capabilities seL4 решает ряд других задач MCS, которые выходят за рамки данного технического документа, и мы отсылаем заинтересованного читателя к рецензируемой публикации [Lyons et al., 2018]. Достаточно сказать, что seL4 обеспечивает самую передовую и гибкую поддержку MCS среди всех ОС, пригодных для критических систем.
Глава 6
Безопасность — не оправдание для плохой производительности
Производительность всегда была отличительной чертой микроядер L4, и seL4 не исключение. Мы создали seL4 для реального мира, и нашей целью было не потерять более 10% производительности IPC по сравнению с самыми быстрыми ядрами, которые у нас были ранее. Как оказалось, в итоге seL4 превзошел производительность тех ядер.
И он превосходит производительность любого другого микроядра. Это утверждение трудно доказать, поскольку конкуренты, как правило, держат свои данные о производительности в секрете (по очень веским причинам!).
Однако мы делаем это заявление о производительности публично при каждой возможности. Если кто-то не согласен, он должен представить доказательства. Мы также знаем из различных неофициальных каналов, что производительность IPC других систем, как правило, колеблется в диапазоне от 2 раз медленнее, чем у seL4, до гораздо медленнее, обычно примерно в десять раз.
Немногие независимые сравнения производительности, безусловно, подтверждают наше утверждение.
Mi et al. [2019] сравнивают производительность трех систем с открытым исходным кодом: seL4, Fiasco.OC и Zircon. В исследовании обнаружено, что затраты на IPC в seL4 примерно на 10-20% выше аппаратного предела входа в ядро, переключения адресного пространства и выхода из ядра. Fiasco.OC более чем в два раза медленнее seL4 (почти в три раза выше аппаратного предела), а Zircon почти в девять раз медленнее seL4.
Gu et al. [2016] сравнивают производительность CertiKOS с seL4, измеряя 3820 циклов для сквозной операции IPC в CertiKOS по сравнению с 1830 в seL4, что в два раза медленнее. Однако оказалось, что seL4bench, набор тестов производительности seL4, в то время содержал ошибку при работе с таймерами на x86, что приводило к завышенным задержкам. Правильная производительность seL4 составляет около 720 циклов, что более чем в пять раз быстрее CertiKOS. Это происходит в контексте того, что CertiKOS предлагает очень ограниченную функциональность и не имеет безопасности на основе capabilities.
Глава 7
Реальное развертывание и пошаговый кибер-ретрофит (Incremental Cyber Retrofit)
7.1 Общие соображения
Планируя защитить безопасность (security or safety) вашей системы с помощью seL4, первым шагом должно быть определение критических активов (critical assets). Цель состоит в том, чтобы минимизировать (minimise) эту часть вашей доверенной вычислительной базы (TCB) и сделать ее максимально модульной (modular), причем каждый модуль становится защищенным seL4 компонентом (Microkit).
Другой важной подготовкой является проверка доступности и статуса верификации (check availability and verification status) seL4 на вашей платформе. Очевидно, вы захотите верифицированное ядро (verified kernel), ведь именно это делает seL4 особенным. Однако даже на платформах, где ядро не верифицировано, тот факт, что оно использует большую часть кода с верифицированной платформы, даст вам гораздо более высокую уверенность (assurance), чем почти любая другая ОС. Но имейте в виду, что без верификации уверенность будет не такой высокой. Кроме того, вы не должны делать никаких заявлений о верификации (verification claim), если вы используете ядро, которое не верифицировано для вашей платформы, или которое каким-либо образом модифицировано.
Кроме того, вам нужно будет оценить, является ли доступная пользовательская инфраструктура достаточной для ваших целей. Если нет, то здесь сообщество может вам помочь. Существуют компании, специализирующиеся на поддержке внедрения seL4. Кроме того, если вы сами разрабатываете какие-либо полезные компоненты, вам следует серьезно рассмотреть возможность поделиться ими с сообществом под соответствующей лицензией open source. Те, кто вкладывается в общее дело, легче получают помощь от других.
7.2 Модернизация существующих систем
Большинство реальных развертываний seL4 не будут запускать все нативно (native). Как правило, существуют значительные устаревшие компоненты (legacy components), которые было бы дорого портировать, потому что они слишком велики или полагаются на слишком много системных сервисов, которые в настоящее время не поддерживаются seL4. Кроме того, часто от выполнения таких устаревших стеков (legacy stacks) нативно было бы мало выигрыша для безопасности (security или safety).
Использование способности виртуализации seL4 часто является прагматичным способом действий, примеры показаны в Разделе 2.3.
Рисунок 7.1: Пошаговый кибер-ретрофит (incremental cyber-retrofit) полетного компьютера Boeing ULB во время программы DARPA HACMS.
Типичный подход — это то, что мы называем пошаговым кибер-ретрофитом (incremental cyber-retrofit) — термин, введенный тогдашним директором программы DARPA Джоном Лончбери. Как показано на Рисунке 7.1, обычно это начинается с простого помещения всего существующего программного стека (whole existing software stack) в виртуальную машину, работающую на seL4. Очевидно, что этот шаг ничего не дает с точки зрения безопасности (security и safety), он только добавляет (очень маленькие) накладные расходы. Его значение заключается в том, что он обеспечивает базовый уровень (baseline), с которого можно начать модуляризацию (modularising).
Отличным примером является работа, проделанная нашими партнерами по проекту HACMS по кибер-модернизации автономного вертолета Boeing ULB. Оригинальная система работала на Linux, и на первом шаге команда поместила seL4 под нее.
На следующем шаге два компонента были извлечены в отдельные защищённые домены (PD — Protection Domain): особенно недоверенное программное обеспечение камеры было перемещено во вторую VM, также под управлением Linux, причем две Linux VM взаимодействовали через каналы. В то же время сетевой стек был извлечен из VM и преобразован в нативный компонент (native component), также взаимодействующий с основной VM.
Последний шаг вывел все остальные критические модули, а также (недоверенное) GPS-программное обеспечение, в отдельные PD, удалив исходную основную VM. Финальная система состояла из нескольких PD, запускающих нативный код seL4, и одной VM, запускающей только Linux и программу камеры.
Результат заключался в том, что в то время как начальную систему легко взломали (hacked) профессиональные тестировщики на проникновение (professional penetration testers), нанятые DARPA, конечное состояние было высокоустойчивым (highly resilient). Злоумышленники могли скомпрометировать систему Linux и делать с ней все, что хотели, но не могли выйти за ее пределы (break out) и скомпрометировать какую-либо другую часть системы. Команда была достаточно уверена, чтобы продемонстрировать атаку во время полета.
Глава 8
Заключения
seL4 было первым в мире ядром ОС с доказательством корректности реализации (функциональной корректности). Затем мы расширили верификацию вниз до двоичного кода и вверх до свойств обеспечения безопасности (security-enforcement properties), как объяснено в Главе 3.
Хотя сейчас существуют и другие верифицированные ядра ОС, seL4 по-прежнему определяет передовой уровень [Heiser, 2019]: у него самая всеобъемлющая история верификации, он по-прежнему является единственной верифицированной ОС, основанной на capabilities, и у него самая передовая поддержка реального времени. И наши текущие исследования направлены на то, чтобы гарантировать, что seL4 сохранит свои позиции явного лидера среди ОС, ориентированных на безопасность (security- and safety-oriented), например, путем внедрения систематического и принципиального предотвращения утечки информации через временные каналы [Ge et al., 2019].
Помимо этого технологического лидерства, seL4 в практических терминах все еще далеко опережает своих последователей: хотя мы с самого начала проектировали seL4 для реального мира, почти все остальные верифицированные ядра ОС являются академическими игрушками и далеки от того, чтобы быть пригодными для реального мира. На самом деле, нам известна только одна (совсем недавно) верифицированная система, которая практически развертываема (хотя и в гораздо более ограниченных сценариях).
Готовность seL4 к реальному миру является результатом двух аспектов, которые управляли дизайном: непоколебимая ориентация на производительность (uncompromising performance focus), как подчеркивается в Главе 6, и механизмы, спроектированные для поддержки самого широкого круга сценариев применения и политик безопасности (security policies), причем последнее стало возможным благодаря контролю доступа на основе capabilities (Глава 4).
Десять лет внедрения seL4 в реальный мир, включая пошаговый кибер-ретрофит устаревших систем (Глава 7), очевидно, помогли нам усовершенствовать и улучшить систему, но я с гордостью могу сказать, что для этого было достаточно мягких, инкрементальных изменений (mild, incremental changes). Единственным исключением является поддержка MCS (Раздел 5.2), которая потребовала довольно значительного изменения модели и ее реализации, но привилегированное управление временем (privileged management of time) было единственным, что мы сознательно оставили в корзине “сделать позже” во время первоначального проектирования [Heiser and Elphinstone, 2016].
Ссылки:
Большое подробное руководство — https://sel4.systems/Info/Docs/seL4-manual-latest.pdf
Сайт авторов seL4, есть информация о сопутствующих важных проектах — https://trustworthy.systems/projects/seL4/