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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
