SeL4

seL4 (security enhanced L4) — це відкрите, високонадійне мікроядро на основі повноважень (capabilities). Воно успадковує характеристики продуктивності та архітектури від сімейства мікроядер L4, але реалізоване з використанням методів високого рівня надійності. seL4 використовує формальну математичну верифікацію для доведення конфіденційності, цілісності та доступності системи серед інших властивостей. Початкова стаття, що описує верифікацію seL4, була введена до Залу слави ACM SIGOPS у 2019 році.

Історія

seL4 було розроблено як мікроядро «з нуля» під впливом сімейства мікроядер L4, з явною метою забезпечення всеосяжної формальної верифікації при збереженні високої продуктивності. У 2009 році проєкт seL4 повідомив про машинно-перевірене доведення функціональної коректності, що охоплює шлях від формальної специфікації до реалізації на C.

У липні 2014 року початкові тексти ядра seL4 та артефакти верифікації було оприлюднено як відкритий код NICTA разом з промисловими партнерами.

7 квітня 2020 року було засновано seL4 Foundation для підтримки управління проєктом, розвитку екосистеми та довгострокового опікування; спочатку фундація функціонувала як проєкт Linux Foundation.

Архітектура

seL4 є надзвичайно мінімалістичним, навіть порівняно з попередніми ядрами L4: воно опікується лише керуванням пам'яттю/ізоляцією процесів та плануванням процесів — усе інше обробляється поза режимом ядра. Під час завантаження ядро seL4 статично виділяє достатньо пам'яті для самого себе, а потім передає всю решту пам'яті та повноважень початковому процесу простору користувача. seL4 ближче до CPU-драйвера, ніж до інших комерційних мікроядер, таких як Mach, QNX чи Minix. Основною мотивацією було надати свободу вибору політик та архітектури для розробників систем, але це також полегшує верифікацію та мінімізує промахи кешу.

Контроль доступу на основі повноважень

seL4 використовує модель на основі повноважень (capabilities) для контролю всього доступу до пам'яті та ресурсів ядра. Це дозволяє міркувати про ресурси та потоки інформації та керувати ними у програмний спосіб (на відміну від універсальних політик безпеки та архітектури «один розмір на всіх»). У цій моделі повноваження (capability) — це непідробний токен, який одночасно іменує об'єкт ядра і кодує операції, що можуть бути над ним виконані. Повноваження зберігаються в керованих ядром таблицях, що називаються вузлами повноважень (CNodes), які утворюють ієрархічний простір імен, аналогічний структурі каталогів файлової системи. CNode містить слоти повноважень і сам є об'єктом ядра, доступним лише через повноваження, що дозволяє явно делегувати, поділяти або відкликати повноваження над ресурсами.

Фізична пам'ять у seL4 спочатку представлена як повноваження нетипізованої пам'яті (untyped memory), які надають доступ до ділянок адресного простору комп'ютера, але не відповідають придатним для використання об'єктам. Нетипізована пам'ять перетворюється на типізовані об'єкти ядра за допомогою операції перетипізації (retype). Ядро записує відношення між нетипізованою пам'яттю та похідними об'єктами в дереві походження повноважень (capability derivation tree, CDT), що дозволяє системі забезпечувати безпечне повторне використання пам'яті: всі повноваження, похідні від ділянки нетипізованої пам'яті, мають бути видалені перш ніж цю ділянку можна буде перерозподілити. Цей механізм замінює неявні алокатори ядра явним, придатним для аудиту життєвим циклом пам'яті під керуванням застосунку.

Керування віртуальною пам'яттю також регулюється повноваженнями. Повноваження на кадр пам'яті надає право відображати цей кадр в адресний простір, з урахуванням прав доступу, закодованих у повноваженні. Самі адресні простори будуються з об'єктів таблиць сторінок, які також створюються з нетипізованої пам'яті та посилаються через повноваження. На додаток до пам'яті загального призначення, seL4 розрізняє нетипізовану пам'ять пристроїв (device untyped memory), на яку накладаються додаткові обмеження для запобігання небезпечній перетипізації або повторному використанню.

