Hacker News Reader

Comment by Hypx | Hacker News Reader

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.

View on HN

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"?

Rust is able to be almost (unsafe blocks) free of segfaults without runtime overhead. That's the core feature that Rust provides with lifetimes.

The Rust compiler can (and does) have bugs, but they get weeded out over time. But so can whatever proof system or proof checker is used on SEL4.

As for integer overflow, yeah...that's a hard problem with Rust, and unfortunately, unlikely to be fixed.

Aren't bounds checks and unwinding examples of non-free safety code in Rust?

Unwinding is only potentially unsafe if you're already using `unsafe` blocks. If you're sticking to safe Rust, unwinding can't cause memory unsafety.

You can largely eliminate bounds checks by using iterators.

> there could be bugs in unsafe code in the standard library

For any embedded work or kernels, you wouldn't be pulling in the standard library via a `#![no_std]` attribute.

But you're right that bugs in the compiler could produce safety issues.

> any embedded work or kernels

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.

Hasn't code for L4 been available for, like, a very long time? SEL4 is a variant of L4, and not (IIRC) the best-known.

L4 is fantastic, by the way.

>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.

Reply on news.ycombinator.com