Seccomp has strict mode, which allows you to say to the kernel "from this point on, allow me to only do read, write (to fd's I already have opened), _exit and sigreturn, otherwise kill the program". It's not perfect, but it reduces the vunrel space a lot.
You can also do a lot more fancy stuff, using the seccomp BPF interface (which I'm totally not writing a Haskell DSL for right now :D)
"Keyboard would get stu" is just brilliant.
Otherwise, what is claimed sounds very impressive, so much that I really wonder "what's the catch? There must be some."
> Otherwise, what is claimed sounds very impressive, so
> much that I really wonder "what's the catch? There must
> be some."
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...
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.
"The kernel was written from scratch"
"shares no code with the Linux kernel"
It's not Linux, just Linux compatible. So I guess the author can apply any license they fancy.
Those advances are mostly from the Dresden OS folks, and the NICTA group (which went on to make one of Qualcomm's best kernels, OKL4).
seL4 was an attempt to convert the API and specification for the L4 kernel into an executable format (using Haskell) and confirm the specification was solid. The system was then extended to actually test the L4 kernel itself.
In the most recent versions, you can run entire device drivers and OS layers under the capability management system. One only needs to look at the Genode tooling (which is the logical continuation of the work started in DRoPS): http://genode.org/documentation/general-overview/index
Genode, Fiasco.OC, L4 (including seL4), and the work on secure GUIs all deserve to be far more popular than they are.