On 3/7/25 9:09 PM, Gernot Heiser via Devel wrote:
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.
What do you consider to be the TCB? To an end user, a computing system is defined by its inputs and outputs. This means that whatever the system’s identity is from the perspective of the outside world is part of the TCB. For a server, that identity can be a cryptographic secret key that only trusted code can use. For other systems, that identity is the ability to access sensor data and control whatever effectors the system has. This means that drivers for critical sensors and effectors are part of the TCB. In the case of a headful system (desktop/laptop/mobile), the most critical effector is the display, and the most critical sensors are some combination of a keyboard, mouse, touchpad, and/or touchscreen. This means that the drivers for these are also in the TCB, because they can impersonate the user (to the system) or the system (to the user). Do you plan to verify these drivers? -- Sincerely, Demi Marie Obenour (she/her/hers)