#sel4 — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #sel4, aggregated by home.social.
-
Someone should build a #smalltalk like system on top of #seL4; every object is its own protection domain. I.e., state encapsulation not as an aspirational promise, but as an enforced property.
-
[Перевод] Введениев в микроядро Sel4
Предлагаю вашему вниманию перевод seL4 Whitepaper, который является хорошим введением в одно из самых известных микроядер для ОС — seL4 (лицензия GPLv2). Здесь не только специфика seL4 и микроядер, но и много полезного материала в целом по безопасности, формальной верификации, виртуализации и системам жёсткого реального времени.
https://habr.com/ru/articles/1036890/
#sel4 #микроядро #microkernel #верификация #secure #realtime #безопасность #capability #операционные_системы #производительность
-
Are you doing something interesting with #sel4? The call for presentations is now out for the #sel4summit 2026 in Vancouver!
-
Flutter, Fuchsia, Zircon, ChromeOS, Aluminium OS, WGPU, Tensor Modem, RIL, SeL4, FIDL будущее Андроида и других ОС №2
В конце 2025 года техноблоги взорвались инсайдами: Google планирует выпустить премиальный ноутбук под брендом Pixel. Но работать он будет не на ChromeOS, как привычные «Хромбуки», и не на Windows. Кодовое имя инициативы — Aluminium. Новость не обошла стороной и хабр. Суть проекта как обычно для Google проста и жестока: ChromeOS как отдельная операционная система должна умереть. Будущее — это Android, который научился быть десктопом. Но прежде чем говорить об Aluminium, нужно понять, почему Flutter стал критичным для всей стратегии Google. И здесь начинается история о том, как устаревший C API чуть не убил будущее кроссплатформенной разработки.
https://habr.com/ru/articles/984090/
#flutter #android_for_desktop #dart #chrome_os #aluminium_os #fuchsia #Tensor_Modem #RIL #SeL4 #FIDL
-
I really wish #seL4 was used in the open source space.
-
I think I'm going to take inspiration from #seL4's microkit system description for my #rust #microkernel I don't feel like implementing automatic device discovery, so defining drivers in a static file would be a good way to avoid that complexity. the only difference is, I think I'll use TOML instead of XML because I really, really hate XML.
-
im gonna experiment with seL4 :3
might even try to write some Rust code for it! -
Has anyone ported seL4 to RP2350 yet? #seL4 #rp2350 #embeddedsystems
-
The seL4 Summit takes place next week in Prague already. Whom am I going to meet there? https://events.linuxfoundation.org/sel4-summit/ #microkernel #os #conference #prague #sel4 #sel4summit
-
#seL4 is based on amazing ideas, but I have yet to see an ecosystem built around it.
-
The SeL4 Microkernel: An Introduction [pdf]
https://sel4.systems/About/seL4-whitepaper.pdf
#HackerNews #SeL4 #Microkernel #Introduction #seL4 #Whitepaper #Microkernel #Architecture #System #Security
-
On Apple Exclaves. Enhancing kernel isolation, one step at… | by Random Augustine | Feb, 2025 | Medium
Link
# 蘋果 Exclaves 系統安全機制解析
## 📌 Summary:
本文深入分析了蘋果在 2024 年導入的 Exclaves 安全機制，這是為瞭解決傳統單體核心作業系統的安全漏洞問題。蘋果透過將敏感資源與功能從 XNU 核心中隔離，建立了一個基於 seL4 微核心的「安全核心」(Secure Kernel)，運行在與主系統隔離的「安全世界」(Secure World)中。這種設計能在主核心被入侵時仍保護關鍵資源，包括攝影機、麥克風指示燈、神經引擎功能等。Exclaves 代表了蘋果為增強 iOS、macOS 等系統安全所做的重大投資，提供了比其他終端裝置製造商更強大的安全防護機制。
## 🎯 Key Points:
- 現代作業系統通常採用單體核心設計，一旦發生漏洞可能導致整個系統被入侵，蘋果的 XNU 核心同樣面臨這個問題
- 蘋果自 2013 年起逐步建立安全隔離方案：先有安全隔離區(Secure Enclave)，後有頁面保護層(PPL)和安全頁表監控(SPTM)
- 2024 年，蘋果在 M4 和 A18 處理器上推出 Exclaves，將敏感資源隔離到安全區域
- Exclaves 運行在名為「安全核心」(Secure Kernel)的微核心上，很可能基於 seL4 開發
- 系統通過建立「安全世界」(可能基於 ARM TrustZone 技術)來隔離 Exclaves，即使 XNU 被入侵也能保護敏感功能
- Exclaves 分為多種資源類型：共享記憶體緩衝區、音訊緩衝區、感測器、Conclaves(多資源分組)及服務
- 執行緒可以從不安全世界切換到安全世界執行代碼(Downcall)，也能反向請求 XNU 服務(Upcall)
- 蘋果使用 Exclaves 保護攝影機/麥克風指示燈、Apple 神經引擎功能、與安全隔離區通訊的組件等
## 🔖 Keywords:
#Exclaves #安全核心 #ARM_TrustZone #單體核心安全 #seL4 -
Ein Meilenstein für IT-Sicherheit: Die @Cyberagentur hat am 20.01.2025 fünf Verträge für das Forschungsprogramm „Ökosystem vertrauenswürdige IT“ (ÖvIT) unterzeichnet. Ziele: Beweisbare IT-Sicherheit und ein internationales Netzwerk von Experten.
Mehr Informationen: https://t1p.de/8mb4c
#ÖvIT #Cybersicherheit #FormaleVerifikation #Forschung #seL4 -
-
also found this for #sel4 #microkernel. i havent watched beyond the first lecture yet though, as i keep discovering so many more new concepts. i barely knew "object capabilites" (aka #ocap i think) before this. i thought pausing this and going back to the other series would be worth it.
https://www.youtube.com/playlist?list=PLtoQeavghzr3nlXyJEXaTLU9Ca0DXWMnt -
Oh wow, I wasn't aware that #seL4 Foundation has uploaded the lectures of #UNSW's famous Advanced Operating Systems course to youtube.
https://www.youtube.com/watch?v=IvqM2pmApSY&list=PLtoQeavghzr3nlXyJEXaTLU9Ca0DXWMnt
#os #microkernel #operatingsystems -
@riskybusiness RE your discussion about viewing iPhone on macOS - I’m 99% sure this is a direct device to device connection, iCloud isn’t involved other than the devices being on the same account and having shared secrets/keys.
It’s not that different from the current implementation that lets you use an iPad as a second screen over wifi - it’s designed for the “my phone is in my pocket/over there charging and I don’t want to get it” use case, not the “my phone is at home and I want to stream its screen over the internet” case - unless I’ve missed something? I’d be shocked if it weren’t encrypted using keys in each device’s Secure Enclave.
Somewhat unrelated, but this also reminds me of some tech DST Group showed me years ago when we were teaching them. It allowed a user to use an untrusted web browser/computer to connect to a Remote Desktop-esque page, but the image was encrypted They had a device which sat between the computer and monitor which decrypted the image signal, and encrypted keyboard/mouse data back to the page. (All built on #seL4 of course).
-
In the first of our #EverythingOpen schedule highlights, we're delighted to present #UNSW Scientia Professor @gernot who will present on efforts to take #sel4 from a #MicroKernel to fully-fledged #OS
with #LionsOS, named for open source luminary, John Lions.Schedule will be posted soon, we promise!
Heavily discounted #EarlyBird #EB tickets still available, for a short time only:
https://2024.everythingopen.au/news/registrations-open/ -
Interestingly, #seL4 would be a worse choice that #Xen for #QubesOS, due to its worse support for x86 speculative execution mitigations. Xen typically provides patches the day the embargo breaks, and Qubes OS users rely on that. There are various ways to make speculative execution less of a concern, but they don’t work for Qubes OS. This is because Qubes OS heavily overcommits CPU and allows execution of arbitrary untrusted code in VMs.
I don’t fault the seL4 developers for not focusing on a use-case that is practically the worst-case scenario for it. It just means that Qubes OS is very much more like a server than an embedded system, and so it needs a hypervisor that is designed for the kinds of workloads it runs.
