On Fri, Apr 19, 2024 at 3:07 PM Michael Neises <neisesmich...@gmail.com> wrote: > > I think Hugo has a salient point when he says a world of bespoke seL4 > images for every application is a distant one. I share the feeling that a > hybrid, intermediate step is meaningful. I also echo the idea that > exploitation at scale is a matter of statistics. > > Even if virtualizing the seL4 undermines its security properties, it is > still a fast and correct microkernel. Putting a usable seL4 image in the > hands of enthusiasts, budding developers, or even seasoned developers would > be a boost to the ecosystem. > > One reason Linux is so popular is that you can use Linux to develop Linux. > I would be thrilled to boot any meaningful home or development environment > on top of the seL4. I would never stop talking about it. >
I don't really think the static Microkit/CAmkES type of architecture will ever be viable for desktops or self-hosting. Basically nobody's going to put up with rebooting into a different image for each application like an 80s-era home computer (if that's the kind of thing you meant by "bespoke seL4 images"). The closest you'd get would be something like Genode, which is more or less a dynamic system that's managed like a static one, and even something like that would be too awkward for most people. Even for some types of embedded systems, a static architecture is going to be rather limiting (e.g. a CNC machine that can have additional hardware like automatic parts loaders or additional axes added). Running per-application static seL4 images in a dynamic hypervisor also seems kind of pointless; you might as well use a regular (non-hypervisor) dynamic microkernel OS instead. IMO the best approach for a microkernel-based desktop OS is something architecturally more like QNX than Microkit/CAmkES, since porting existing Linux code to something like that is going to be relatively easy. Even though such a system is going to be difficult or impossible to formally verify as far as security goes since it's so open-ended, it's still going to be a lot more architecturally secure than anything mainstream. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
