The existing code does not implement the below policy. If it did, it would not loop across all modules provided, create a region consisting of the concatenation of all module contents and mapping them into the root server (with no direct means of knowing how many were provided or where they are located). One could argue that the code is less secure because one can inject code into the root server at run-time that has never been analyzed. Since the loader is doing most of the work, I think size isn't very relevant here. This said, it's your code. I hope dynamic systems aare in important application of seL4. Dave Just to confirm what has already been stated: while it would be possible for seL4 to load multiple images, however this is incongruent with L4 philosophy. We want to keep the kernel as small as possible to minimise the trusted computing base and maximise policy freedom. The root task can act as a loader to load multiple images according to whatever policies suit the system. One example loader we have is the capdl loader (https://github.com/seL4/capdl) which can load capabilities and set up processes based on a specification. Camkes (https://docs.sel4.systems/CAmkES/) can be used to initialise such specifications. We're working on improving our documentation and tools for setting up seL4 systems, so keep an eye out in the coming year.