Just wondering why the microkernel has to be written from scratch and not use an open kernel that has some proofs behind it.
Most of it is gplv2
Hello! 
I’m new here and very interested in Rust as a language for systems development!
I then saw your question and I already thought the same (you know, why reinvent the wheel?). But I think the creators of Redox OS want to show that it is possible to write an OS fully in Rust.
To your idea: I’d also prefer using an existing microkernel that additionally is mathematically proven to be correct. As far as I understand, sel4 is also proven to be correct if compiled with optimizations enabled, meaning that you could do gcc/clang -O3 to fully optimize it and then build a Rust ecosystem around it. Take a look at this: robigalia. Its goals are 1.) building an OS around sel4 with Rust and 2.) provide a POSIX interface.
Yeah, I know that Redox OS doesn’t and probably won’t ever aim to support POSIX. But in my understanding, a POSIX interface with C functions forwarding the function caller to a safe Rust function would enable us to recompile any C/C++ application that claims to be POSIX-compatible.
I’m gonna follow both projects’ development - I prefer robigalia’s goals, but I really think that Redox is more actively developed. Anyway, I’m looking forward to seeing Rust more and more in such projects as it is a great language!
Sincerely
Sören
The proven correctness is more wishful thinking then anything else as the assumptions in https://sel4.systems/Info/FAQ/proof.pml can never be accomplished. Without discussing that point, if it was the point, to make a secure and stable OS, why would one ever start from scratch?
From what I gather, and please excuse me if I’m wrong, I am fairly new here, Redox is more a research project aimed to bring progression to the ecosystem (while implementing a a real, working example of the topic at research). That cannot be achieved by only utilizing existing software. Also that justifies just about any design decision that is not conservative or security/stability-minded.
As to your link to robigalia: Thank you for the interesting topic to read up on! It certainly looks interesting. But I think it is a misconception that correctness or safety implies security (“Create a secure POSIX-compatible userland”).
The proven correctness is more wishful thinking then anything else as the assumptions in https://sel4.systems/Info/FAQ/proof.pml2 can never be accomplished.
That certainly is a good point. Also, development of Redox seems much more advanced than that of robigalia. I assume Redox OS to be more stable or even usable much earlier.
But I think it is a misconception that correctness or safety implies security
You probably mean that an interface’s design - no matter how memory-safe the interface is - can lead to serious problems. Like a process escaping from its chroot-environment (I know that chroot is a Linux command, but that should serve as an example). Though I think that robigalia’s developers probably wanted to write a safe POSIX implementation. Of course, any security breach regarding POSIX’s design could still be used on robigalia, but the POSIX functions would be memory-safe as far as Rust can promise.
This should be another topic (or maybe there already is a post about it), but nothing could keep someone from implementing a POSIX interface for Redox OS. In simplest case, several functions certainly could simply be forwarded to their Rust equivalent. Some other functions might need more wrapping, but why not try it? Maybe a project for my next free days? 
Hi, Robigalia lead dev and seL4 proof engineer here.
about seL4 proofs
The proof is not wishful thinking. There are ways of satisfying or validating each of the assumptions:
- assembly: the proofs are being updated to include this
- hardware: some verified hardware exists, but this is always an assumption in high-assurance applications, so no sleep lost there
-
hw management: some of this (eg TLB behavior) is being added, but this is indeed a source of bugs in seL4 for some SoCs. Fortunately it’s relatively small and people review it
- boot code: this was part of the proof once, and is being added back again.
- virtual memory: this is pretty bulletproof, but the complications it mentions do apply.
- DMA: a problem in any high-assurance application. IOMMU solves this.
- timing channels: this will be mitigated in the near-future with temporal partitioning.
What is the goal of the proof, anyway? The proof provides evidence of correctness, to a high degree of assurance. This is not an absolute thing, as you mention, the proof has some assumptions that need to be validated before you can apply its conclusions. But seL4 is the most extensively validated kernel, formally or otherwise, and important investments by government and military groups show that they want the sort of assurance seL4 provides.
about robigalia
So, Robigalia is about creating a persistent capability-based operating system. By “secure POSIX-compatible userland”, I mean that it is confined and can’t violate integrity or confidentiality of the rest of the system. This is accomplished quite easily using the guarantees provided by seL4 about confinement and information flow security. Of course, POSIX itself isn’t terribly trustworthy, so anything running inside a POSIX “container” is somewhat suspect. But things inside the “container” won’t be able to break out of it.
Safety in the Rust sense has nothing to do with the security of Robigalia, really. It does help with ease of implementation, but the security comes from the inherent properties of pure capability systems. It’s baked into the architecture.
why redox shouldn’t port seL4
rewriting it in anything but C is stupid. the proofs won’t apply and the C is already fine.
why redox shouldn’t use seL4
it’s much more interesting to have a pure-Rust kernel, and gives you more design flexibility
3 Likes
Why wouldn’t the proofs apply from C to Rust?