51–60 of 66 posts
Earlier quoted context omitted.
Microkernels by themselves are not special; SeL4 is because it's proven to be secure.
It's proven correct against specification. That's not the same thing as 'secure' (although it helps).
Having said that, it is surprisingly easy to get hardware to violate its specifications.
Is there a seL4 implementation targeted at, like, dinking around on some desktop, or is this stuff mostly interesting to embedded-ish folks?
Maybe an ARM desktop once multi core is implemented and verified. Verifying the whole thing for x86 seems scary. It is a kind of undertaking that gives normal people a glimpse of how ADHD is. It is a huge task and I would not know how to structure it, where to start and how to predict and plan all the intermediate steps.
Write down all the modules, then write down their dependencies on each other. Make sure the dependency graph is as close to a line as possible. This is called “layering” in software engineering.
Now, figure out how to prove each layer correct.
Earlier quoted context omitted.
Microkernels by themselves are not special; SeL4 is because it's proven to be secure.
SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...
Earlier quoted context omitted.
Microkernels by themselves are not special; SeL4 is because it's proven to be secure.
SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...
Makes me wonder when we finally get proper government funding of FOSS projects.
A lot of the seL4 work was actually funded by several nations' taxpayers, and developed by the late Trustworthy Systems group at Data61 (formerly NICTA). Sadly, they were disbanded a few years back and had to rush to set up a standalone seL4 Foundation: https://microkerneldude.org/2020/04/07/the-sel4-foundation-w... > seL4 is the result of big investments. Firstly by the Australian tax payers, who (through NICTA) fun…
Earlier quoted context omitted.
SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...
Why is it interesting?
Earlier quoted context omitted.
SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...
Why is it interesting?
Pure capability-based access control, where capabilities are communicable, but not forgeable "references with rights" to objects. While this is interesting, it's not really unique: other L4 kernels also have it, and Capsicum (but not POSIX capabilities) implements something like it on Unix. But even here, seL4 has some unique twists, such as the way IPC replies are handled, which allows policies that prevent "unsolicited" replies.
A unique approach to memory management, where after boot-time, the kernel does no memory management, and even kernel memory is managed completely by user-level code. In fact, the kernel has no heap. Instead, when the user requests an operation that requires kernel memory (e.g. creating an address space, which requires memory for page tables) the user provides the memory explicitly to the kernel. This sets seL4 apart not just from monokernels, but from other L4 kernels as well.
Support for passive servers: one of the most exciting recent features, these are server processes that run on scheduler time "donated" by the client. Among other things, this can be used to make sure that non-critical clients will not monopolize services needed by critical clients.
IIRC seL4 is also the fastest L4 kernel for most use cases - and its worst-case execution time is bounded, at least on older CPUs which have published timing data.