Hi Genode, I am building userspace on seL4 directly and have run into a design issue. I am implementing server and client using badged endpoints. I think Genode would have run into the same issue, and I would like to understand better how Genode solves it. It is not directly a Genode question, but I would benefit from your experience. Below I have laid out the scenario, the issue, and some questions.
*Scenario*
I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knows which object the client is trying to manipulate.
The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object.
*Issue* I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and give the badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has no way to look up the badge of the second cap, it cannot look up the underlying object for obj_T2.
So my questions are:
1.
Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask. 2.
Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it? 3.
As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why.
Thanks for the help, everyone!
Thanks, Sid Graduate Student @ UBC sid-agrawal.ca
Hi Sid,
I'm not an expert regarding the topic you're in. However, if I'm not mistaking, the badges you're talking about sound like what is accomplished by the so-called ID space in Genode [1][3][4].
Some examples on how ID spaces are used are the Trustzone VMM block driver [2] that manages its device objects with IDs, the VFS file systems [5] and GPU buffers [6]. Maybe, looking into that code provides you with some answers.
Let me know if so!
Cheers, Martin
[1] <GENODE>/repos/base/include/base/id_space.h [2] <GENODE>/repos/os/src/server/tz_vmm/include/block_driver.h [3] https://genode.org/documentation/genode-foundations-21-05.pdf 8.8.4. ID space [4] grep -r "ID space" <GENODE>/doc/ [5] <GENODE>/repos/os/src/lib/vfs/fs_file_system.h [6] <GENODE>/repos/os/src/drivers/gpu/intel/main.cc
On 20.04.22 00:42, Sid Agrawal wrote:
Hi Genode, I am building userspace on seL4 directly and have run into a design issue. I am implementing server and client using badged endpoints. I think Genode would have run into the same issue, and I would like to understand better how Genode solves it. It is not directly a Genode question, but I would benefit from your experience. Below I have laid out the scenario, the issue, and some questions.
_Scenario_
I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knowswhich object the client is trying to manipulate.
The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object.
_Issue_
I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and givethe badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has noway to look up the badge of the second cap, it cannot look up the underlying object for obj_T2.
So my questions are:
Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask.
Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it?
As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why.
Thanks for the help, everyone!
Thanks, Sid Graduate Student @ UBC sid-agrawal.ca http://sid-agrawal.ca
Genode users mailing list users@lists.genode.org https://lists.genode.org/listinfo/users
Hi Martin, I think my question was slightly different.
It can be better explained by giving the example of attaching a function for a region_map. This function takes in a dataspace capability as an argument. I understand that when a client does a rm_client.attach(ds_cap, vaddr, size ...) It is transformed (by the client stub code) to a seL4 IPC message which goes over a badged-endpoint to the rm_service in the core.
The rm_service finds out which rm to manipulate by knowing which badged endpoint the message was delivered to(I think). However, it also got another badged endpoint cap as an argument (the one for dataspace). seL4 will not reveal the badge for this endpoint as the IPC message did not arrive over this endpoint. But the core still needs to find the dataspace corresponding to this dataspace-cap. So my question is, how can the server know the badge of an endpoint that it had issued in the past.
I think the answer lies in [1] *decode_seL4_message() and new_seL4_message()* functions. Here I see that when Msfbuf_base has a cap as an argument(dataspace cap in the case of rm.attach()), it is added in the IPC msg buffer in two places:
- The seL4 cap is sent as an extra cap in the IPC message - Another place is an IPC message argument. Looks like it is a value of the RPC object.
I think the 2nd one is the missing piece in my design. I relied solely on the server to recognize the server-side object using just the badged endpoint seL4 cap. This does not work as seL4 will not reveal the badge of any of the endpoints caps, which came as extra caps in a message.
Thanks, Sid
[1] <GENODE>/repos/base-sel4/src/lib/base/ipc.cc's
On Fri, Apr 22, 2022 at 2:37 AM Martin Stein martin.stein@genode-labs.com wrote:
[CAUTION: Non-UBC Email]
Hi Sid,
I'm not an expert regarding the topic you're in. However, if I'm not mistaking, the badges you're talking about sound like what is accomplished by the so-called ID space in Genode [1][3][4].
Some examples on how ID spaces are used are the Trustzone VMM block driver [2] that manages its device objects with IDs, the VFS file systems [5] and GPU buffers [6]. Maybe, looking into that code provides you with some answers.
Let me know if so!
Cheers, Martin
[1] <GENODE>/repos/base/include/base/id_space.h [2] <GENODE>/repos/os/src/server/tz_vmm/include/block_driver.h [3] https://genode.org/documentation/genode-foundations-21-05.pdf 8.8.4. ID space [4] grep -r "ID space" <GENODE>/doc/ [5] <GENODE>/repos/os/src/lib/vfs/fs_file_system.h [6] <GENODE>/repos/os/src/drivers/gpu/intel/main.cc
On 20.04.22 00:42, Sid Agrawal wrote:
Hi Genode, I am building userspace on seL4 directly and have run into a design issue. I am implementing server and client using badged endpoints. I think Genode would have run into the same issue, and I would like to understand better how Genode solves it. It is not directly a Genode question, but I would benefit from your experience. Below I have laid out the scenario, the issue, and some questions.
_Scenario_
I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knowswhich object the client is trying to manipulate.
The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object.
_Issue_
I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and givethe badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has noway to look up the badge of the second cap, it cannot look up the underlying object for obj_T2.
So my questions are:
Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask.
Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it?
As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why.
Thanks for the help, everyone!
Thanks, Sid Graduate Student @ UBC sid-agrawal.ca http://sid-agrawal.ca
Genode users mailing list users@lists.genode.org https://lists.genode.org/listinfo/users
Genode users mailing list users@lists.genode.org https://lists.genode.org/listinfo/users
Hello Sid,
are your aware of the article series about "Genode on seL4" [1]? Especially the section about "Translation of capabilities aka unwrapping" [2] may be of interest to you.
[1] https://genode.org/documentation/articles/index [2] https://genode.org/documentation/articles/sel4_part_2#Translation_of_capabil...
Regards
Hallo,
the issue was discussed in 2014 on the se14 mailing list:
https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/I3AYF2A...
We worked around it by associating a system-globally unique ID value with each object, using this value as badge, and sharing it with the client. Upon calling the server, the client supplies this value along with the actual capability. At the server side, the (potentially forged) value serves as a hint that allows the server to look up the object and compare the value with the real badge of the addressed object.
This approach maintains the notion of capabilities being unforgeable on se14. However, since globally unique IDs are shared with the client, the approach is in principle prone to covert information flow - by the means of ID allocation influenced by two conspiring components.
As far as I know, this use case remained unaddressed by se14. But I have admittedly not followed recent developments.
Genode's custom base-hw kernel supports this use case.
Norman
Hi Norm
On Mon, Apr 25, 2022 at 2:34 AM Norman Feske norman.feske@genode-labs.com wrote:
[CAUTION: Non-UBC Email]
Hallo,
the issue was discussed in 2014 on the se14 mailing list:
https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/I3AYF2A...
Thanks. This is such a Deja Vu. I have not read the entire post, but I
feel like it will answer my questions.
We worked around it by associating a system-globally unique ID value with each object, using this value as badge, and sharing it with the client. Upon calling the server, the client supplies this value along with the actual capability. At the server side, the (potentially forged) value serves as a hint that allows the server to look up the object and compare the value with the real badge of the addressed object.
This approach maintains the notion of capabilities being unforgeable on se14. However, since globally unique IDs are shared with the client, the approach is in principle prone to covert information flow - by the means of ID allocation influenced by two conspiring components.
This lines up precisely with my understanding from reading the Genode code.
The crux of it being - "*using this value as badge, and sharing it with the client".*
I also completely agree with the security pitfalls you mentioned. Quite exciting to know that I am on the right track in terms of using and hitting the limits of the seL4 API. I will read up the exchange and follow up if needed.
Thanks a ton!!
Sid
As far as I know, this use case remained unaddressed by se14. But I have admittedly not followed recent developments.
Genode's custom base-hw kernel supports this use case.
Norman
-- Dr.-Ing. Norman Feske Genode Labs
https://www.genode-labs.com · https://genode.org
Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Genode users mailing list users@lists.genode.org https://lists.genode.org/listinfo/users
are your aware of the article series about "Genode on seL4" [1]? Especially the section about "Translation of capabilities aka unwrapping" [2] may be of interest to you.
Hi Christian,
Thanks for sharing this. I did look at this article and the note about unwrapping. But unwrapping only works for the endpoint over which the message was received if that cap was in extraCaps. It does not work for all caps all caps in extraCaps.
[1] https://genode.org/documentation/articles/index
[2] https://genode.org/documentation/articles/sel4_part_2#Translation_of_capabil...
Regards
Christian Helmuth Genode Labs
https://www.genode-labs.com/ · https://genode.org/ https://twitter.com/GenodeLabs · https://genodians.org/
Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Genode users mailing list users@lists.genode.org https://lists.genode.org/listinfo/users
-
Christian Helmuth -
Martin Stein -
Norman Feske -
Sid Agrawal