For example, Microsoft's Gazelle and Illinois Browser OS build their browsers based on a secure kernel, so why no (se)L4 microkernel/hypervisor based browser? I haven't even seen the idea. Besides, there is only old information about secure kernel/OS-based browsers in the first place, and nothing current and up-to-date. Perhaps it has failed?
I thought the IBOS kernel leveraged L4 (Pistachio?)
I believe generally the push has been to better use the isolation feature in existing operating system environments - such as having separate processes for rendering and javascript execution per origin which also have unique sandboxed storage. From a platform vendor as browser vendor perspective, building what amounts to a new operating system running at the hypervisor layer is a huge effort that amounts to them now having one more internal OS to secure.
So I would instead expect this to be more of a research platform task, like perhaps something you would see on Genode.
The markets primarily want speed, compatibility, ease of view, and ease of deployment. They also want security if they can get that too. They will not pay for security in most cases. OSS developers work on what is fun to them which is usually the new design more than porting every bit of legacy code to the new design. Solutions usually must fit into these constraints.
Secure browsers cost a lot to develop. Developers needed to add security in a way that didn’t compromise any of the things that users carry about the most. Instead, they’d be making changes to browsers that ran on typical, operating systems. Expensive ports of browsers to separation kernels remain an academic curiosity.
The other issue is momentum. The highest assurance security community was focused on separation kernels that ran a combination of virtual machines and isolated apps. All open source and commercial efforts begin to run browsers inside VM’s’s. New projects followed suit. Here’s an example of that type of architecture:
Bromium aka HP Sure Click is based on Xen. I’d argue Xen provides comparable security, along with nice to have features such as multi processor support.
sel4 is more suited for tasks with very limited but also very sensitive functionality. For example, something like a secure element.
Technically, you _can_ add rich OS functionality (such as GUI) on top of sel4 but development will be slow and painful and the performance will be bad. And when done you haven't really improved security that much since most your assets are now outside the tiny kernel.
I believe generally the push has been to better use the isolation feature in existing operating system environments - such as having separate processes for rendering and javascript execution per origin which also have unique sandboxed storage. From a platform vendor as browser vendor perspective, building what amounts to a new operating system running at the hypervisor layer is a huge effort that amounts to them now having one more internal OS to secure.
So I would instead expect this to be more of a research platform task, like perhaps something you would see on Genode.