seL4 Micro-Kernel Working Towards A General-Purpose, Multi-Server OS

[ayumu]

will it save you from browser vulnerability? will you formally verify your browser?

No, but the capability mechanisms in seL4 would allow the browser to be really well isolated from the rest of the system. These facilities could also be leveraged internally by the browser itself, to better sandbox its own components.

[mdedetrich]

Here let me translate that for you:


Doesn't sound so impressive now does it?

While TDD is something we should all strive for, touting it as your main selling point... just isn't that impressive unless you're running a DOD contract writing software to run aircraft engines or something. As others are being quick to point out it doesn't mean jack shit for typical server or desktop usage scenarios.

This has nothing to do with TDD. seL4 is a mathematically formally verified kernel (see https://docs.sel4.systems/projects/s...20is%20correct.). The formal proof for sel4 is written in Isabelle/HOL and iirc some specifications are written in Haskell.

[pabloski]

all you have to do to get rid of this "misconception" is to provide microkernel, abi-compatible with linux, running just as fast. what was stopping you all those years?

They did just this with L4linux and it was faster than stock Linux!!!

I repeat, you people are living in the past. You have no clue at all of the improvements in the microkernel space. Did you know that a bunch of Android OEMs run Android virtualized on top of seL4????

[pabloski]

When it comes to Minix 3, especially when compared to seL4, it's not a misconception. Minix3 has some interesting overall design decisions in user space, but seL4 is by far the better kernel. I'd be down for a port of the Minix3 userspace to seL4 (yes, I am aware this is a lot of work because of the different ideas of just how micro the kernel should be).

I agree. Let's not forget that Minix was born to teach OSdev. seL4 has been built to be used in the wild. Also, L4 has changed the way microkernels work. No more IPC everywhere, but page sharing between process boundaries. Definitely a revolution, giving us a bing performance boost.

[pal666]

Will using synthetic oil in your car engine prevent your muffler from rusting out?

Obviously having fewer kernel bugs doesn't solve all problems in other system components, but that doesn't mean that it's not worthwhile to use a kernel with fewer bugs.

obviously any approach is not worthwhile unless it's scalable

[pal666]

If a microkernel is ABI-compatible with the Linux kernel, then by definition it isn't actually a microkernel.

i'm pretty sure "micro" part refers to implementation rather than interface

[pal666]

No, but the capability mechanisms in seL4 would allow the browser to be really well isolated from the rest of the system.

for most people browser is the system. it contains all your passwords, all your credit card numbers etc. and i wasn't even thinking about chromeos

[pal666]

They did just this with L4linux and it was faster than stock Linux!!!

l4linux is monolithic linux running on hypervisor, it isn't more secure than plain linux. btw, can you share benchmark of some modern game on l4linux?

I repeat, you people are living in the past. You have no clue at all of the improvements in the microkernel space.

well you have no clue what you are talking about(see first part of this post)

[Nemerian]

Wasn't Genode OS used with L4?

[pabloski]

l4linux is monolithic linux running on hypervisor

Yes and it is faster than Linux, even in the face of the hypeolithic linux runnrvisor overhead!!

can you share benchmark of some modern game on l4linux?

Games are programs. If business/office/utility programs go fast, games will go fast too!

well you have no clue what you are talking about(see first part of this post)

Because asking about games benchmarks means having a clue!?! Ok God!

Also, what part of my last post don't you answer? A lot of mobile phones run on L4 + Android on top!!! And they are damn fast. Some of them even compartmentalize Android subsystems under isolated virtual machines. And they are damn fast!!