On 11/22/20, Demi M. Obenour
Do you believe that an seL4-native general-purpose OS is practical? I certainly hope so! What do you believe such an OS would look like?
UX/RT will look like a loose reimplementation of QNX with several concepts from Plan 9 and Linux thrown in. It won't really be a clone of any of those systems though. I think a QNX-like architecture (i.e. a natively Unix-like system with the filesystem as an IPC transport layer, as well as avoidance of most vertical modularization of subsystems) is the most practical architecture for a microkernel-based general-purpose OS.
There is a distinction between assurance (essentially, correctness) and security. For instance, a legacy VM can still be very secure if there is no way for untrusted data to enter it, or if its interactions with untrusted data are extremely limited. That’s how QubesOS works, and it has proven to be quite successful. In the case of QubesOS, this has allowed Linux-native desktop environments (such as XFCE and KDE) to be used in security-critical areas. This in turn allows for a much better user experience than would otherwise be possible given the project’s resources, and has been critical in QubesOS’s success in the desktop space.
Yes, that kind of system can work and be reasonably secure, but it adds significant overhead, and can't really be implemented easily on top of a static system, since you pretty much need one VM per application.