
"All this is a matter for user mode. "
Well... in seL4. In standard OSs (Windows, Linux...) this is a matter of
kernel mode. And here is the party. Of course if you use seL4 as TCB then
you can partition whatever you want on top.
The challenge that I probably didn't expressed correctly, is to integrate
seL4 on top of other dynamic systems (in example to virtualize a browser),
as seL4 needs to know in advance how much memory will have available...
Running seL4 on bare metal is a "kids game" (don't want to offend anyone),
the challenge is to integrate it on systems where resources are dynamically
assigned.
I think we are thinking about different threat models Gernot, I'm looking
to isolate what comes from the outside World (Internet) from inside World
(standard OS). I think you are talking about seL4 managing all the systems
resources, as a TCB. Absolutely different stuff.
El jue, 18 abr 2024 a las 11:36, Gernot Heiser via Devel
(
On 18 Apr 2024, at 19:18, Hugo V.C.
wrote: "A web browser is a good example of this. The number of security domains is at least the number of origins in use, which can be extremely large. Furthermore, some origins might be CPU-intensive."
Yes. That's the challenge when you try to use a solution aimed to static systems for dynamic systems... Not sure how other will solve this,
Operating systems have been dealing with this kind of problem for well over half a century, it’s called the working-set model.
You may have 1000s of processes, but very few are active during a time window, and you allocate the resources to them.
Remember what virtual memory was originally introduced for? Allowing program memories to exceed the size of physical memory.
All this is a matter for user mode. The microkernel’s job is to do the things usermode cannot.
Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems