On 8 Mar 2025, at 10:29, Andrew Warkentin via Devel <devel@sel4.systems> wrote:
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.
I don’t see a reason for providing bulk data copying as a kernel service (despite Liedtke doing this in the original L4, in violation of his own minimality principle). It can (and therefore should) be provided as a user-level service, which is why we dropped it in seL4. And, done properly, it’ll easily outperform QNX’s in-kernel implementation.
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).
Our design (details of which are still very much in flux and thus too early to publish) reduces the TCB to something that should be verifiable. Gernot