Hacker News Reader

Comment by monocasa | Hacker News Reader

I think that it's more that they already have a kernel, and their focus is moving as much as possible outside the kernel rather than adding to it.

And, FWIW, I can see a point where they have a kernel written in C or C++ that's formally verified (like sel4), at which point, what's the point of rewriting it in Rust? sel4's semantics are stronger than what Rust gives you out of the box.

I say this as someone who's written a handful of Rust kernels, and is quite bullish on Rust adoption.

View on HN

IIRC sel4 was initially specified in Haskell, formally verified, then formally translated to C.

> While the Haskell prototype is an executable model and implementation of the final design, it is not the final production kernel. We manually re-implement the model in the C programming language for several reasons. Firstly, the Haskell runtime is a significant body of code (much bigger than our kernel) which would be hard to verify for correctness. Secondly, the Haskell runtime relies on garbage collection which is unsuitable for real-time environments. Incidentally, the same arguments apply to other systems based on type-safe languages, such as SPIN [7] and Singularity [23]. Additionally, using C enables optimisation of the low-level implementation for performance. While an automated translation from Haskell to C would have simplified verification, we would have lost most opportunities to micro-optimise the kernel, which is required for adequate microkernel performance.

https://www.sigops.org/s/conferences/sosp/2009/papers/klein-...

Neat, I didn't know about seL4. Can you point me to how they define the proof for it?

They've done a really good job documenting it in their papers and online docs, but the general flow is to verify equivalence of the generated binary and the formal specification, then to prove properties like memory safety of the formal spec.

I'd start here if you want to learn more: https://sel4.systems/Info/FAQ/proof.pml

Let me know if you have any other questions.

FOSDEM speach video [1] about the status of seL4, I really enjoyed.

[1]: https://fosdem.org/2020/schedule/event/uk_sel4/

> what's the point of rewriting it in Rust

The fact that you don't have to write C and also that you can have different API semantics. E.g. you can pass user space code (say callbacks) to the kernel while maintaining safety.

I don't see a world where they allow "run this user code as ring 0".

I do. If it's a callback and all arguments are passed in, it's fine.

It can literally take control of the machine. Even if it's written in Rust, there's no "this binary used an unsafe block" on binaries. If they're signing and proving everything, then what's the purpose of sticking that code in user space to begin with?

There does exist a precedent in tha mainframe world of trusted compilers and mechanisms of verifying that a piece of code was produced by the blessed compiler.

I guess the embedded version of this would have to be an offline compiler & code signing based system, and the language would need to be much more sandboxy than Rust.

I know maybe you are writing a driver or smth.

Bad idea in the wake of Spectre and meltdown. You want user code in a different address space for those reasons these days.

Unless you mean more like using the user callback in the same way, say, a posix signal handler works, or Microsoft's SEH or APCs, then I would say it's already possible with a C ABI, citing those things as examples.

Reply on news.ycombinator.com