[seL4] Re: Question about LionsOS

"running seL4 in a virtualized environment makes a huge amount of sense for testing and debugging, or if one is shipping a virtual appliance." or running on top of any other standard OS... Those are latest news (April 17th): "*Google and Mozilla on Tuesday announced security updates that address more than 35 vulnerabilities in their browsers, including a dozen high-severity flaws.*" https://www.securityweek.com/chrome-124-firefox-125-patch-high-severity-vuln... I'm not sure if people understands what is the scenario right now. This is a Circus. Browsers are pathetic in terms of security. Too complex, too big, too much JIT... too much interaction with Internet. The worst ever scenario we could figure out, and this only gets worse every year as, instead of simplifying the protocols we use for Internet, we make them more complex (aka "more features"). So: 1) Let's forget the naive idea of users changing behavior or vendors making secure software. Users are "ignorant" and vendors are unethical. That's raw reality. 2) Let's forget about users using (wonderful) secure platforms (like QubesOS) or... ups..., looks there's nothing else, as seL4 is aimed for embedded world (right now) 3) Let's try to build solutions, far from perfect, but that improve (current) real requirements security. In example, using seL4 integrated on other (insecure) platforms. The magic of seL4 is correctness. Anyway, this does not magically solves the Universe problems. But keeps being correct. There's no engineering limitation that avoids running seL4 on top of any other OS using virtualization functionality. And besides unfounded non engineering based facts, the reality is that an attacker will almost ALWAYS (exceptions are exceptions by definition) prefer a scenarios where seL4 is not present to the same scenario where seL4 is there. If anyone can prove I'm wrong here, please correct me. So, my proposal, is, of course, let's fight to try putting seL4 as close as possible to the silicon and anywhere if possible, but... if not possible, let's fight so put it somewhere else! In example: we have a scenario with Host OS (with nested virtualization enabled) ==> hypervisor XYZ ==> XYZ OS layer ==> Clown Buggy Browser we can convert this to: Host OS (with nested virtualization enabled) ==> seL4 ==> XYZ OS layer ==> Clown Buggy Browser As simple as this. In the last scenario is, by far, more complex (need to exploit drivers, tcp/ip stack, "glue" software) to jump from "Clown Buggy Browser" to "Host OS". And that's enough for me. Moreover, in the last scenario, I can have: Host OS (with nested virtualization enabled) ==> seL4 | ==> XYZ OS layer ==> Clown Buggy Browser (Work) | ==> ABC OS layer ==> Clown Buggy Browser (Fun) | ==> ABC OS layer ==> Clown Buggy RandomTrendyApp Does it sound familiar to you guys...? And yes, I obviously prefer Mediterranean food and: MyPerfectSilicon (RISCV) ==> seL4 ==> Native seL4 Code == > Clown Buggy Browser/App But this is not going to happen in the short term, so, meanwhile, I think that it is not crazy to find half-way solutions to just be able to survive this era. El jue., 18 abr. 2024 21:51, Demi Marie Obenour escribió:

...

On 18 Apr 2024, at 20:38, Hugo V.C. 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

On 4/18/24 07:12, Gernot Heiser via Devel wrote: metal makes no sense whatsoever.

...

Gernot

I think the point is that if a system needs dynamic resource allocation, _something_ needs to do it. Traditional systems do this in the kernel. seL4 declares this to be the responsibility of userspace, but I’m not aware of a userspace component that can actually do that job.

Also, running seL4 in a virtualized environment makes a huge amount of sense for testing and debugging, or if one is shipping a virtual appliance. -- Sincerely, Demi Marie Obenour (she/her/hers)

_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems