[kardashian007]

Seriously, two things: formal verification of correctness is sorely needed and a language platform which has complete, bidirectional C interoperability in targeting both kernel- and user-land which can be gradually migrated to one compilation unit a time and has much more safety, is more succinct, has C feature parity and no/minimal runtime performance hit would be requirements for candidates to change languages, but only after impressing Linus, lieutenants and contributors of undeniable value.

See also: seL4, Isabelle/Coq, Idris

[moosingin3space]

seL4 looks like a great base to build secure embedded systems on. There's an interesting project called robigalia that aims to make it possible to build seL4 userspace threads in Rust, which should be an excellent base to build on.

[zzzcpan]

I disagree. It is possible to put some real effort into the compiler making the same C code safe against such problems without infinitely expensive rewrites.

[johncolanduoni]

Tools like this for C already exist, and have existed for some time. They've failed to reach fixation, even in security-critical areas like kernels. If that is going to be the answer, then a different approach to making C safer is definitely required.

[duneroadrunner]

Might I suggest SaferCPlusPlus [1] as the "different approach". SaferCPlusPlus is a memory safe subset of C++. But the key is that the C++ preprocessor is now powerful enough to enable the creation of compatible safe substitutes for the unsafe C/C++ elements. (Native pointers in particular of course.) So rather than rewriting all your code, translating from traditional C/C++ to SaferCPlusPlus can be just a glorified "find and replace" exercise. (Well, maybe a little more than that, but not much.)

I think solutions that don't require any code modification like Softbound and SAFEcode (and even the LLVM sanitizers) aren't popular because the resulting executables are quite slow. Whereas SaferCPlusPlus strives for minimal performance penalty. (Perhaps with some cooperation from C/C++'s formidable optimizing compilers.) (Btw, if it's not already clear, this is a shameless plug.)

And not only is conversion to SaferCPlusPlus far less effort than rewriting everything in another memory safe language, it can be done completely incrementally. What language has better "bidirectional C interoperability" than C++?

[1] https://github.com/duneroadrunner/SaferCPlusPlus

[zzzcpan]

Production ready tools are not there yet, they all are essentially POCs and some work has to be done to apply those ideas to existing projects. For the linux kernel, I presume, it would have to be done in gcc with a bunch of gcc flags or it won't be adopted.