[seL4] Does the CSpace needs to have a cap to the TCB

Hi, We roughly do the following steps when setting up a new process in seL4: - Allocate a new TCB - Allocate new CSpace - Make the TCB point to the CSpace - Construct the VSpace and add the relevant caps in the new CSpace - Update the VSpace cap in the TCB. - Add a copy of the TCB cap in the new CSpace.

(I am looking at the process spawn function in libesel4utils at: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/src/process.c#L49...)

My question is about the last point i.e. copying of TCB to the new CSpace.

If I want to restrict the new domain from changing its VSpace, suspend itself, and change its fault handlers, I would simply not do the last step. Will that work?

Is there any fundamental need for the TCB cap to be in the cspace it points to?

Thanks, Sidhartha Agrawal