[tonyhb]

Spent a while on the weekend reading about the seL4 kernel, which uses capability based security and has end to end mathematical proofs of correctness on the compiler and underlying kernel. Its predecessors are used in Apple's A7 and Qualcomm's chips.

Watching https://www.youtube.com/watch?v=lRndE7rSXiI and it says that it's mathematically impossible for seL4 to suffer from things such as buffer overflows.

I'm faaaaaar out of my field here... but this sounds as like a far better improvement in security compared to running things in a chroot. Apart from it being really new (there's just a kernel with a C compiler), would this be a good route to head down for improving security? Why aren't we writing a linux port on this?

Kernel info here: http://en.wikipedia.org/wiki/L4_microkernel_family#High_assu...

[johnny22]

Here's an approach being tried for desktop apps: https://blogs.gnome.org/alexl/2015/02/17/first-fully-sandbox...

[fizgig]

That's cool.

I've toyed with PC-BSD, which has a per-application jail setup function called Warden. FreeBSD jails are supposedly a more secure version of standard chroot (which historically was pretty easy to break out of). I have always wondered about the vulnerability of X-Windows in the PC-BSD context, and if an untrusted jailed app could cause grief on the main desktop via X.

It's nice to see more stuff like this being experimented on. I recall reading about a similar Windows thing some time ago (Sandboxy?), but the concept never seemed to go mainstream for some reason.