On 1/22/20, Demi M. Obenour <demioben...@gmail.com> wrote: > > Me too. I was attracted to seL4 mostly because of the hope that it could > replace Xen in QubesOS. QubesOS certainly qualifies as a large dynamic > system! >
I think a better approach to a secure microkernel-based Linux-compatible OS is to make a Linux-compatible microkernel-native OS rather than trying to virtualize Linux, since it's easier to run everything with least privilege if your protection domains are processes rather than VMs. You don't even have to give up Linux's hardware support since the LKL project <https://github.com/lkl/linux> should allow the use of Linux drivers within user-mode servers reasonably easily (it does mean giving up much of the vertical modularity seen in many microkernel OSes, but in general I think that vertical modularity offers relatively little benefit for most OS subsystems and isn't worth the overhead). > >> I strongly suspect the more fundamental and general extension would be to >> remove the scalability limitation of Notifications, probably by >> generalising them to a hierarchy, i.e. you signal a sub-notification >> which >> then signals the higher-level notification. I’m not claiming having >> thought >> this through, though. > > That approach seems good. It does require side tables, but it is probably > significantly less intrusive. Being able to read multiple levels of > notifications in a single system call would be especially helpful. Yeah, I'd agree that seems like a good way to handle multiple notifications as well. > > Highly dynamic systems generally avoid arbitrary limits (not imposed > by the physical hardware) whenever possible, since someone *will* > eventually hit them. That said, one could make a decent argument that > a typical userspace client process will not have over 20 processes that > will be sending data to it at high speed. Most userspace processes > don’t simultaneously interact with 20 different subsystems of a > monolithic kernel, after all. I would expect a userspace process > to need to receive notifications from network, graphics, input, > storage, Bluetooth, and USB subsystems. Everything else will likely > be low-speed control messages, which can be handled by a userspace bus. > Implementing D-Bus on top of seL4 IPC would be a nice project. > Personally I'd say a better approach is to just go with a pure file-oriented architecture in which byte and sequential packet streams accessed through a filesystem namespace are the only form of IPC exposed to user programs, and then implement things like D-Bus and other RPC on top of that. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
