Микроядро seL4, Ada/SPARK и 185 модулей: разбор проекта

Мне 38 лет, я сварщик из Санкт‑Петербурга. Профильного IT‑образования у меня нет. В июне 2026 года я купил ноутбук, поставил Linux и начал разбираться, как всё устроено изнутри. В октябре с этого же ноутбука я открыл страницу на смартфоне по обычному Wi‑Fi. Страницу отдавала операционная система, которую я собрал сам.

Проект называется Schild TCB, это исследовательский прототип доверенной вычислительной базы на Ada/SPARK поверх микроядра seL4, для x86_64, проверенный на ThinkPad T580. То, как изучал терминал, маски подсетей, рукопожатия TCP, HTTP и HTTPS, SSH — про это можно отдельную статью написать. Здесь — про результат. Сразу оговорю границы: часть доказана, часть только прогнана в QEMU, а кое‑что и на железе пощупал.

Два образа

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

Первый, schild_os.iso, собран с нуля целиком. Загрузчик, драйверы NVMe и e1000e, сетевой стек, планировщик — всё своё. Это как раз то, что обычно и называют операционной системой, и тут она вся моя.

Второй, sel4_primary.iso, стоит на микроядре seL4, которое писал не я. Моё там только то, что поверх: root‑задача на Ada и несколько изолированных демонов. Ядро чужое, но проверенное.

Зачем так. Bare‑metal образ отвечает на вопрос «работает ли», образ на seL4 — на вопрос «доказано ли». Микроядро я писать не стал: написать своё и формально доказать его я бы не смог, это годы работы. seL4 уже есть, он маленький и проверенный, а мой вклад это то, что поверх него. Мне кажется, это честнее, чем делать вид, что я написал всё сам.

Про доказательства

Ядро написано на Ada. Почему Ada — не скажу точно. Слышал о нём ещё в детстве, не помню от кого, в голове он у меня рядом с Фортраном, как что‑то древнее и серьёзное.

Проверяется всё в SPARK. SPARK — подмножество Ada, где к коду добавляются контракты. gnatprove доказывает, что код ведёт себя ровно так, как записано, для всех возможных входов, а не для набора тестов.

В root‑задаче есть MLS‑политика, Белла‑Лападула. Там всего три правила. Выглядят они так:

-- No Read Up: читать можно только данные не выше своего уровня function Can_Read (Subject : Clearance; Object : Clearance) return Boolean with Post => Can_Read'Result = (Subject >= Object); -- No Write Down: писать можно только данные не ниже своего уровня function Can_Write (Subject : Clearance; Object : Clearance) return Boolean with Post => Can_Write'Result = (Subject <= Object); -- Strict IPC: обмен сообщениями только между равными уровнями function Can_IPC (Sender : Clearance; Receiver : Clearance) return Boolean with Post => Can_IPC'Result = (Sender = Receiver);

Постусловие не комментарий и не тест. Это утверждение, которое gnatprove обязан доказать для любых Subject и Object. Не получается — он показывает контрпример, конкретные значения, при которых утверждение ложно.

Ещё пример, покороче. Аллокатор кадров памяти доказывает, что выделенный физический адрес выровнен по странице и лежит внутри ядра:

