On Fri, Mar 7, 2025 at 8:37 PM Isaac Beckett via Devel <devel@sel4.systems> wrote:
Hello! I saw Microkit 2.0 has just been released, and it’s prompted a question I’ve been thinking about since before Microkit, when CaMKes was the main thing:
Both Microkit and Camkes are designed for embedded and/or static systems, where there is no detection/configuration of hardware at runtime, and in Microkit no swapping of components such as drivers.
Is there any work ongoing to use seL4 for a general purpose operating system? Like, a situation where you may have e.g. PC style hardware that can have all sorts of reconfiguration between power-off and next boot, or even while booted and running.
Of course this introduces a lot of attack surface, but it makes a lot more sense for a general purpose computer, rather than an embedded one.
Is there any recent work/prior art on using seL4 outside of the context of deeply embedded systems?
I was trying to base the QNX-like OS I'm writing < https://gitlab.com/uxrt/uxrt-toplevel> on seL4, but I gave up and decided to fork it when I couldn't efficiently implement QNX-like IPC (which involves copying arbitrary-length buffers directly between address spaces) on it. Eventually it will probably end up diverging from seL4 quite significantly. At some point I may write a companion OS based on seL4 proper with a compatible subset of the API for static deeply-embedded systems, but that isn't a priority for me. I'm a bit skeptical of the benefits of kernel verification alone for what I'm writing, since most of security is managed by the process server, which is unverified. Verification is going to be significantly more difficult for dynamic systems in general, since whatever user-level servers are responsible for handing out capabilities will themselves have to be verified if kernel verification is to actually be meaningful (and verifying such servers is probably going to be more difficult than verifying the kernel).