ACM Software System Award Given to seL4 Microkernel
awards.acm.org
awards.acm.org
Also in memoriam Jochen Liedtke [0], who started the L4 kernel project and rekindled research in microkernels by showing that they don't have to be slow ('slow' as in Mach's long IPC latencies).
The verification story is currently stronger with RISC-V.
Considering close cooperation between seL4 and RISC-V projects, ARM aka the legacy architecture is unlikely to be a priority anytime soon.
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.
It is signed by apple and verified as part of the secure boot process.
> The Secure Enclave Processor runs an Apple-customized version of the L4 microkernel.
[1] https://support.apple.com/guide/security/secure-enclave-sec5...
For what it's worth, I'm not sure Apple publishes which variant of L4 it runs on, and there are many of them. The whole formal verification conversation here might be moot.
The SEPOS kernel is an apparently derived from a fork of L4-embedded they used in Darbat (a fork of XNU to run on top of L4). Not formally verified unless Apple internally has done so.
And they've made a lot of pretty deep changes for example adding native support for Mach-O files.
https://www.zdnet.com/article/minix-intels-hidden-in-chip-op...
I wish someone would build a beyond-posix desktop OS on top of it...
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.
The memory management, scheduling and IPC are implemented in an interesting and novel way (compared to your typical mainstream OS) and allow for quite different OS design.
In particular, capability-based IPC and memory management could provide a robust base for a secure OS from the ground up, instead playing whackamole in an aging POSIXish design.
Sadly (tho I understand the rationale), most approaches to building a full OS on top of (L4 in general) are "run userspace Linux in an isolated container", which kind of ignores all the power underneath.
Having said that, it is surprisingly easy to get hardware to violate its specifications.
I believe seL4 is also used for the firmware on Qualcomm modems now, but it's a little hard to follow if they've switched from OKL4 which was a related project.
Isn't seL4 more used for things like data diodes, cryptographic equipment and military hardware? Stuff that you need to keep from getting hacked or malfunctioning, but not time-shared with untrusted users.
> our L4- embedded kernel from the mid-Noughties runs on the secure enclave of all recent iOS devices (iPhones etc)
https://research.redhat.com/blog/article/look-to-the-horizon...
> seL4 is the result of big investments. Firstly by the Australian tax payers, who (through NICTA) funded its creation, and (through NICTA and then CSIRO’s Data61) continued supporting it. Over the past 6 years, US taxpayers (mostly through DARPA, but also other parts of the DoD as well as DHS) invested a lot in completing and extending the verification story, as well as deploying on real-world systems. And most recently, HENSOLDT Cyber funded verification of the RISC-V port of the kernel.