I'd rather seL4, which isn't written in rust but on a time-proven language (C) and yet has thorough proofs of doing what it's supposed to do, unlike this OS you suggest.
https://www.cvedetails.com/vulnerability-list/opmemc-1/memor...
https://msrc-blog.microsoft.com/2019/07/16/a-proactive-appro...
Which are reaching the tipping point of enough is enough.
Which is why Android 11 will now require memory tagging hardware for C and C++ code, when running on ARM.
https://security.googleblog.com/2019/08/adopting-arm-memory-...
https://source.android.com/devices/tech/debug/tagged-pointer...
And no, it doesn't need to be Rust, in fact NVidia has decided to dump C and C++ for security critical firmware, betting on Ada,
https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto...
While F-Secure is using bare metal Go for their Foundry, https://www.f-secure.com/en/consulting/foundry
Speaking of seL4, Genode OS is now using Ada alongside seL4,
Now does seL4 support properly modern CPUs: multiple cores, with different power settings? This I don't know.
And what about Spectre?
What about Spectre? It is an hardware exploit, thus there is only so much one can don in software to prevent it.
However that shouldn't be an argument for not improving the security of the IT stack, people still die when wearing security belts and helmets, but they surely do surving in higher rates than when they weren't a requirement.
Exploits due to logical programming errors, false premises, hardware bugs, will always be around, however reducing the attack surface is already a big improvement.
And there has been mitigations done in software in the Linux kernel (and the web browsers but that's userspace), so my question:
has seL4 being updated with mitigations for Spectre?
Plus for a microkernel, this can be a big performance issue..
As for seL4, I only have superficial knowledge of the project.
seL4 may give you a formally verified kernel. However, formal verification is a dark art with very few high priests that actually understand it on the planet. Unless it becomes commoditised, it's not going to be popular. There has been some work towards that but it's still high-priest land.
Unless a significant portion of the software that runs on top of that microkernel is also formally verified, there's always risk of many sorts.
Oh and don't forget the fact that the hardware itself is likely not formally verified so open to attack.
That's a very absolutist way of thinking and therefore not very practical I confess - but hey I was playing devil's advocate.
If the Sealed Rust initiative succeeds then we may have a general purpose formal provability story at the Rust-LLVM-IR boundary thanks to the RustBelt project. That, in theory, will open the door to provably correct kernels and full stacks which I think is the right way to attack the problem.