I am attempting to prototype an seL4 based system that ideally will have 
multiple threads, each with their own CSpaces which are each a tree e.g. not 
rooted in the initial cnode. My strategy here is to 1. chain new cnodes off of 
the initial cnode in the initial thread, and 2. Create a new thread TCB etc., 
revoke the initial cnode caps and set the new cnode cap as it’s own cnode root 
in that new thread. I have run into some issues at step 1 and am writing to ask 
if this is a viable strategy. 

 

Perhaps I am misunderstanding something but chaining in this way does not seem 
possible if all 32 bits are to be resolved in searching the initial cnode, so I 
am not certain if this strategy will work. Is it possible to configure the 
initial cnode guard to be something other than 32 bits? I have searched through 
the config of the kernel and cannot find some easily changed parameter for 
compile time, and for runtime I have tried to use the TCB_SetSpace and 
TCB_Configure on the initial thread to change the guard but this has lead to 
other problems. If I set it to something like 16, does this mean that all of 
the slot indices in the bootinfo struct are no longer valid as being set at 
0x0, 0x1, etc and now will be at half word indices? It is very unclear to me 
from the documentation how this works but perhaps I am missing something. 
Setting it to something like 4 leads to an explicit TCB illegal operation and 
something larger like 19 returns seL4_Error 3 illegal op when I try to create 
new cnodes via untyped_retype from the init cnode. 

 

Is there something obvious that I am missing? I wonder if this is even 
possible—having cnodes not rooted in the initial cnode. Or if it is possible, 
is there some other mechanism to create a new cnode that is not rooted in the 
initial cnode? It is also probably important to note that due to constraints I 
am not able to use any of the nice sel4_libs provided to help with this.

 

Thanks very much in advance for any help.

 

 

Alexandra Clifford, MS

05-53 Secure Resilient Systems and Technology

MIT Lincoln Laboratory

244 Wood st., Lexington MA 02421

Email: [email protected]

 

Attachment: smime.p7s
Description: S/MIME cryptographic signature

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to