"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 (<devel@sel4.systems>) escribió: > On 18 Apr 2024, at 19:18, Hugo V.C. <skydive...@gmail.com> 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 > _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
