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

Reply via email to