Hacker News Reader

Comment by sophacles | Hacker News Reader

> I like Rust, but I don't understand why "OS written in [language]" is a compelling goal within itself.

There's a few good reasons in my mind:

* proof of concept - if a language claims to be a systems language, being able to point to an OS in it is pretty good proof that it's true.

* dogfooding - if there are problems with how the language works for the OS case, they can be highlighted by the OS. (this is similar to self hosting a compiler)

* community building - some folks want to work on a new OS, and doing it in a specific language helps grow both groups and at least introduces them to each other.

View on HN

Maybe but this is at the cost of worst design..

For me the 'logical' thing to do to build a 'safety first' OS in the 21st century would be: use the seL4 microkernel and then Rust to build the full OS kernel.

Though I don't know if Spectre changed this.

I'm no expert in this domain but it seems to me that RedLeaf (implemented in Rust and formally verified) is vastly superior to seL4. AFAIU RedLeaf is orders of magnitude cheaper to formally verify to a much higher standard[1] while also being significantly more performant[2] and that Rust's properties are key to both of those advantages[1,2]. (Note: I only skimmed [2].)

Edit: It seems RedLeaf is immune to meltdown due to its design while seL4 has meltdown mitigations[2]. I would assume the same goes for spectre, but that would be an assumption on my part. (Note again, I've only skimmed [2] so I can easily be wrong here.)

[1]: https://www.ics.uci.edu/~aburtsev/doc/redleaf-hotos19.pdf

[2]: https://www.usenix.org/system/files/osdi20-narayanan_vikram....

While I don't know anything specific about RedLeaf, I highly doubt that it is completely immune to Spectre. Spectre fundamentally stems from how modern CPUs are designed and the current understanding is that there is no way to fix Spectre. If you're curious, see the paper "Spectre is here to stay: An analysis of side-channels and speculative execution" [0]. Even on fully up to date OSs with the latest version of Chrome, Spectre is still exploitable (see [1]).

[0]: https://arxiv.org/abs/1902.05178 [1]: https://security.googleblog.com/2021/03/a-spectre-proof-of-c...

I must admit that I don't really understand the RedLeaf design if it doesn't use hardware protections you cannot run C or use unsafe Rust "safely"?? Everything in 100% safe Rust isn't going to happen ever so it isn't really a seL4 competitor more a research prototype.

That said I can imagine a two layer system: if you use 100% safe Rust you have a 'fast path' direct access, otherwise you fallback to slower hardware protection.

I'll have a look thanks but note that seL4 is implemented in C because C has a formally verified compiler CompCert which Rust doesn't have..

... not to mention that seL4 was started in 2006, a full four years before Rust was even conceived of. The proof was finished a year before.

Reply on news.ycombinator.com