seL4
| Тип | Мікроядро; ядро операційної системи на основі повноважень |
|---|---|
| Розробник | спільнота seL4; seL4 Foundation |
| Мова програмування | C (ядро); Isabelle/HOL (доведення) |
| Ліцензія | GPL-2.0 (ядро); переважно дозвільне ліцензування в екосистемі |
| Репозиторій | github.com/seL4/seL4 |
| Вебсайт | sel4.systems |
seL4 (security enhanced L4) — це відкрите, високонадійне мікроядро на основі повноважень (capabilities). Воно успадковує характеристики продуктивності та архітектури від сімейства мікроядер L4, але реалізоване з використанням методів високого рівня надійності.[1][2] seL4 використовує формальну математичну верифікацію для доведення конфіденційності, цілісності та доступності[3] системи серед інших властивостей. Початкова стаття, що описує верифікацію seL4, була введена до Залу слави ACM SIGOPS у 2019 році.[4]
seL4 було розроблено як мікроядро «з нуля» під впливом сімейства мікроядер L4, з явною метою забезпечення всеосяжної формальної верифікації[5] при збереженні високої продуктивності.[6] У 2009 році проєкт seL4 повідомив про машинно-перевірене доведення функціональної коректності, що охоплює шлях від формальної специфікації до реалізації на C.[7]
У липні 2014 року початкові тексти ядра seL4 та артефакти верифікації було оприлюднено як відкритий код NICTA разом з промисловими партнерами.[8][9]
7 квітня 2020 року було засновано seL4 Foundation для підтримки управління проєктом, розвитку екосистеми та довгострокового опікування; спочатку фундація функціонувала як проєкт Linux Foundation.[10][11]
seL4 є надзвичайно мінімалістичним, навіть порівняно з попередніми ядрами L4: воно опікується лише керуванням пам'яттю/ізоляцією процесів та плануванням процесів — усе інше обробляється поза режимом ядра. Під час завантаження ядро seL4 статично виділяє достатньо пам'яті для самого себе, а потім передає всю решту пам'яті та повноважень початковому процесу простору користувача. seL4 ближче до CPU-драйвера, ніж до інших комерційних мікроядер, таких як Mach, QNX чи Minix.[12] Основною мотивацією було надати свободу вибору політик та архітектури для розробників систем, але це також полегшує верифікацію та мінімізує промахи кешу.[13][14][1]
seL4 використовує модель на основі повноважень (capabilities) для контролю всього доступу до пам'яті та ресурсів ядра. Це дозволяє міркувати про ресурси та потоки інформації та керувати ними у програмний спосіб (на відміну від універсальних політик безпеки та архітектури «один розмір на всіх»). У цій моделі повноваження (capability) — це непідробний токен, який одночасно іменує об'єкт ядра і кодує операції, що можуть бути над ним виконані. Повноваження зберігаються в керованих ядром таблицях, що називаються вузлами повноважень (CNodes), які утворюють ієрархічний простір імен, аналогічний структурі каталогів файлової системи. CNode містить слоти повноважень і сам є об'єктом ядра, доступним лише через повноваження, що дозволяє явно делегувати, поділяти або відкликати повноваження над ресурсами.[15]
Фізична пам'ять у seL4 спочатку представлена як повноваження нетипізованої пам'яті (untyped memory), які надають доступ до ділянок адресного простору комп'ютера, але не відповідають придатним для використання об'єктам. Нетипізована пам'ять перетворюється на типізовані об'єкти ядра за допомогою операції перетипізації (retype). Ядро записує відношення між нетипізованою пам'яттю та похідними об'єктами в дереві походження повноважень (capability derivation tree, CDT), що дозволяє системі забезпечувати безпечне повторне використання пам'яті: всі повноваження, похідні від ділянки нетипізованої пам'яті, мають бути видалені перш ніж цю ділянку можна буде перерозподілити. Цей механізм замінює неявні алокатори ядра явним, придатним для аудиту життєвим циклом пам'яті під керуванням застосунку.[15]
Керування віртуальною пам'яттю також регулюється повноваженнями. Повноваження на кадр пам'яті надає право відображати цей кадр в адресний простір, з урахуванням прав доступу, закодованих у повноваженні. Самі адресні простори будуються з об'єктів таблиць сторінок, які також створюються з нетипізованої пам'яті та посилаються через повноваження. На додаток до пам'яті загального призначення, seL4 розрізняє нетипізовану пам'ять пристроїв (device untyped memory), на яку накладаються додаткові обмеження для запобігання небезпечній перетипізації або повторному використанню.[16]
IPC у seL4 не призначена як механізм передавання повідомлень загального призначення, а як спосіб реалізації міждоменного виклику функцій або сервісів через межі захисту. Розробники seL4 представляють її як Захищений виклик процедури (Protected Procedure Call, PPC), який переносить лише невеликі аргументи та значення повернення (подібно до виклику функції через межі доменів захисту), а не як буферизований транспорт для довільних даних. Розробники seL4 явно не рекомендують використовувати IPC для пересилання великих обсягів даних або для синхронізації, а замість цього застосовувати IPC переважно для виклику сервісів за схемою запит–відповідь та передавання повноважень.[17]
Міжпроцесна взаємодія у seL4 побудована на керованих повноваженнями об'єктах ядра і спроєктована так, щоб мінімізувати стан ядра, водночас роблячи владу явною. Основним об'єктом IPC є кінцева точка (endpoint), яка представляє одночасно право на комунікацію та точку зустрічі для комунікації: потік може надсилати в кінцеву точку або приймати з неї лише за наявності відповідних повноважень.[15]
IPC через кінцеві точки є синхронною та блокувальною (з можливістю надбудови інших схем комунікації). Операція надсилання очікує, доки приймач не буде готовий, а операція прийому очікує, доки не з'явиться відправник. На відміну від багатьох традиційних систем передавання повідомлень, кінцеві точки seL4 не надають керованих ядром черг повідомлень або поштових скриньок. Ядро підтримує лише черги потоків, що очікують, а дані повідомлення передаються безпосередньо між потоками за допомогою невеликого корисного навантаження (англ. payload) фіксованого розміру. Це уникає неявного виділення пам'яті ядра під час комунікації та узгоджується з моделлю явного керування ресурсами seL4.[15][7]
Повідомлення можуть містити як дані, так і вибрані повноваження, що дозволяє IPC слугувати не лише механізмом комунікації, але й засобом явного делегування повноважень. Передавання повноваження під час IPC напряму передає право доступу до об'єкта ядра, тісно інтегруючи комунікацію та контроль доступу.[15]
Хоча синхронна IPC є фундаментальним примітивом комунікації, що надається ядром, вона не призначена для передавання великих обсягів даних[17] і її використання в системах на основі seL4 мінімізується на критичних для продуктивності шляхах. Системи зазвичай розділяють комунікацію на площину керування (control plane) та площину даних (data plane).[джерело?] IPC використовується переважно для операцій керування, таких як конфігурація, взаємодія за схемою запит–відповідь та передавання повноважень, тоді як масовий або високочастотний обмін даними реалізується в просторі користувача за допомогою спільної пам'яті у поєднанні з асинхронними сповіщеннями.[15][18]
Області спільної пам'яті явно створюються з нетипізованої пам'яті та відображаються у декілька адресних просторів, а сповіщення використовуються для сигналізації про доступність даних або завершення роботи. Цей шаблон дозволяє реалізацію блокувально-вільних (lock-free) або очікувально-вільних (wait-free) структур даних, таких як кільцеві буфери, без залучення ядра до шляху даних. Тримаючи ядро поза масовим передаванням даних, системи seL4 зменшують накладні витрати на копіювання, уникають непотрібного блокування та зберігають простоту, необхідну для формальної верифікації. Цей архітектурний підхід просувають фреймворки вищого рівня в екосистемі seL4, зокрема CAmkES, seL4 Device Driver Framework (sDDF) та seL4 Microkit.[19][20]
- Черги повідомлень POSIX: черги повідомлень POSIX експонують іменовані черги, розташовані в ядрі, що підтримують асинхронне передавання повідомлень. Вони покладаються на неявне виділення пам'яті ядра та глобальний простір імен і відділяють передавання повідомлень від механізмів контролю доступу. На противагу цьому, seL4 не має ані глобального простору імен IPC, ані керованих ядром черг повідомлень; будь-яка комунікація вимагає володіння явним повноваженням на кінцеву точку, а політики буферизації за потреби реалізуються в просторі користувача.[21][22]
- Порти Mach: порти Mach об'єднують іменування та повноваження для IPC і зазвичай асоціюються з керованими ядром чергами повідомлень та асинхронною буферизованою комунікацією. На противагу цьому, кінцеві точки seL4 уникають буферизації повідомлень у ядрі та натомість надають семантику синхронного рандеву, зменшуючи складність ядра та приховане використання ресурсів порівняно з більш гнучкими, але повільнішими механізмами IPC у Mach.[23]
- IPC у L4: модель IPC у seL4 безпосередньо походить від попередніх мікроядер L4, які також робили акцент на синхронному, високопродуктивному передаванні повідомлень. seL4 зберігає семантику IPC у стилі рандеву, проте відокремлює передавання повідомлень від синхронізації. Це дозволяє оптимізувати перше для PPC (виклику серверів) та тісніше інтегрує їх із формальною системою повноважень та верифікованою архітектурою ядра, роблячи передавання повноважень явним і придатним для формального міркування.[1]
На додаток до кінцевих точок, seL4 надає об'єкти сповіщень (notifications): подібні до семафорів об'єкти для асинхронної сигналізації подій та легковагової синхронізації. Сповіщення зазвичай використовуються для доставки апаратних подій переривань драйверам пристроїв у просторі користувача або для сигналізації про зміни стану між компонентами, підтримуючи мікроядерну архітектуру, в якій обробка переривань і драйвери виконуються поза ядром.[15]
seL4 використовує специфікації, написані як математичні моделі в Isabelle/HOL для опису коректної роботи системних викликів. Ці специфікації потім зв'язуються з реалізацією на C для доведення її функціональної коректності: усі системні виклики виконують правильні операції та повертають правильні результати (відсутні логічні помилки, не аварійно завершується, не зависає, тощо).[7][24] Це забезпечує дуже високий ступінь надійності[25] того, що система повноважень ядра забезпечує ключові властивості тріади CIA інформаційної безпеки для процесів: конфіденційність інформації між процесами, цілісність стану ядра та потоку керування, а також доступність шляхом запобігання відмові в обслуговуванні для авторизованого використання ресурсів.[3]
Маючи ~10 тис. рядків коду (LoC) та ~500 тис. рядків доведень (LoP), це один з найбільших верифікаційних продуктів, коли-небудь створених,[26] початкову статтю про який було введено до Залу слави ACM SIGOPS у 2019 році.[4] Накладні витрати верифікації у 50 рядків доведення на 1 рядок коду C різко збільшують вартість розробки та сповільнюють швидкість розробки, ускладнюючи внесення змін.[26] Однак автори стверджують, що при $400 за рядок коду, вартість виявилася меншою за $1000 за рядок для подібних ядер високої надійності (але не верифікованих) і лише вдвічі дорожчою за вартість подібних ядер низької надійності.[27]
Як і в інших формально верифікованих систем, гарантії seL4 є відносними щодо його специфікації та базових припущень. Хоча це означає, що верифікація не охоплює всі можливі несправності, вона все ж суттєво підвищує загальну надійність системи, усуваючи цілі класи дефектів реалізації та роблячи решту припущень явними (і, відповідно, тестованими).[28][26]
- seL4 — це лише мікроядро, на якому будуються повноцінні операційні системи. Однак тематичне дослідження критичних CVE ядра Linux показує, що ізоляція неверифікованих підсистем зменшила б серйозність кожного з обраних CVE, не пов'язаного з допусковим середовищем (pre-boot).[29]
- Доведення не охоплюють усі аспекти функціонуючого комп'ютера під керуванням seL4 і не поширюються на всі підтримувані платформи та конфігурації.[7] Наприклад, початкові доведення стосувалися лише кодової бази на C, але пізніша робота поширила доведення на скомпільовані бінарні файли (верифікація бінарних файлів не підтримується на всіх платформах).
- Хоча seL4 може зв'язувати свої специфікації зі специфікаціями апаратного забезпечення, можуть існувати помилки у специфікаціях або у фізичному апаратному забезпеченні. Однак за понад 15 років публічно не повідомлялося про жодні помилки у верифікованих частинах ядра.[30] Хоча апаратні помилки впливають на усі операційні системи, і seL4 має пом'якшення для деяких відомих апаратних помилок, проєкт наразі не має ресурсів для реалізації стількох пом'якшень, скільки є у зріліших комерційних операційних системах.[31] Це, однак, не є фундаментальним обмеженням seL4.
Хронологія верифікації та функціональних можливостей / дорожня карта (вибрані віхи)
[ред. | ред. код]| Дата | Віха / обсяг | Статус | Примітки |
|---|---|---|---|
| 29 липня 2009 | Доведення функціональної коректності коду на C щодо абстрактної специфікації.[33][7] | Верифіковано | Одне ядро (single core), не поширювалося на бінарний файл. |
| 2011–2012 | Надійний аналіз найгіршого часу виконання (WCET) системних викликів ядра seL4 та затримки переривань для певних одноядерних платформ Arm.[34] | Стабільно (проаналізовано; пізніше доведення вищого рівня використовувалися для покращення меж WCET) | Перший такий аналіз, проведений на системі із захистом пам'яті. Arm з того часу припинила специфікувати найгірші затримки виконання інструкцій, але роботу можна застосувати до майбутніх платформ.[35] |
| 2012–тепер | Доведення забезпечення безпеки (цілісності та конфіденційності потоку інформації) та розширення на коректність бінарного коду[33][36] (згодом розширено на Intel x64 та RISC-V 64)[37] | Верифіковано (підтримка варіюється залежно від платформи) | Підтверджує, що бінарний файл, створений GCC з рівнем оптимізації -O2, все ще забезпечує доведення високого рівня без верифікації/довіри компілятору.[38] |
| 2014–2017 | Техніки аналізу високої надійності (межі циклів, недосяжні шляхи, інтеграція з ланцюжком інструментів), розширені з доведень вищого рівня, що додатково покращує WCET бінарного коду.[39][35][5] | Стабільно (проаналізовано; надійність на рівні досліджень) | |
| 19 листопада 2019 | Системи зі змішаною критичністю (MCS: часова ізоляція / контексти планування) інтегровано в основну гілку.[40] | Стабільно (не верифіковано) | |
| 2019–тепер | Часові побічні канали / механізми «часового захисту» (time protection) оцінюються; формалізація та робота з верифікації тривають.[36] | У процесі | Потребуватиме апаратної підтримки. |
| 2024–тепер | Багатоядерність: дорожня карта верифікованого «статичного мультиядра» (static multikernel) та фреймворк верифікації паралелізму (інкрементальний підхід до надійності)[41] | У процесі | |
| 3-й кв. 2027 | MCS: заплановано завершення верифікації функціональної коректності на рівні C.[32] | Заплановано |
Примітка: Статус верифікації seL4 варіюється залежно від архітектури та конфігурації; документація seL4 надає матрицю того, які властивості охоплені для кожної конфігурації (наприклад, функціональна коректність, цілісність/доступність, конфіденційність та охоплення коректності бінарного коду).[42]
seL4 часто використовується як основа ядра для компонентних вбудованих систем, а seL4 Foundation підтримує набір супутніх інструментів та фреймворків. Артефакти екосистеми (включно з кодом, інструментами та доведеннями) загалом надаються під дозвільними ліцензіями (такими як ліцензія BSD).
seL4 Microkit — це фреймворк операційної системи, побудований поверх seL4, який надає невеликий набір абстракцій, спрямованих на зниження бар'єру для побудови статично структурованих систем зі збереженням цілей продуктивності та ефективності використання пам'яті.[20][43]
seL4 Device Driver Framework (sDDF) — це драйверна архітектура для систем на основі seL4, що обговорювалася на численних самітах; матеріали самітів описують архітектуру, що наголошує на розділенні відповідальностей та подієво-орієнтованій/асинхронній комунікації зі шляхами даних через спільну пам'ять.[44]
LionsOS розробляється групою Trustworthy Systems в Університеті Нового Південного Уельсу (UNSW)[45] і має на меті надати орієнтовані на застосунки сервіси операційної системи, такі як мережа, файлові системи та інший ввід/вивід. Хоча проєкт переважно націлений на статичні архітектури, де ресурси виділяються під час завантаження (наприклад, вбудовані системи), планується підтримка більш динамічних операційних систем.[46][47]
Основні цілі LionsOS — конкурувати з Linux завдяки використанню мікроядра seL4, що зберігає продуктивність системи, водночас забезпечуючи коректну реалізацію апаратного забезпечення seL4 з використанням засобів верифікації на основі теорій про здійснимість за модулем (Satisfiability Modulo Theories, SMT).[48] Основними будівельними блоками запропонованої системи є seL4 microkit та seL4 device driver framework (sDDF). Версія 0.3.0 була випущена 25 березня 2025 року.[49][50]
seL4 Foundation координує аспекти управління проєктом та сприяє вендоронейтральній екосистемі. Початково вона була запущена під егідою Linux Foundation для підтримки ширшого впровадження та довгострокового вендоронейтрального опікування технологією seL4.[10][11] З того часу вона перетворилася на власну незалежну організацію.[51] Вибір GPL для ліцензування було зроблено для заохочення взаємності комерційних інвестицій та стримування форкування.[52] Щорічний seL4 Summit є основним майданчиком для представлення розвитку екосистеми, напрямків досліджень, звітів про досвід та галузевих сесій з метою сприяння комерційним інвестиціям у seL4.[53]
- ↑ а б в Elphinstone, Kevin; Heiser, Gernot (3 листопада 2013). From L3 to seL4 what have we learnt in 20 years of L4 microkernels?. Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. SOSP '13. New York, NY, USA: Association for Computing Machinery. с. 133—150. doi:10.1145/2517349.2522720. ISBN 978-1-4503-2388-8.
- ↑ DornerWorks; VanVossen, Robert (26 листопада 2019). An Introduction To Building Secure Systems with the seL4 Microkernel. DornerWorks (англ.). Процитовано 3 лютого 2026.
- ↑ а б Murray, Toby (2013). seL4: From General Purpose to a Proof of Information Flow Enforcement (PDF). 2013 IEEE Symposium on Security and Privacy. IEEE.
- ↑ а б The Hall of Fame Award 2019. ACM SIGOPS. 29 жовтня 2019.
- ↑ а б seL4 in Australia. Communications of the ACM. Квітень 2020.
- ↑ de Matos, Everton; Lawton, George; Lennon, Conor (2025). Towards seL4 for Enhanced System Isolation and Security on Embedded Devices. IEEE Open Journal of the Computer Society. 6: 1329—1340. Bibcode:2025OJCmS...6.1329D. doi:10.1109/OJCS.2025.3592377. ISSN 2644-1268.
- ↑ а б в г д Klein, Gerwin (2009). seL4: Formal Verification of an OS Kernel (PDF). Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP '09). ACM.
- ↑ "The World's Most Highly-Assured OS" Kernel Open-Sourced. Phoronix. 29 липня 2014.
- ↑ Highly Secure Operating System seL4 Released as Open Source. SecurityWeek. 29 липня 2014.
- ↑ а б seL4 Microkernel Optimized for Security Gets Support of Linux Foundation. The Linux Foundation. 7 квітня 2020.
- ↑ а б seL4 developers create open source foundation to enable safer, more secure and more reliable computing systems. CSIRO. 8 квітня 2020.
- ↑ Andronick, June (11 січня 2022). The sel4 verification: The art and craft of proof and the reality of commercial support (Invited talk). Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, NY, USA: ACM. с. 1. doi:10.1145/3497775.3505265. ISBN 978-1-4503-9182-5.
- ↑ Haslbeck, Maximilian P.L. Chair for Logic and Verification - Teaching. www21.in.tum.de. Процитовано 3 лютого 2026.
- ↑ Cici, Tuna (3 листопада 2024). seL4 Microkernel: Architecture. Medium (англ.). Процитовано 3 лютого 2026.
- ↑ а б в г д е ж seL4 Reference Manual (PDF) (Звіт). seL4 Foundation.
- ↑ Memory Management. seL4 Documentation.
- ↑ а б Heiser, Gernot (7 березня 2019). How to (and how not to) use seL4 IPC. microkerneldude.org.
- ↑ The seL4 Device Driver Framework. docs.sel4.systems.
- ↑ а б The seL4 Microkit. docs.sel4.systems.
- ↑ mq_overview(7) - Linux man page. linux.die.net (англ.). Архів оригіналу за 2 серпня 2025. Процитовано 2 лютого 2026.
- ↑ Kerrisk, Michael (2010). 5: POSIX Message Queues. The Linux programming interface: a Linux and UNIX system programming handbook (PDF). San Francisco: No Starch Press. ISBN 978-1-59327-220-3.
- ↑ Rashid, Richard (1986). Mach: A New Kernel Foundation for UNIX Development (PDF). USENIX.
- ↑ Verification: What the Proof Implies.
- ↑ Formal Methods | DARPA. [www.darpa.mil. Процитовано 3 лютого 2026.](https://www.darpa.mil}})
- ↑ а б в Fisher, Kathleen; Launchbury, John; Richards, Raymond (13 жовтня 2017). The HACMS program: using formal methods to eliminate exploitable bugs. Philosophical Transactions. Series A, Mathematical, Physical, and Engineering Sciences. 375 (2104) 20150401. Bibcode:2017RSPTA.37550401F. doi:10.1098/rsta.2015.0401. ISSN 1364-503X. PMC 5597724. PMID 28871050.
- ↑ Heiser, Gernot (2015). seL4 is Free! What does it mean for you? (PDF).
- ↑ Hall, Anthony (1990). Seven Myths of Formal Methods (PDF) (Звіт).
- ↑ Nerup, Carl (6 вересня 2018). Microkernels Really Do Improve Security - Cog (амер.). Процитовано 3 лютого 2026.
- ↑ seL4 Proofs | seL4. sel4.systems. Процитовано 2 січня 2026.
- ↑ seL4. Document that the x86 port has known vulnerabilities · Issue #1108 · seL4/seL4. GitHub (англ.). Процитовано 23 лютого 2026.
- ↑ а б Development Roadmap. seL4. Процитовано 2 січня 2026.
- ↑ а б History. seL4.
- ↑ Blackham, Bernard (2011). Timing Analysis of a Protected Operating System Kernel (PDF). Proceedings of the IEEE Real-Time Systems Symposium (RTSS).
- ↑ а б WCET: Worst-Case Execution-Time Analysis of seL4. Trustworthy Systems.
- ↑ а б seL4 verification project. Trustworthy Systems.
- ↑ Andronick, June (2022), Griggio, Alberto; Rungta, Neha (ред.), The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved (англ.), TU Wien, TU Wien, с. 1, doi:10.34727/2022/ISBN.978-3-85448-053-2_1, процитовано 3 лютого 2026
- ↑ Myreen, Magnus O. (25 січня 2018). Verification of the GCC-Generated Binary of the seL4 Microkernel (PDF). ENTROPY 2018 (англ.). Cambridge, United Kingdom: Chalmers University of Technology. Процитовано 2 лютого 2026.
- ↑ Blackham, Bernard (2014). High-Assurance Timing Analysis for a High-Assurance Real-Time Kernel. Real-Time Systems.
- ↑ Announcing new releases: seL4-11.0.0, camkes-3.8.0, CapDL ... lists.sel4.systems (HyperKitty).
- ↑ seL4 Summit 2024 Abstracts – seL4 Verification: Status and Plans. seL4.
- ↑ Verified Configurations. seL4 Documentation.
- ↑ seL4 Microkit (slides) (PDF). seL4 Summit 2023.
- ↑ The seL4 Device Driver Framework (sDDF) (slides) (PDF). seL4 Summit 2023.
- ↑ The seL4 microkernel | TS. trustworthy.systems. Процитовано 3 травня 2026.
- ↑ Heiser, Gernot; Velickovic, Ivan; Chubb, Peter; Joshy, Alwin; Ganesh, Anuraag; Nguyen, Bill; Li, Cheng; Darville, Courtney; Zhu, Guangtao (27 травня 2025), Fast, Secure, Adaptable: LionsOS Design, Implementation and Performance, arXiv, doi:10.48550/arXiv.2501.06234, arXiv:2501.06234, процитовано 3 травня 2026
- ↑ Introduction. LionsOS 0.3.0 (en-au) . Процитовано 2 лютого 2026.
- ↑ Lions OS: Secure, Fast, Adaptable. Institute for Computing Platforms - Systems Group (англ.). Процитовано 3 травня 2026.
- ↑ 0.3.0. LionsOS 0.3.0 (en-au) . Процитовано 3 травня 2026.
- ↑ au-ts/lionsos, Trustworthy Systems, 1 травня 2026, процитовано 3 травня 2026
- ↑ The seL4 Foundation | seL4. sel4.systems. Процитовано 2 лютого 2026.
- ↑ What does seL4's license imply?. microkerneldude (англ.). 9 грудня 2019. Процитовано 2 лютого 2026.
- ↑ seL4 Summit 2025 – Panel: Building a business case for using a verified kernel. seL4.systems.
