Originally I thought Fuchsia was the first kernel to extensively use capability-based security, but it looks like in seL4 they are also the main security primitive.
-
Could somebody with 1500+ reputation create a tag "seL4", so it could be added here? Seems there is some work in a seL4 specific Q/A site for stack overflow: https://area51.stackexchange.com/proposals/120611/sel4 – Axel Heider Nov 28 '18 at 16:11
-
Could you please clarify the question? Do you want to know the first capability based kernel? Or the differences between Fuchsia and seL4? – Anna Lyons Nov 29 '18 at 23:51
-
@AnnaLyons The later, but only if they are conceptual vs implementation details. – LOST Dec 01 '18 at 00:03
-
@Lost OK, I've answered based on that. Happy to answer any follow-up questions! – Anna Lyons Dec 02 '18 at 22:31
-
1created tag `sel4` – RAbraham Dec 04 '18 at 04:21
-
In case anyone stumbles upon this: capabilities were already used to implement resource access control in first generation microkernels. Second generation microkernels such as L4 did away with them for performance reasons. They then later reappeared in the third generation (as both a resource access control and resource accounting mechanism), i.e. seL4 but also e.g. Fiasco.OC. – Peter Dec 02 '20 at 16:35
1 Answers
Fuchsia is a capability-based operating system built on top of Google's Zircon microkernel, which is itself is based on the little kernel.
It makes more sense to compare Zircon to seL4, or an operating system framework like Genode (which runs on seL4) to Fuchsia. I'll briefly compare seL4 to Zircon.
seL4 provides minimal mechanisms and is designed for high-assurance systems. Zircon provides a lot of policy and is not designed for high-assurance, with a focus on utility. I believe both aim at high performance. In short, seL4 is a very minimal microkernel compared to Zircon.
For example while seL4 provides the mechanisms to build a process abstraction, it does not define a process at all. Comparatively Zircon has much policy built into the microkernel itself, including processes. seL4 has proofs of many properties (functional correctness, integrity, isolation) when configured for specific platforms, and Zircon does not.

- 228
- 2
- 4