> arbitrary service graph
This makes alot of sense. While I am not intricately intimate with the SeL4 codebase, this would be a similarity. For example, if you do not share permissions when creating a SeL4 thread it will NEVER be able to communicate or share with its creator (aside from side-channel timing attacks, which is the next big validation target, but requires CPUs to have better concepts of time, and there is a new RISC-V instruction they are recommending)
Do you have to check the memory mappings/permissions are a subset every time you change turfs, or is there some way this is cached with some privledged calls (privledge by the graph, and not levels or flat, as you say)?