Slashdot Mirror

There are technical reasons also. Android under the Linux kernel does sandboxing by giving each app its own user, which I find to be a bit of a kludge.

Fuchsia's microkernel Zircon (nee Magenta) instead uses capability-based security, in a model where Processes live in Jobs and Jobs can be nested, allowing the ones that are deeper nested having lesser privileges.
However, Zircon has a major flaw: capabilities can not be revoked, other than by killing the whole process, or jobs.
If I had been in charge, I would have instead chosen seL4, which has revocation, is stable on ARM and which has a formal proof of correctness (was it ten or twenty man-years of work just for the proof? I forget).
But, yeah... seL4 is licensed under GPL. ;-P

Ah, but Enterprise IT wants to be certain their more technically-inclined lusers can't disable the enterprise's ability to "manage" and "audit" the systems they manage. It's literally one of the selling points touted by Intel (and AMD for their equivalent of ME) until recently.

It's not like the machines Enterprise IT buys are any different from the ones I can buy as a consumer, and bulk buyers have a hell of a lot more sway than individual consumers.

Honestly, if you want secure, you gotta use ARM these days. ARM has been formally/mathmatically verified, and there's even a formally verified microkernel.

So we can all cheaply run a Raspberry Pi 3 and get a formally verified hardware and software stack. Or a BeagleBone... or whatever ARM system you want to use.

Sure, there aren't any servers, or even device drivers. It's been decades of work, but you too can have an idle loop that is provably bug-free in both hardware and software!

Ah, but Enterprise IT wants to be certain their more technically-inclined lusers can't disable the enterprise's ability to "manage" and "audit" the systems they manage. It's literally one of the selling points touted by Intel (and AMD for their equivalent of ME) until recently.

It's not like the machines Enterprise IT buys are any different from the ones I can buy as a consumer, and bulk buyers have a hell of a lot more sway than individual consumers.

Honestly, if you want secure, you gotta use ARM these days. ARM has been formally/mathmatically verified, and there's even a formally verified microkernel.

So we can all cheaply run a Raspberry Pi 3 and get a formally verified hardware and software stack. Or a BeagleBone... or whatever ARM system you want to use.

Sure, there aren't any servers, or even device drivers. It's been decades of work, but you too can have an idle loop that is provably bug-free in both hardware and software!

(Disclaimer: I had my fingers in that pie.)

I think some people have tried to prove that it's not possible to prove the correctness of a non-trivial OS.

It's been done. You can get a fully verified OS. Incidentally, they didn't trust the compiler, so they also formally verified the assembly output.

It is possible if you have the resources, have a look at seL4 a verified microkernel.

> And provably correct code is still a pipe dream.

http://sel4.systems/

http://sel4.systems/FAQ/

Is it really that hard to give more background information?