[seL4] Re: Question about LionsOS

"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 () escribió:

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