SB might listen for a "verify" request on its endpoint.

Servers could invoke their own, privately-held spacebank capability and ask it to verify the unknown capability passed by the untrusted client, by sending it as part of IPC.

During IPC seL4 will unwrap any sent capabilities into their badge value if the capability being sent was badged from the endpoint being invoked.

In this way, if SB receives the badge value for a sent capability on the verify api request, it knows the capability was badged from its own endpoint, and can return a "verified" response to the caller.

See section 4.2.2 in the manual for details.

- JB

I have a server process SB that issues badged endpoints to users.  Clients can invoke the endpoints to access memory and possibly other resources.  Essentially, it is a version of Robigalia’s space bank.  Other programs pass endpoints issued by SB to provide servers the resources needed to do their tasks, and the servers invoke the endpoints to obtain memory that they know cannot be revoked or modified by other programs.

SB is part of the TCB, and is trusted by all of its clients.  Clients, however, do not trust each other, and may pass forged endpoints to servers to cause servers to misbehave.  Therefore, servers need to be able to ask SB if a given capability was actually issued by SB.

SB can make that check by checking that the endpoint is a badged version of its master endpoint, which it never gives anyone else access to.  What is the correct API function for doing this?

Sincerely,

Demi M. Obenour

_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel