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/I3AYF2AMRIRAMTCBMRENP7TVTH6RDCJQ/

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