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.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
