"Running seL4 in any way other than on bare metal makes no sense whatsoever." There are scenarios where it makes sense. The power of seL4 is isolation guarantee. That is, software running virtualized on top of seL4 can't escape from seL4. This means it can be used to safely run a web browser (virtualized) in a standard OS. A browser is only exposed to external threats, that come from the Internet, they reach the host tcp/ip stack and then the browser. Here an attacker can exploit an OS flaw (in this scenario, the tcp/ip stack) or can exploit a browser flaw. What attackers are doing now is to exploit browsers, not tcp/ip. Why? Any bug hunter knows the answer: it's, by far, much easier to find (and succesfully weaponize) bugs in browsers! So, what vendors have been trying is to "virtualize" (really just sandboxing) browsers (very inefective as they rely on OS own mechanisms, which are not always available or robust), or running cloud browsers, which is painful, not user friendly, and expensive... A solution better than that would be to run the browser virtualized on seL4. You don't solve the host tcp/ip stack surface attack, nor the "glue" software surface attack required to run seL4 virtualized, but, again, any bug hunter would always prefer the scenario of exploiting a browser than being forced to exploit the tcp/ip stack or "glue" software. Exploitation is a matter of stats. That is the scenario I'm talking about. El jue., 18 abr. 2024 13:14, Gernot Heiser via Devel <devel@sel4.systems> escribió:
On 18 Apr 2024, at 20:38, Hugo V.C. <skydivebcn@gmail.com> wrote:
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 don’t think I understand. Running seL4 in any way other than on bare metal makes no sense whatsoever.
Gernot _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems