Comment by throwawaymaths
Comment by throwawaymaths 3 days ago
Safe what? Rust isn't memory safe if you are using unsafe anywhere. There are other "safety" issues with rust as well. Sel4 is in c but it's provably safe (if you're on arm).
Comment by throwawaymaths 3 days ago
Safe what? Rust isn't memory safe if you are using unsafe anywhere. There are other "safety" issues with rust as well. Sel4 is in c but it's provably safe (if you're on arm).
> 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.
sel4 is implemented 3 times: in c, haskell and isabelle/HOL.
The implementation in isabelle is proven to satisfy various key high level security properties. All 3 implementations are proven to be semantically equivalent. The compiled assembly output from gcc is also proven to be semantically equivalent to the C implementation.
Having these implementation layers is helpful for the proof work since the highest level properties can be proven over a much simpler and highly abstracted implementation (in issabelle / HOL), and the layers make the chain of equivalence proofs down to assembly more tractable. Most of the proof work is done in isabelle with the final C <-> assembly proofs using a custom automated smt based proof engine implemented in python.
The trusted components are the various language semantics / import tools, as well as a few very low level pieces of actual OS code (mostly parts of the early boot sequence iirc).
multicore sel4 is implemented but still unverified:
https://docs.sel4.systems/projects/sel4/frequently-asked-que...
I guess https://github.com/seL4/l4v/tree/rt is the ongoing verification work for that
> SeL4 is safe because of its extensively verified codebase written in a language suited for verification
I think this is incorrect. It is written in C, compiled to arm assembly, and the assembly is analyzed and checked by Isabelle/HOL.
Section 3 in the whitepaper <https://sel4.systems/About/seL4-whitepaper.pdf> describes how it is done: (1) they restrict themselves to a possible-to-reason subset of C (that they have a parser in Isabelle for), and implement a kernel and prove the implementation is formally correct, and (2) to avoid compiler/kernel bugs of host & trojan horses, they verify the compiled/linked output as well.
Their Figure 3.2 shows how this is done: each transformation into the "Graph Language" nodes is proven formally correct. They need two proofs because the binary is automatically proven correct, i.e. what they prove is that their formalized binary is equivalent to the original binary using a HOL4 disassembler, without knowing what sort of binary they have at their hands. On the C side, they preserve semantics while proving the program correct (manually, i.e. they wrote the proofs themselves), and then they prove the two are equivalent, again automatically, using SMT solvers and throwing small chunks of data at it.
As they explain, proving the two "Graph Language" representations to be equivalent semantically is, in general, undecidable like the halting problem. However, they get away with it because the C compiler is not too wild in its output.
> but it could just as well be ported to Rust
Without formal semantics for the complete rust language the result couldn't be verified. Rust's complexity makes it hard to define formal semantics.
I wouldn't normally bring this up as a disadvantage of rust, but people aren't normally talking about software that has been formally verified.
Ferrocene doesn't involve formal proofs. ISO 26262 and IEC 61508 are primarily process-focused standards for project management, quality control, integration, testing, and code review. To the extent there's automated code analysis, it would involve linting for disallowed patterns similar to MISRA C.
The point still stands: rust isn’t memory safe if you use unsafe.
It’s true that to write a kernel safely, you need more than memory safety, but that’s kind if a different point. Folks don’t just use the unsafe construct in Rust to do kernely things.
Yeah I read it. I define memory safe as: Any program accepted by the compiler follows the typing rules of the language.
That holds for Rust if you don’t use unsafe at all. It also holds in other memory safe languages (like JavaScript). Some memory safe languages gaurantee this without any caveats (JavaScript) while others guarantee it with caveats (Rust if you don’t use unsafe, Java if you don’t use certain APIs, etc).
I didn't neccessarily mean Rust, but was curios to see how that would look.
Here's a Rust demo implementation of the seL4 root task (the first process that gets started on boot) using their Rust SDK and it doesn't look like it's using unsafe anywhere: https://github.com/seL4/rust-root-task-demo/blob/main/crates...
(I don't speak Rust so I might have missed it).
Go might be another interesting choice.
(let's not turn this thread into Rust vs Go vs whatever agaaaaaain ... we've got enough of those please).
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.