On 26 Mar 2025, at 15:22, Anton Burtsev via Devel <devel@sel4.systems> wrote: For example, in a classical Xen split device driver model, i.e., a shared device driver VM (or a process in seL4) multiplexes a single physical device across multiple client VMs. In Xen each client connects to the driver VM and provides a set of pages to establish a region of shared memory for communication. The fact that these pages provided by the client protects the driver from a denial of service attack. In Xen it's impossible to revoke the pages -- once they are granted they belong to the driver VM (at least if I remember correctly, there might be some nuances and I didn't look at Xen recently). This scenario seems hard in seL4 as the shared pages can be revoked at any time. Well, in seL4, unprivileged tasks don’t normally *own* their resources (in the sense of having access to the caps that control them – apps don’t normally have access to teir own Cspace) but this is left to a more privileged resource manager, which would be responsible for establishing the shared memory in which case this problem doesn’t exist. 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 pages. However, a better protocol in that case would be for the client to *grant* the page to the server (driver) and the server to map them back to the client.By the same protocol the client could request a revoke, by requesting the server to grant them back. Effectively, in seL4, if my understanding above is correct, one structures the system in such a manner that revocation is eliminated, i.e., the client cannot revoke its pages. Revocation is needed for any dynamic resource management. But that doesn’t mean that an untrusted app is given that power. Eg, how do you implement demand paging? The server unmaps some of your memory, and re-maps it on demand. But then a logical question: why do we need revocation in the first place? In the end the client trusts the driver to release the pages back via the TCB when connection is teared down. This seems natural -- there is a degree of trust and cooperation between clients and the driver. That’s still revocation, isn’t it? Just not by the untrusted app. Of course, no-one stops you from building silly systems where untrusted tasks can stuff up others. Gernot