Розділ 14. seL4

Сідней, 2004 рік

Австралійський Сідней. Університет Нового Південного Уельсу. У дослідницькій лабораторії під назвою NICTA (National ICT Australia, тоді одна з найбільших комп’ютерних дослідницьких установ в Австралії) сидить молодий німецький професор. Його звати Гернот Гайзер. Йому близько сорока. Він народився у Західній Німеччині, вчився у Швейцарії, переїхав до Австралії у 1991-му. У Цюріху в ETH він зробив PhD під керівництвом Вольфганга Фіхтнера — з симуляції напівпровідникових приладів, не з операційних систем. До ОС він прийшов уже в Сіднеї. Гайзер заснував групу, яка зосереджується на мікроядрах сімейства L4.

L4 — це лінійка мікроядер, започаткована Йохеном Лідтке в Німеччині у 1990-х. Лідтке зробив одне просте, але критичне відкриття: попередні мікроядра (зокрема MACH) були повільні, бо їх погано спроектували. Якщо мікроядро написати правильно — воно може бути швидким, не повільніше за моноліт.

Лідтке помер у 2001 році. Його справу продовжили дослідники по всьому світу. Один з них — Гайзер у Сіднеї.

У 2004-му Гайзер сидить і думає над великою задачею. Усі сучасні операційні системи мають баги. Linux, Windows, BSD — тисячі CVE щороку. Усі ці системи у “важливих” застосуваннях — лікарнях, автомобілях, авіоніці, військовій техніці — постійно ризикують. Не тому що інженери погані, а тому що 30 мільйонів рядків коду неможливо перевірити повністю.

А якби можна було зробити маленьке ядро, у якого кожен рядок коду формально доведено правильним? Не “ймовірно правильним”, а математично доведено?

Це б змінило все.

Виклик

Гайзер скликає команду. Серед них — Кевін Елфінстон (інженер з Австралії, керівник проекту), Гарві Туч, Філіп Дерен, і молодий аспірант на ім’я Девід Мерфі. До них приєднується група верифікаторів під керівництвом Джерві Кляйна.

Початкова мета: формально верифікувати маленьке ядро на L4. На той час L4-ядра мали приблизно 10 тисяч рядків коду на C, що теоретично робило задачу можливою. На відміну від 10-30 мільйонів у Linux, де про повну верифікацію мріяти не варто.

Команда планує проект на 5 років. У 2004-му це здається оптимістичним.

Реальність — 8 років.

Технічна сторона

Як виглядає процес формальної верифікації ядра ОС?

Крок 1. Написати формальну специфікацію того, що ядро має робити. Не словами (“керує процесами”), а математичною мовою у Isabelle/HOL. Кожна функція ядра — теорема. Кожен системний виклик — формальне твердження про те, як міняється стан системи. Ця специфікація сама по собі — кілька тисяч рядків математичного коду.

Крок 2. Написати абстрактну реалізацію — версію ядра у вигляді функціонального псевдокоду, що демонструє правильну поведінку. Функціональна, без оптимізацій, без C-специфіки. Ще тисячі рядків.

Крок 3. Написати конкретну реалізацію — справжній C-код, який можна скомпілювати і запустити на залізі. Близько 10 тисяч рядків. Тут вже думаєш про швидкість, ефективність використання пам’яті, особливості конкретної архітектури.

Крок 4. Формально довести, що: - Конкретна реалізація (C-код) відповідає абстрактній. - Абстрактна реалізація відповідає специфікації. - За транзитивністю — C-код відповідає специфікації.

Для цього треба написати доведення на Isabelle/HOL. Це сотні тисяч рядків. На один рядок C — 20-25 рядків доведення.

Крок 5. Перевірити доведення на машині. Isabelle/HOL автоматично перевіряє, чи кожен крок коректний. Якщо так — ядро доведено правильним.

8 років у бункері

Проект тривав з 2004-го по 2009-й рік для першої повної верифікації функціональної коректності — це і є ті 5 років. Потім ще роки на розширення: integrity (2011), confidentiality / information-flow (2014), AArch64 порти. Разом — близько 8 років активної роботи до сучасного стану ядра.

Розмір остаточних артефактів: - Код ядра seL4: ~9000 рядків C + ~600 рядків асемблера для критичних місць. - Формальна специфікація: ~4900 рядків Isabelle. - Доведення коректності: ~200 000 рядків Isabelle.

Тобто на кожен рядок C-коду — приблизно 22 рядки доведення. Це найбільше формальне доведення, коли-небудь зроблене для системного коду.

