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