I've only briefly heard of that kernel, and I suspect the same is true for many people at HN. It's also been open sourced pretty recently so maybe it needs more time for people to become aware of it. It may catch on if we give it more time. But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have. I was thinking of a kernel written entirely in Rust, and that would be not only much more reliable, because it would have far fewer segfaults and the like, plus be more immune to the types of highly publicized security flaws lately (Heartbleed, etc.). Of course, the whole OS might have to be written in Rust + memory safe languages. So we might be a ways off from the ideal goal, but clear I was thinking that we can start with a Rust kernel and build on top of that.
SEL4 is provably free of segfaults, without any runtime overhead at all. Unlike Rust. Though it took considerable development time overhead to achieve that.
(Moreover, rust itself may have bugs, or there could be bugs in unsafe code in the standard library. The amount of trusted infrastructure is much smaller for SEL4, I suppose if you compile it with compcert, I imagine it's quite small)
The worst case latency is also part of the proof for SEL4-- which is a kind of correctness you cannot achieve via rust (even ignoring overhead).
There are many elements of program correctness beyond memory safety. The developers of rust generally eschewed concerns about other kinds of correctness. For example, your integer types may overflow and your algorithms could fail to work as a result. SEL4's proofs show the operation of the software match its specifications completely (given some assumptions), it's really far far beyond the memory safety promises of rust.
If it took a huge development effort for SEL4 to get to the state it is currently in, doesn't that make it unlikely anyone can easier go in and change thinks or add features? Not knowing too much about SEL4, but it just seems like a very limited kernel, meant primary for embedded devices, and that's about it. It doesn't seem to have the feature you expect from kernels these days.
A Rust based kernel could be a *nix, and do everything from desktops to server. It would be developer friendly in the same way Linux or Windows is. Plus, the baseline safety would be much higher with a Rust based kernel, without having to formally proven everything.
It's a microkernel: it is intentionally minimal. Microkernel operating system design is from the 1980s is different from the monolithic, bulky and older operating systems designs you are used to (famously including Linux, see the Tanenbaum-Torvalds debate). It has all the features that it would likely ever need already.
Instead of having all the services required for an operating system in the kernel, the kernel just implements the bare minimum including fast IPC. Things that traditionally are implemented in the kernel (filesystems, device drivers, other modules, etc) are all implemented as services living in userland and are assigned the minimum necessary additional permissions for them to perform their task.
You can build a *nix like system on top of seL4. You can even run Linux itself on top of seL4, with L4 acting as a hypervisor.
An operating system doesn't consist of just the kernel.
>If it took a huge development effort for SEL4 to get to the state it is currently in, doesn't that make it unlikely anyone can easier go in and change thinks or add features?
No. Most of the huge development was in developing proofs for C. The developers now find that development is easier than just using C directly. The process is to write it in a high level specification language, then when you're done messing around and know you have it how you want it, translate it to C by hand and the proofs will tell you that you did it right (or wrong).
>It doesn't seem to have the feature you expect from kernels these days.
It has exactly the features we expect from kernels these days. The features we do not expect from kernels these days but did expect from them 30 years ago are available in a library where they belong.
>A Rust based kernel could be a *nix
So can any L4. Why would "start from absolutely nothing" be easier than "start from an existing microkernel"?
Perhaps not, but in a kernel you'd have plenty of your own unsafe code.
SEL4 doesn't.
There are, of course, people thinking about bridging the worlds of formally provable correctness and Rust, e.g. https://github.com/rust-lang/rust/issues/18496 though extraction based is likely to not produce the most elegant or efficient code... and I assume the along-the-side proofs like SEL4 uses would be harder for Rust because the language is more complex than C.
>But even so, it's still mostly written in C and likely have many of the same pitfalls that all kernels written in C will have
No it won't, that's the point. It is a much stronger guarantee of being without those bugs than using rust would provide.
>because it would have far fewer segfaults and the like
SEL4 can not segfault, that's the point. It isn't fewer, it is zero.
>but clear I was thinking that we can start with a Rust kernel and build on top of that.
Yes, and I am saying if people actually wanted that, they could start with a formally verified kernel that already exists and build on top of that. But they don't.