Команда нараховувала близько 15-20 людей в активний період. Загальна вартість проекту, включно з фінансуванням NICTA і пізніше від різних агенцій (включно з DARPA), — оцінюється у $30-50 мільйонів доларів за все десятиліття.

Це здається багато. Але для порівняння — Linux-ядро коштує мільярди людино-годин, і досі має тисячі CVE.

2009: оголошення

У серпні 2009 року команда seL4 публікує статтю на 23-й Symposium on Operating Systems Principles (SOSP) з назвою:

“seL4: Formal Verification of an OS Kernel”

Стаття стає сенсацією у спільноті. Перше у світі ядро операційної системи формально верифіковане до останнього рядка.

Що саме доведено: - Functional correctness — ядро поводиться згідно зі специфікацією. - No buffer overflows — неможливо переповнити буфер. - No null pointer dereferences — неможливо звернутися до нульового покажчика. - No memory leaks — пам’ять не “тече”. - No undefined behavior — С-стандарт каже, що деякі речі (як цілочисельне переповнення) “невизначені”. У seL4 цього не може статися. - Termination — кожен системний виклик гарантовано завершується (не зависає назавжди). - Confidentiality and integrity — інформація між процесами не “тече”, якщо це заборонено політикою (це окреме доведення, додане у 2014-му).

Для більшості програмістів це абстрактні слова. Але практично це означає: seL4 не має жодного класичного бага системного програмування. Жодного. За визначенням.

Чому це важливо

Поки seL4 існував лише в академії, це було досягнення без особливих практичних наслідків. Цікаво, але хто справді користується академічними мікроядрами?

Усе змінилося приблизно з 2014-го, коли seL4 почав потрапляти у реальний світ.

DARPA HACMS Project (High-Assurance Cyber Military Systems). DARPA — агентство передових оборонних досліджень США — фінансувало проект, щоб довести, що seL4 може використовуватись у реальному військовому обладнанні. Найкрасивіший результат — у 2017 році HACMS-команда зробила безпілотний гелікоптер Boeing Little Bird, керований seL4. Тоді запросила команду red team — професійних хакерів — спробувати зламати гелікоптер. Хакери мали повний доступ до однієї з підсистем гелікоптера. Не змогли вирватись з неї. Не змогли захопити керування. Ізоляція seL4 математично гарантувала, що навіть скомпрометована підсистема не може отримати контроль над усім.

Qualcomm. З 2014-го мережеві модеми у багатьох смартфонах Qualcomm запускають seL4 як основу свого baseband firmware. Це означає, що сотні мільйонів смартфонів у світі вже мають seL4 всередині. Ти, можливо, тримаєш зараз у руці пристрій, у якому seL4 керує радіо.

Автомобілі. Кілька автовиробників (точні імена частково під NDA, але це включає декілька з топ-10 світових виробників) використовують seL4 у компонентах ADAS (advanced driver assistance systems). Тобто у системах, що приймають рішення про гальмування, керування тощо.

Авіоніка. Дослідницькі проекти НАТО і Boeing використовують seL4 в експериментальних системах безпілотників.

Автономні системи. DARPA, ARL (Army Research Lab), і кілька стартапів використовують seL4 як основу для досліджень автономних систем.

Військова криптографія. seL4 ліг в основу кількох систем шифрування для урядів західних країн.

Тобто seL4 уже не академічна іграшка — це продакшн-технологія, яка живе у дуже відповідальних системах.

Як seL4 виглядає всередині

Якщо ти заглянеш у вихідний код seL4 (він відкритий, GPL, на seL4.systems), тебе вразить, як мало там коду. Усе ядро — кілька десятків невеликих C-файлів. Найбільший — близько 1000 рядків. Більшість — менші.

Що там є: - Управління пам’яттю — ядро вирішує, як ділити фізичну пам’ять між процесами. - Перемикання потоків — вирішує, який потік наступний отримає процесор. - IPC (inter-process communication) — обмін повідомленнями між процесами. - Capability управління — про це окремий розділ.

Чого НЕМАЄ у ядрі: - Драйверів пристроїв (ні USB, ні мережі, ні SSD — нічого). - Файлових систем. - Мережевих стеків. - GUI. - Шифрування. - Командного інтерпретатора.

Усе це — процеси користувацького простору, які працюють поверх seL4. Вони не верифіковані (бо їх занадто багато і вони змінюються), але вони ізольовані через capability-механізм. Один драйвер не може зачепити інший. Один процес — інший. Зловмисник, який зламав один компонент, не може вирватись з нього до решти системи.

Це і є сенс мікроядра. Маленьке, верифіковане ядро як основа довіри. Усе інше — звичайні процеси, які можуть мати свої баги, але не можуть пошкодити систему в цілому.

