On 3/26/25 4:04 PM, Gernot Heiser via Devel wrote:
On 27 Mar 2025, at 05:22, Gernot Heiser <gernot@unsw.edu.au> wrote:
I guess, in seL4 world one structures the system like this: there is a protocol which requires the client VM to work with the TCB along these lines: give up N pages from it's memory allocation back to the TCB which then "moves" them into the driver. The TCB has to be "below" the client in the capability chain to make sure that the client looses the ability to revoke the pages from the driver,
That would be one way of doing it in seL4 if the client *does* own the
Note that even if you use a protocol where the client supplies
shared-memory frames directly to the server, the server can still protect itself from the client.
If the client unmaps the shared page, the server will trigger a page
fault on its next access.
That invokes the server’s page-fault handler (normally part of the resource manager, but could be a thread inside the server). The page-fault handler finds that the fault is due to a page shared with
This would presumably involve revoking all further client access (i.e. revoking all of the client’s caps to server endpoints/notifications etc) – a clear case where revocation is essential to stop further requests from
The fault handler would then clean up state the server holds on behalf of the client. And it would recover the server by aborting whatever operation was faulted and re-set the server to a sane state.
In most designs, this work would be split between two handlers: The
But theoretically it could be all internal to the server (which then
needs to rely on owning its internal memory, i.e. can’t be revoked).
If the handler is external (part of a trusted resource manager) then
"Having to rely on VMs for anything that isn’t written from scratch for seL4 would not be great." A stripped down Linux kernel seL4 VM boots in few seconds. Just tweak Linux to be fast and have a full flexible environment. As a QubesOS user I don't see any speed difference from running Xen guests... On Wednesday, March 26, 2025, Demi Marie Obenour via Devel <devel@sel4.systems> wrote: pages. the client and takes appropriate action. the mis-behaving client. page-fault handler being part of a trusted resource manager (i.e. something higher up in the trust hierarchy) which invokes a server-internal handler for cleanup/recovery. that could implement transparent demand paging of the server too, it would have to do enough bookkeeping to be able to distinguish between faults on client-provided memory and faults triggered by server pages being swapped out.
Demand paging must be functionally transparent to the paged task.
Meaning the resource manager must observe an invariant that if a page is unmapped (eg for swapping to backing store), a page fault triggered by that will only restart the paged task once that page is mapped to a frame that has the same content as the one that had been unmapped earlier. Then the functionality of the paged task is unaffected by paging.
Paging is still observable in the timing, of course, but that’s not different from being preempted by a higher-priority thread.
The design space is big – which is part of the challenge with seL4: it’s easy to do bad designs, and requires a lot of expertise to do good ones. Which is why we’re working on sample designs. LionsOS is a one with a static architecture, that avoids a lot of the complexity (and should ease verification). But we also have a fully dynamic one in the works, but that one is at a very early stage.
Will it be possible to implement a POSIX-like API on top of this? By “POSIX-like”, I mean “similar enough to POSIX that existing applications like browsers, web servers, etc can be ported fairly easily.” Having to rely on VMs for anything that isn’t written from scratch for seL4 would not be great. -- Sincerely, Demi Marie Obenour (she/her/hers) _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems