Hi list, Here is a question about capability derivation trees, in particular when it comes to seL4_CNode_Copy and seL4_CNode_Mint. Suppose I have an untyped cap Untyped0, and I create a page cap by retyping Untyped0 into Frame0 (with seL4_AllRights). I then call CNode_Mint to mint Frame0 into Frame1 with restricted rights (say read-only). Finally, I call CNode_Copy to copy Frame1 into Frame2. What would the capability derivation tree look like at the end? Case 1: |--------| |Untyped0| |--------| / | \ / | \ / | \ |------| |------| |------| |Frame0| |Frame1| |Frame2| |------| |------| |------| Case 2: |--------| |Untyped0| |--------| | |------| |Frame0| |------| | |------| |Frame1| |------| | |------| |Frame2| |------| Case 3: |--------| |Untyped0| |--------| | |------| |Frame0| |------| / \ / \ |------| |------| |Frame1| |Frame2| |------| |------| Which one of the above is the correct answer? I suspect it's case 3, but I'm not sure. Best, Chang