Microkit: спроба зробити seL4 зручним

Найбільша критика seL4 завжди була: жахливо складно з ним працювати. Запустити “Hello World” на seL4 — це години роботи. Конфігурувати компоненти, capabilities, IPC канали — окрема наука.

Тому з 2020-х команда (тепер під назвою Trustworthy Systems, перенесена з NICTA до UNSW Sydney) розробляє seL4 Microkit (раніше називався sel4cp).

Microkit — це спрощений фреймворк зверху seL4. Він прибирає більшість бойлерплейту. Ти описуєш свою систему у YAML-файлі: які компоненти існують, які capabilities у кого, як вони спілкуються. Microkit генерує всю обв’язку.

Це робить seL4 доступним для звичайного embedded-розробника. Без 5-річної експертизи в L4-внутрішностях.

Microkit ще ранній (на 2024-й — близько версії 1.4), але це найперспективніший шлях, щоб seL4 вибрався з військово-промислової ніші у широкий світ.

Чи може seL4 замінити Linux

Чесна відповідь: ні, не для більшості задач. Linux і seL4 — у різних світах.

Linux: - Універсальний. Запускає все: від веб-сервера до Android до суперкомп’ютерів. - Має масові драйвери для будь-якого заліза. - Швидкий для general-purpose обчислень. - Має 30 мільйонів рядків коду, тисячі CVE на рік. - Якщо одна частина зламається — може потягти всю систему.

seL4: - Спеціалізований. Призначений для систем, де ціна помилки дуже висока. - Драйверів — мало. Кожен порт — кропітка ручна робота. - Швидкий, але потребує спеціальної інженерної праці. - Має 9000 рядків коду, жодного формального бага. - Якщо одна частина зламається — інші не постраждають, бо ізоляція математично гарантована.

Для веб-сервера або десктопа Linux залишиться. Для автомобіля, гелікоптера, медичного приладу, ядерного реактора, або шифрувального модуля у банку — seL4 (або інше верифіковане мікроядро).

Це різні інструменти для різних задач. Не “seL4 проти Linux” — а “seL4 ТАМ, де Linux небезпечний”.

Майбутнє seL4

Декілька цікавих напрямків зараз:

LionsOS — дослідницький проект Trustworthy Systems, який намагається зробити повноцінну операційну систему загального призначення на основі seL4 + Microkit. Це експеримент: можна показати, що верифіковане мікроядро може робити те саме, що Linux, не жертвуючи швидкістю?

Verus, Kani, Prusti — інструменти формальної верифікації для Rust. Якщо комбінувати seL4 (верифіковане ядро) з Rust-верифікованими компонентами зверху, можна побудувати систему, де кожен критичний шлях формально доведений.

AI-керована верифікація. Як ми говорили у попередньому розділі, AI може писати доведення в десятки разів швидше за людину. Це робить розширення seL4 (нові функції, нові архітектури, нові порти) дешевшим. Через 5 років, можливо, портування seL4 на нову архітектуру буде автоматичним.

Конкуренти. seL4 — не єдине верифіковане ядро. Є CertiKOS (Yale, конкурент), є Pip (французький проект), є Verisoft (старий німецький проект). Якщо їх кілька — конкуренція пришвидшує прогрес.

Що з цього винести

1. seL4 — перше у світі ядро операційної системи, формально верифіковане до останнього рядка.
2. Розробка зайняла близько 8 років, ~$30-50 мільйонів, команду 15-20 людей.
3. Технічно: ~9 тисяч рядків C-коду + ~200 тисяч рядків Isabelle/HOL-доведень.
4. Доведено відсутність цілих класів багів: переповнення, use-after-free, race conditions, undefined behavior.
5. Уже у продакшні: модеми Qualcomm (~сотні мільйонів смартфонів), автономні системи DARPA, частково в авто і авіації.
6. Не замінить Linux для широкого використання, але є необхідним там, де Linux не можна довірити.
7. Майбутнє — спрощення (Microkit), інтеграція з Rust, AI-автоматизація доведень, ширше прийняття.

У наступному розділі — те, що насправді робить seL4 особливим. Не сам факт верифікації — а архітектурна модель безпеки, на якій воно побудоване. Capability-based security. Концепція з 1960-х, яку індустрія забула на 40 років. Зараз, з seL4 і прибуттям AI-агентів, вона повертається — і саме вона стане ключем до безпечного майбутнього.

Це найзабутіший важливий принцип у всій комп’ютерній науці. Ходімо подивимось, що це таке.