Міжпроцесна взаємодія (IPC)

IPC у seL4 не призначена як механізм передавання повідомлень загального призначення, а як спосіб реалізації міждоменного виклику функцій або сервісів через межі захисту. Розробники seL4 представляють її як Захищений виклик процедури (Protected Procedure Call, PPC), який переносить лише невеликі аргументи та значення повернення (подібно до виклику функції через межі доменів захисту), а не як буферизований транспорт для довільних даних. Розробники seL4 явно не рекомендують використовувати IPC для пересилання великих обсягів даних або для синхронізації, а замість цього застосовувати IPC переважно для виклику сервісів за схемою запит–відповідь та передавання повноважень.

Міжпроцесна взаємодія у seL4 побудована на керованих повноваженнями об'єктах ядра і спроєктована так, щоб мінімізувати стан ядра, водночас роблячи владу явною. Основним об'єктом IPC є кінцева точка (endpoint), яка представляє одночасно право на комунікацію та точку зустрічі для комунікації: потік може надсилати в кінцеву точку або приймати з неї лише за наявності відповідних повноважень.

IPC через кінцеві точки є синхронною та блокувальною (з можливістю надбудови інших схем комунікації). Операція надсилання очікує, доки приймач не буде готовий, а операція прийому очікує, доки не з'явиться відправник. На відміну від багатьох традиційних систем передавання повідомлень, кінцеві точки seL4 не надають керованих ядром черг повідомлень або поштових скриньок. Ядро підтримує лише черги потоків, що очікують, а дані повідомлення передаються безпосередньо між потоками за допомогою невеликого корисного навантаження () фіксованого розміру. Це уникає неявного виділення пам'яті ядра під час комунікації та узгоджується з моделлю явного керування ресурсами seL4.

Повідомлення можуть містити як дані, так і вибрані повноваження, що дозволяє IPC слугувати не лише механізмом комунікації, але й засобом явного делегування повноважень. Передавання повноваження під час IPC напряму передає право доступу до об'єкта ядра, тісно інтегруючи комунікацію та контроль доступу.

Розділення площини керування та площини даних

Хоча синхронна IPC є фундаментальним примітивом комунікації, що надається ядром, вона не призначена для передавання великих обсягів даних і її використання в системах на основі seL4 мінімізується на критичних для продуктивності шляхах. Системи зазвичай розділяють комунікацію на площину керування (control plane) та площину даних (data plane). IPC використовується переважно для операцій керування, таких як конфігурація, взаємодія за схемою запит–відповідь та передавання повноважень, тоді як масовий або високочастотний обмін даними реалізується в просторі користувача за допомогою спільної пам'яті у поєднанні з асинхронними сповіщеннями.

Області спільної пам'яті явно створюються з нетипізованої пам'яті та відображаються у декілька адресних просторів, а сповіщення використовуються для сигналізації про доступність даних або завершення роботи. Цей шаблон дозволяє реалізацію блокувально-вільних (lock-free) або очікувально-вільних (wait-free) структур даних, таких як кільцеві буфери, без залучення ядра до шляху даних. Тримаючи ядро поза масовим передаванням даних, системи seL4 зменшують накладні витрати на копіювання, уникають непотрібного блокування та зберігають простоту, необхідну для формальної верифікації. Цей архітектурний підхід просувають фреймворки вищого рівня в екосистемі seL4, зокрема CAmkES, seL4 Device Driver Framework (sDDF) та seL4 Microkit.

Порівняння з іншими моделями IPC

