Comment by junon
Comment by junon 3 days ago
This comment demonstrates a lack of understanding of what the unsafe keyword is for in Rust.
Unsafe specifically states that no code within it may introduce UB after the unsafe block exits (post-condition). It also doesn't allow certain operations no matter how hard you try (e.g. the borrow checker still applies, but you can use raw pointers in ways you couldn't outside of an unsafe block, assuming you don't introduce UB).
As someone designing a kernel in Rust, you literally cannot avoid unsafe code, regardless of the language, to implement a kernel.
It's worth mentioning that "unsafe" and "vulnerable" are two different things.
SeL4 is safe because of its extensively verified codebase written in a language suited for verification. Last I checked they port it to C after the fact, but it could just as well be ported to Rust. It'd still be "unsafe" but significantly less "vulnerable".
For example, modifying cr3 or TTBRn_EL1 is incredibly unsafe. But it happens all the time when context switching.
In the kernel I use `unsafe` pretty commonly to denote functions with preconditions not representable by the type system. This enforcement wouldn't even be possible in C or any other language I know of personally that'd be efficient to write an OS in.
The only gripe I have with Rust's unsafe is that I can't mark methods with preconditions as unsafe while still requiring `unsafe` clauses within the function body. I've thought about opening an RFC for `unsafe(pub)` for this reason.
But doing so has made iteration and overall safety of the codebase much easier to reason about because it forces me to think about every call site in which I might introduce a problem if not done carefully.
> This enforcement wouldn't even be possible in C or any other language I know of personally that'd be efficient to write an OS in.
The sky is the limit when it comes to verification of complex properties for C programs. You “just” need a few expert level theorem prover users and a couple of years :)
If you’re actually operating in the kind of domain where exhaustive verification is worth the time investment, C blows Rust out of the water (due to it’s simple semantics and mature ecosystem of verification tooling). There remain no formal semantics of the surface level rust language (and constructing one is a daunting task given its deep and baroque complexity). Verification at the MIR or LLVM levels may be more tractable, but I’m not aware of any large scale results here. C or assembly in combination with some verification tooling remains the gold standard for fast and correct software at the highest level.
Rust offers reasonable memory safety in a relatively accessible and fully automated package. It’s a better choice than C for the majority of cases, but it’s far from the last word when it comes to safety.
btw (and as noted in a sibling comment), sel4 is fully verified down to the assembly level.