procedure Allocate_Physical_Frame (Passport : in out Schild_Frame_Deallocator.Frame_Deallocate_Passport; Success : out Boolean)
with Pre => not Passport.Is_Freed, Post => (if Success then (Passport.Physical_Address and 16#0FFF#) = 0 and Passport.Physical_Address < Schild_Mmu_Overseer.Kernel_Physical_Limit);

Всего в proof‑наборе 185 модулей ядра. Из них 108 доказаны полностью, not‑proved: 0. Остальные вне доказательства: 39 skipped — ассемблер, MMIO, AES‑NI, это физически нельзя загнать в SPARK, и 38 спецификаций без тела. Семь демонов root‑задачи доказываются отдельно, на том же уровне.

Зачем это всё, лучше всего видно на одной истории. Права на страницы MLS‑колец я задал как ReadOnly:= 1. А в раскладке CapRights у seL4 бит 0 это Write, бит 1 это Read. То есть моя «read‑only» страница на самом деле была «write‑only», а такие страницы x86 не поддерживает, и ядро маскировало их в «нет доступа вообще». Тесты это не ловили, потому что код просто не читал эти страницы. Поймал верификатор: когда я перевёл root‑задачу в SPARK‑режим и начал доказывать контракты, он показал, что контракт не сходится с реальностью. Пошёл разбираться, нашёл. Исправление в одну строку: ReadOnly:= 2.

Тесты не нашли, доказательство нашло. Для меня это главный результат всего проекта.

Про роль ИИ

Освоить Ada/SPARK и математическую верификацию за такой срок в одиночку невозможно: документация огромна. Я использовал ИИ‑агента как умный справочник и инструмент для код‑ревью. Я просил его объяснять спецификации seL4, переводить сухой математический язык контрактов SPARK на человеческий и помогать искать зацепки, когда gnatprove выдавал not‑proved. ИИ не писал систему за меня (он часто ошибался в нюансах микроядерной архитектуры), но он работал как идеальный штурман, подсвечивая, куда копать.

Про изоляцию

Отдельная тема — изоляция. Это то, ради чего вообще нужен микроядерный подход. Идея простая. Драйвер сети внутри ядра — ошибка в нём роняет всю систему. Вынес драйвер в отдельный процесс в Ring 3 — роняет только этот процесс. Ядро живое, остальные домены работают, упавший можно перезапустить.

У меня в Ring 3 вынесены сеть и хранилище, оба в домене NetServer: драйвер e1000e, стек TCP/IP, HTTP‑сервер, плюс драйвер NVMe и файловая система SchildFS. У каждого домена своё адресное пространство (CSpace и VSpace), общаться они могут только через IPC по явно переданным capabilities. Глобального адреса, через который один домен мог бы залезть в другой, просто нет.

Когда поток делает запрещённое (лезет в несмапленную память, берёт неверный capability), seL4 систему не роняет. Ловит и шлёт сообщение в fault‑эндпоинт домена. Root‑задача получает его и решает, что делать. Логика эскалации взята из ARINC 653 и зафиксирована в SPARK‑контрактах модели Health Monitor:

-- ARINC 653, эскалация по уровням -- процесс: счётчик <= Max_Restarts -> Restart (перезапуск домена) -- партиция: счётчик > Max_Restarts -> Stop (остановка домена) -- модуль: остановлены все домены -> Module_Idle Post => (if All_Stopped (State) then Action = Module_Idle elsif Count (State, Domain) > Max_Restarts then Action = Stop else Action = Restart);

Процесс упал — перезапускаем. Падает повторно — останавливаем весь домен. Остановлены все — переводим модуль в IDLE.

Есть и отдельный timeout‑эндпоинт. Если домен исчерпал бюджет процессорного времени, ядро шлёт сообщение не в fault‑эндпоинт, а в timeout‑эндпоинт, root‑задача различает их по бейджу. Сбой по памяти и сбой по времени это два разных события, и обрабатываются по‑разному.

Бюджеты задаются на уровне ядра, в микросекундах. NetServer 5000, MLS 2000, Config Daemon 1000, причём спорадический: бюджет 1000 микросекунд, период 100 миллисекунд. То есть Config Daemon просыпается редко, работает коротко, занять процессор надолго не может. Раньше детерминированный порядок партиций я держал сам, в коде. Теперь это гарантия ядра: даже если поток захочет занять всё время, ядро его остановит.

[S8.10] NetCNode@4105...
[S8.10] Mint net_ep...
[S8.10] Mint badged fault (root@4113)...
[MCS] SC@4111 + Reply@4112 -> TCB@4103 budget=5000 period=5000 badge=1...
[S8.10] Mint reply into Net CSpace slot 3...
[S8.10] SetSpace...
[S8.10] SetIPCBuffer...
[S8.10] WriteRegs...
[S8.10] Resume...
[S8.10] IPC Call (init)... [E1000E] MMIO base set (pre-mapped vaddr)
[E1000E] reset: read OK
[E1000E] reset: write OK

Похожее доказано и для запуска доменов: домен запускается ровно один раз, fault‑эндпоинты разных доменов не пересекаются, общий timeout‑эндпоинт привязан до первого запуска. Это проверялось только тестами, а теперь — доказано.

Где я застрял

Теперь честно про то, где застрял, потому что отчёт из одних побед никому не нужен.

Главное — IOMMU, устройство управления памятью для ввода‑вывода. Нужно оно для DMA‑изоляции. Когда устройство делает DMA, оно пишет напрямую в физическую память, минуя процессор и его MMU. Если сетевая карта скомпрометирована, она теоретически может писать в любую физическую память, включая память ядра. Изоляция на уровне VSpace её не остановит, потому что DMA идёт не через процессор. Останавливает это только IOMMU.

Я собрал seL4 с поддержкой IOMMU, ядро определило VT‑d, root‑задача прошла все проверки. Но под конфигурацией KernelVerificationBuild=OFF спорадический scheduling context зависает недетерминированно: от 33 до 67 процентов зависаний в зависимости от периода. Round‑robin стабилен. Триггер локализован в refill‑пути планировщика seL4. Это не мой код, это upstream‑ограничение на x86_64, и обходного пути у меня нет: не переписывать же ядро.

Дальше SMAP. Аппаратная защита, которая запрещает ядру обращаться к памяти пользователя без явного разрешения. В этой версии seL4 SMAP жёстко связан с CONFIG_PRINTING, опцией вывода логов ядра. Нужны логи — нет SMAP. Нужен SMAP — нет логов. Я выбрал логи, потому что без них отладка невозможна.

И ещё: формальное доказательство x86_64 MCS слабее, чем ARM MCS. Это не моя ошибка, это официальный статус upstream seL4. Всё, что я могу, это назвать это вслух, а не делать вид, что гарантии одинаковые.

Был ещё один баг, который нашёл я, а не наоборот. На ноутбуке с 32 гигабайтами root‑задача зависала на первом же retype, операции создания ядерных объектов. Не падала, просто висела. Причина оказалась в формуле, которая вычисляет максимальное число IOMMU‑слотов: на 32 гигабайтах получалось 262 142 слота, ядро резервировало под них почти шесть мегабайт в.boot.bss, граница ядра сдвигалась, и в boot‑reuse регион попадал четырёхмегабайтный блок, который при обнулении вешал контроллер. Патч в одну строку:

-#define MAX_NUM_DRHU    ((-PPTR_DRHU_START) >> PAGE_BITS)
+/* A real platform has <= 8 IOMMUs, so cap it there.
+   The upstream formula treats the whole 1 GiB kernel-device window
+   as DRHU slots, yielding 262142 and bloating .boot.bss to ~6 MiB. */
+#define MAX_NUM_DRHU    8

Реальный сервер имеет максимум восемь IOMMU. Ядро сжалось с восьми мегабайт до двух, зависание ушло. Баг не мой, но нашёл его я.

Про отладку

Отлаживать такое на ноутбуке без UART и COM‑порта это отдельное удовольствие. Второй машины для логов нет, поэтому схема была такая: загрузился с флешки, посмотрел на экран, потом грузился в Linux и описывал симптомы. Когда логи перестали писаться даже в файл, в ход пошли светодиоды клавиатуры, Num Lock и Caps Lock, как индикация этапов загрузки. Горит Caps — код дошёл до такого‑то места. Не горит — упал раньше.

Самый показательный баг был с пустой HTTP‑страницей. Соединение устанавливается, сервер отвечает, но страница приходит пустая, в логах чисто. Оказалось, перед отправкой пакета драйвер сбрасывал кэш, но clflush сбрасывает одну 64-байтовую линию, а я вызывал его только для первой линии буфера. Короткие пакеты уходили нормально, а HTTP‑ответ длиной около 500 байт занимал несколько линий, часть уходила устаревшими байтами, сетевая карта видела плохую контрольную сумму и молча дропала пакет. Исправление: сбрасывать кэш по всему буферу шагами по 64 байта.

Итог

Работают два образа: bare‑metal и seL4. Сеть и хранилище изолированы в Ring 3. TCP работает на железе, страница открывается со смартфона. 185 модулей ядра доказаны на SPARK Level 4, семь демонов root‑задачи тоже. Crash‑containment и временная изоляция проверены в QEMU.

Вот кусок лога с ноутбука в момент, когда телефон открыл страницу:

[IRQ] e1000e interrupt (badge=0x00000000000000E1)
[NET] RX IPv4
[TCP] SYN -> SYN-ACK
[TCP] ACK -> ESTABLISHED
[TCP] DATA -> ACK
[HTTP] req handled
[HTTP] reply sent
[TCP] FIN sent

На самой странице есть ссылка hardware_debug_log, она ведёт ровно на этот лог. Вот как страница выглядит на телефоне:

Не закрыто только одно: IOMMU, то есть DMA‑изоляции нет. Это упирается в upstream seL4 на x86_64, и тут я ничего сделать не могу. Либо ждать, пока там стабилизируется, либо переходить на ARM. Ещё усилить доказательство root‑задачи: она уже в SPARK, но не все пути доказаны.

Патчи к seL4 я приложу, если буду распространять ядро: это GPL‑код. Репозитория пока нет, проект локальный. Технических деталей тут много, но я их не все выложил: если будет интерес к MCS, ARINC 653 или патчам, их можно разобрать отдельно.

За всеми этими цифрами стоит простое: три месяца по вечерам и выходным, ноутбук, флешка и любопытство. Если кто‑то прочитал и решил, что тоже хочет разобраться в чём‑то сложном, значит, статья написана не зря.