Черги повідомлень POSIX: черги повідомлень POSIX експонують іменовані черги, розташовані в ядрі, що підтримують асинхронне передавання повідомлень. Вони покладаються на неявне виділення пам'яті ядра та глобальний простір імен і відділяють передавання повідомлень від механізмів контролю доступу. На противагу цьому, seL4 не має ані глобального простору імен IPC, ані керованих ядром черг повідомлень; будь-яка комунікація вимагає володіння явним повноваженням на кінцеву точку, а політики буферизації за потреби реалізуються в просторі користувача. Порти Mach: порти Mach об'єднують іменування та повноваження для IPC і зазвичай асоціюються з керованими ядром чергами повідомлень та асинхронною буферизованою комунікацією. На противагу цьому, кінцеві точки seL4 уникають буферизації повідомлень у ядрі та натомість надають семантику синхронного рандеву, зменшуючи складність ядра та приховане використання ресурсів порівняно з більш гнучкими, але повільнішими механізмами IPC у Mach. IPC у L4: модель IPC у seL4 безпосередньо походить від попередніх мікроядер L4, які також робили акцент на синхронному, високопродуктивному передаванні повідомлень. seL4 зберігає семантику IPC у стилі рандеву, проте відокремлює передавання повідомлень від синхронізації. Це дозволяє оптимізувати перше для PPC (виклику серверів) та тісніше інтегрує їх із формальною системою повноважень та верифікованою архітектурою ядра, роблячи передавання повноважень явним і придатним для формального міркування.

Сповіщення та сигналізація подій

На додаток до кінцевих точок, seL4 надає об'єкти сповіщень (notifications): подібні до семафорів об'єкти для асинхронної сигналізації подій та легковагової синхронізації. Сповіщення зазвичай використовуються для доставки апаратних подій переривань драйверам пристроїв у просторі користувача або для сигналізації про зміни стану між компонентами, підтримуючи мікроядерну архітектуру, в якій обробка переривань і драйвери виконуються поза ядром.

Формальна верифікація

seL4 використовує специфікації, написані як математичні моделі в Isabelle/HOL для опису коректної роботи системних викликів. Ці специфікації потім зв'язуються з реалізацією на C для доведення її функціональної коректності: усі системні виклики виконують правильні операції та повертають правильні результати (відсутні логічні помилки, не аварійно завершується, не зависає, тощо). Це забезпечує дуже високий ступінь надійності того, що система повноважень ядра забезпечує ключові властивості тріади CIA інформаційної безпеки для процесів: конфіденційність інформації між процесами, цілісність стану ядра та потоку керування, а також доступність шляхом запобігання відмові в обслуговуванні для авторизованого використання ресурсів.

Маючи ~10 тис. рядків коду (LoC) та ~500 тис. рядків доведень (LoP), це один з найбільших верифікаційних продуктів, коли-небудь створених, початкову статтю про який було введено до Залу слави ACM SIGOPS у 2019 році. Накладні витрати верифікації у 50 рядків доведення на 1 рядок коду C різко збільшують вартість розробки та сповільнюють швидкість розробки, ускладнюючи внесення змін. Однак автори стверджують, що при $400 за рядок коду, вартість виявилася меншою за $1000 за рядок для подібних ядер високої надійності (але не верифікованих) і лише вдвічі дорожчою за вартість подібних ядер низької надійності.

Обмеження

Як і в інших формально верифікованих систем, гарантії seL4 є відносними щодо його специфікації та базових припущень. Хоча це означає, що верифікація не охоплює всі можливі несправності, вона все ж суттєво підвищує загальну надійність системи, усуваючи цілі класи дефектів реалізації та роблячи решту припущень явними (і, відповідно, тестованими).

seL4 — це лише мікроядро, на якому будуються повноцінні операційні системи. Однак тематичне дослідження критичних CVE ядра Linux показує, що ізоляція неверифікованих підсистем зменшила б серйозність кожного з обраних CVE, не пов'язаного з допусковим середовищем (pre-boot). Доведення не охоплюють усі аспекти функціонуючого комп'ютера під керуванням seL4 і не поширюються на всі підтримувані платформи та конфігурації. Наприклад, початкові доведення стосувалися лише кодової бази на C, але пізніша робота поширила доведення на скомпільовані бінарні файли (верифікація бінарних файлів не підтримується на всіх платформах).