seL4: доказанное ядро и недоказанные ожидания

Сильное доказательство начинается с точного утверждения

seL4 предоставляет машинно проверенные доказательства для определённых свойств и конфигураций. Functional correctness связывает реализацию с формальной спецификацией; для поддерживаемых вариантов существуют дополнительные результаты, включая binary correctness и свойства безопасности. Однако набор доказательств различается между архитектурами и конфигурациями. Это явно отражено в документации проекта. S10 S12

Из этого следует важное правило инженерного отчёта: указывать не только имя seL4, но и версию, архитектуру, выбранную конфигурацию и конкретное доказанное свойство. Утверждение «вся платформа математически безопасна» требует гораздо большего объёма обоснования, чем ссылка на доказательство микроядра.

Спецификация определяет, что считается правильным

Формальная корректность означает соответствие определённой модели, а не автоматическое совпадение со всеми ожиданиями пользователя. Если архитектура выдала компоненту право на ресурс, корректное ядро может именно это право и обеспечить. Ошибка распределения полномочий не обязана быть ошибкой реализации микроядра.

Для проектирования это полезное разделение ответственности. Команда ядра доказывает свойства механизма, архитектор системы определяет политику, а разработчики сервисов обеспечивают корректность протоколов. Сильное доказательство нижнего слоя уменьшает область неопределённости, но не отменяет остальные роли.

Capabilities: полномочие должно иметь объяснимое происхождение

В модели seL4 доступ к объектам задаётся capabilities. Проверять систему нужно как граф полномочий: какие компоненты получают доступ к памяти, каналам и устройствам, как права передаются и какие связи возможны после инициализации. Документация о proof stack отдельно обсуждает capDL и проверенную инициализацию для поддерживаемых конфигураций. S10

Предлагаемый аналитический пример — изолированный сервис ключей и недоверенный сетевой стек. Недостаточно нарисовать два процесса. Нужно установить, кто владеет общей памятью, кто может менять запрос во время обработки, кто создаёт новые каналы и кто имеет возможность восстановить отозванное полномочие. Именно эти связи определяют смысл изоляции.

Red: сильная гипотеза может быть ошибкой политики, а не поиском memory corruption в ядре. Например, проверяется, даёт ли разрешённый маршрут полномочий доступ к ресурсу, который по замыслу должен быть недоступен.

Blue: документация графа доступа должна позволять объяснить каждое полномочие. «Так было удобно драйверу» — причина реализации, но не доказательство соответствия политике.

Что находится в предпосылках

seL4 явно перечисляет предпосылки: корректность определённых низкоуровневых частей, boot code и аппаратуры. DMA рассматривается отдельно: устройства не должны произвольно разрушать модель памяти. Для confidentiality proof также отмечено, что охватываются каналы, представленные моделью; временные каналы не исчезают просто из-за наличия доказательства информационных потоков. S11

Это не слабость формального подхода. Наоборот, явное перечисление допущений позволяет направить аудит в оставшуюся область. Практически полезнее точно знать, что требует доверия, чем иметь неопределённое обещание «защищено аппаратно».

Для конкретной платы поэтому важны устройства с прямым доступом к памяти, конфигурация их изоляции, boot chain и firmware. Название IOMMU в спецификации изделия само по себе не доказывает корректное включение, карту разрешений и отсутствие обходных путей. Эти вопросы должны иметь отдельное проектное свидетельство.

Микроядро и драйверы: уменьшение доверенной базы требует архитектуры

Вынос драйвера из ядра уменьшает его привилегии только в пределах действительно выданных ресурсов. Если компоненту доступны широкие диапазоны памяти или DMA без подходящего ограничения, его фактические возможности могут быть гораздо больше, чем подсказывает слово userland.

FAQ seL4 прямо предупреждает, что использование микроядра не делает систему автоматически безопасной, и связывает практическую пользу доказательств с правильной конфигурацией. Драйверы DMA и их влияние на модель требуют отдельного внимания. S13

Для Blue удобна таблица «компонент → объект → полномочие → причина → способ отзыва». Она помогает обнаружить ситуации, когда изоляция есть на диаграмме процессов, но отсутствует на уровне прав. Для Red та же таблица задаёт допустимую область анализа: какие действия может совершить уже скомпрометированный компонент без нарушения доказанного ядра.

Confidentiality и timing нельзя смешивать

Если два домена не могут читать память друг друга, это сильное свойство. Но из него ещё не следует отсутствие информации в задержках, нагрузке на общие ресурсы или поведении внешнего протокола. Документация seL4 специально отделяет ограничения модели информационных потоков от других доказательств. S11

Исследовательский отчёт должен назвать канал и наблюдение. «Секрет не читается напрямую» и «секрет нельзя статистически вывести из времени ответа» требуют разных аргументов. Обратная ошибка также вредна: наличие неохваченного канала не отменяет доказанную корректность механизмов памяти и доступа.

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

seL4 рядом с Linux и Windows

При размещении сложной ОС в отдельном домене возникает вопрос о границе между гостем и сервисами платформы. Возможность rootkit внутри гостевого ядра не обязательно означает компрометацию микроядра. Но гостевой ввод, виртуальные устройства и совместно используемые сервисы остаются предметом анализа.

Сравним с Benthic: его механизмы меняют представление Windows о процессах, сети и файлах. Если внешний компонент получает данные только через уже скомпрометированный Windows-сервис, собственная изоляция этого компонента не делает полученные сведения истинными. Защита памяти наблюдателя и достоверность его источника — два разных требования. E15 E18

В проектируемой системе нужно поэтому фиксировать источник каждого утверждения: прямое наблюдение, сообщение гостя, измерение загрузки или вывод анализатора. Один красивый dashboard не должен стирать различие между этими типами свидетельств.

Практическая матрица assurance

Таблица предлагает состав доказательств для целой системы. Она не утверждает, что все её строки уже формально доказаны одним проектом seL4. Такое разделение позволяет использовать сильные результаты микроядра без приписывания им чужих гарантий.

Критерий качественного Red / Blue исследования

Хороший результат точно указывает, была ли нарушена предпосылка, ошибочна политика, уязвим сервис или затронута сама реализация. Эти случаи имеют разные последствия для доказательства и разные способы устранения. Главная ценность seL4 для исследователя — возможность формулировать эти различия гораздо строже, чем общую фразу «ядро считается доверенным».

 161  	if (Data->RequestorMode == KernelMode || Data->Iopb->MinorFunction != IRP_MN_QUERY_DIRECTORY || (Flags & FLTFL_POST_OPERATION_DRAINING))
 162  	{
 163  		return FLT_POSTOP_FINISHED_PROCESSING;
 164  	}