Hacker News new | ask | show | jobs
by wyager 3525 days ago
SeL4 is an indicator of things to come. We can build complicated OSs with extreme reliability; the up-front cost is just higher than most companies are willing to spend right now, because customers don't yet realize that it's technically possible to avoid the huge costs associated with software failure in exchange for slightly higher amortized software costs.
3 comments
johncolanduoni 3525 days ago
Until we have a way to extend seL4 or something like it to full multiprocessor operation (without the multiple kernels with separate resources limitation that is currently the only way to use multiple processors with seL4) I'd disagree that we can build general-purpose OSes with verification. Our techniques for verifying concurrent programs are still very primitive and cumbersome, and I don't think many would take an OS where processes can't use multiple hardware threads seriously.

Also, seL4 (being a microkernel) leaves out a huge swath of kernel-level facilities that need to be implemented with the same standard of verification (resource management, network stack, drivers, etc.). Running on a verified microkernel provides a great foundation, but these still add a ton of code that needs to be verified. Plus the concurrency problem will strike again at this level.

link
tptacek 3525 days ago
L4 is incredibly simple. It is essentially (a word I chose carefully) the opposite of a complicated OS. It also doesn't really do anything.

If you have just a few extremely simple applications you'd like to run in an enclave, L4 is a good way to minimize the surface area between the applications themselves and the hardware.

If you'd like to host a complicated operating system on the simplest possible hosting layer: again, L4 is your huckleberry.

Otherwise: not so useful.

Note that if you just host XNU on top of L4, you might rule out a very small class of bugs, but the overwhelming majority of XNU bugs are contained entirely in the XNU layer itself; having XNU running on an adaptor layer doesn't do much to secure it.

link
duaneb 3525 days ago
I don't think I've ever seen a complicated OS based on SeL4, and it is the opposite of complicated itself.

I don't think SeL4 means much for macOS/iOS.

link