Re: [seL4] Request for enhancement: Notification queues

On 2020-01-22 23:35, Andrew Warkentin wrote:

On 1/22/20, Demi M. Obenour 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.

I think that is a good idea in some cases, but I believe that it will impose unnecessary overhead in others. In the case of graphics, for example, marshaling would be significant overhead. I believe that having the graphics driver be an seL4 native server would be a better approach. The same goes for virtualization, networking, and storage. Graphics is interesting because a GPU has its own MMU, which can provide strong, hardware-enforced isolation. This allows for secure graphics drivers to be implemented in a surprisingly small amount of code, provided that legacy device support is dropped. The Genode project was able to implement full support for OpenGL this way. For networking, it would be nice if performance could be similar to that achieved by DPDK/Snabb. That isn’t compatible with the Berkeley sockets API. Message buses, such as D-Bus, can likely be made much faster if the server can copy memory from one client’s address space to another. That’s why Android has Binder, for example, and why kdbus was almost a thing on Linux. Sincerely, Demi