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