>C++. Oh lord. Why are you writing a microkernel in C++? If there was anything they learned from L4 (Xen, Linux, ...) it is that C is sufficient. Why do you want to implement something small with something that is large? This one is a real head scratcher.
Because if there was anything proven from years and years of using C, it's that it is woefully insecure and should not be trusted to write a kernel with.
You can still fuck up with C++, sure, but std::shared_ptr offers more guarantees than *.
Yes, we know that C is not secure. We also know that C++ is not secure and moreover it definitely isn't C, now with security. It's just more bigger C. So use your phrase, you can still fuck up with C++. You can just do it in more clever and insidious ways.
seL4, a third-generation microkernel is 8,700 lines of C code and 600 lines of assembler.
So we also empirically know that you can formally verify a microkernel written in C. Now if the Fuchsia folks had gone ahead and formally verified their microkernel, this issue would be moot. But they haven't. So we are instead left with std::shared_ptr offers more guarantees than *. While this isn't nothing, it isn't much either.
I wouldn't use SEL4 as an argument. It is completely unreasonable to build a production kernel the way they did - it took them ages to get what they had. Google is probably looking to develop features/ move code a lot faster than is possible using their technique.
Good coding practices take no time to implement, you learn it once and you write that way. It is not bullet proof, neither are capabilities. Still, at least they're practical.
I think you miss the point of a microkernel! The point is to keep all your "features" outside of it, and to use it only to implement the core set of functionality necessary to have secure shared access to the hardware. The general L4 concept has proven industry use, so there's no reason you can't take advantage of the already accomplished work on seL4 to bootstrap your own secure OS.
It's true that seL4 is not a magic safety or security bullet; in particular, their FAQ says that they haven't completed extending their proofs to DMA safety via VT-d or SystemMMU on ARM, so DMA-accessing services would have to be separately verified. And its particular feature set may not be appropriate for all situations. But if its API does work for you, it would be foolish not to at least consider using it.
It is really unreasonable to dismiss seL4 simply because it took them a lot of effort to create it. That effort is now done and can be re-used and magnified by further effort.
How about Muen separation kernel in SPARK Ada with automated prover eliminating many classes of undefined behavior? Or C with tools like Frama-C and Astree Analyzer (like SPARK for C)? C++ can't reach the safety of its competition due to more complexity and less tooling.
I thought about it. The reason I left it off is a lack of static analysis, automatic generation of tests, certified compilers, etc. There's tons of FOSS and commercial vendors for doing such things in C with quite a bit for Ada. Whereas, I could find only one or two products for C++ that seemed like it would be really helpful as opposed to just kind of. So, I pivoted my recommendations to go with languages that have huge, tooling ecosystems in academic R&D and commercial. You can certainly use it but might get less value in long term.
Embedded, real-time Java could also be on the list since Java ecosystem has a verification tool for about everything. CompSci loves Java for some reason (probably mandated classes). Yet, verifiable C and SPARK are closer to the metal than embedded Java plus no Oracle risk. So, left off Java as well.
There is no Oracle risk with Java, when companies play by the rules.
PTC, Aicas, IBM, MicroEJ, Excelcior JET, HP, Cisco, Ricoh, Azul, Red Hat and so many other companies are selling JDKs with their own set of features, without having had any issue with Sun or Oracle.
Only Google has an issue with Oracle, because they decided they were the cool kid better than anyone else whose rules don't apply to.
Because if there was anything proven from years and years of using C, it's that it is woefully insecure and should not be trusted to write a kernel with.
You can still fuck up with C++, sure, but std::shared_ptr offers more guarantees than *.
EDIT: HN stop eating my stars