Hacker News Reader

Comment by nullc | Hacker News Reader

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.

View on HN

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.

Reply on news.ycombinator.com