Comment by dexterlemmer | Hacker News Reader

Comment by dexterlemmer | Hacker News Reader

Parent Full thread

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