Hello Sid, I am an seL4 enthusiast. I'm not sure what the best practice is for this situation, so hopefully someone more knowledgeable will chime in. I'm certain the underlying issue here has been researched before as previous capability systems have used the badging mechanism that seL4 uses. For example, in coyotos this was called a "protected payload". I'm not sure what "PD" means, I'm assuming from context that you mean "process".
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.
By design, there is no way to ask the kernel what the badge value is for a capability. The creator of the endpoint is assured that this badge value can never be seen or modified by anyone who receives a badged cap to the endpoint. In this way, the creator of the endpoint can use the badge to store secrets, such as permission bits or object type.
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?
Yes. This mechanism allows you to use a single endpoint for multiple purposes, so a server only needs to use one. This is convenient since seL4 does not have a "select" mechanism to wait on multiple endpoints. You might consider storing an array index instead of a pointer to get more room for other bits you may want to store here. Alternatively, you might use any unused low bits of the pointer (due to object size and alignment) to store the object type.
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.
I also don't think this is a good idea. I think this friction may be an indication that a different design might work better. Can you expand on what motivated you to use multiple threads in a single process to wait on multiple endpoints, instead of just using a single endpoint? -JB