Hello.
There have been many interesting points, but it was a strawman fallacy to
suggest Hugo accused "all the volunteers" of being unethical.
I think Hugo has a salient point when he says a world of bespoke seL4
images for every application is a distant one. I share the feeling that a
hybrid, intermediate step is meaningful. I also echo the idea that
exploitation at scale is a matter of statistics.
Even if virtualizing the seL4 undermines its security properties, it is
still a fast and correct microkernel. Putting a usable seL4 image in the
hands of enthusiasts, budding developers, or even seasoned developers would
be a boost to the ecosystem.
One reason Linux is so popular is that you can use Linux to develop Linux.
I would be thrilled to boot any meaningful home or development environment
on top of the seL4. I would never stop talking about it.
Cheers,
Michael
On Fri, Apr 19, 2024, 5:05 AM Indan Zupancic
Hello Hugo,
On 2024-04-19 10:06, Hugo V.C. wrote:
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.
Both Chromium and Firefox are open-source. Calling Mozilla and all the volunteers unethical is unkind. Nothing is stopping you and like minded people from forking and creating a version which is more secure.
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)
This doesn't solve the problem of insecurity on the browser side, it at best helps to contain the damage if a browser process is compromised.
But it only contains damage towards the OS side, not towards the user. Considering how much is done in browsers nowadays, an attacker is pretty much done if they have the same information and access as the browser has.
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.
Of course adding another layer of indirection makes live harder for attackers. Following this line of through, why stop with one nested virtual machine, why not keep going? You could nest Linux on top of seL4 on top of Linux.
On the other hand, it makes everything more complex and that will give more attack vectors in itself.
Using an seL4 guest OS instead of a Linux guest OS can only stop attacks that rely on weaknesses in the host OS that can be exploited by guest kernels, but not from (guest) user space.
You can achieve the same level of security by disallowing most of the browser code from making system calls and not using any virtualisation at all.
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.
But the same is true if a browser runs as a separate user, if it is compromised it is contained to what permissions it has, which can be very little. With your solution you just need to do it twice instead of once. Security wise, having to do the same thing twice isn't really more secure than having to do it once.
Greetings,
Indan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems