yes, we don't need to debate the question "can people write memory safe code in C" the answer is overwhelmingly obvious to almost all of us
Conversation
It would be hard enough to make a microkernel secure if it was 50k lines of Rust with only 4k lines of unsafe code with potential memory corruption, let alone millions of lines of trusted C full of memory corruption from all kinds of trivial mistakes / oversights. It's a joke.
1
4
17
Just want to point out that seL4 is about 10K lines of C and is formally verified to use no UB, no OOB array access, no crashes, etc... Not trying to defend C but there are ways to make anything safe if you care enough. The problem is people don’t care.
3
1
8
Sure, but at that point it's not C. It's a subset of C that was verified via proofs. Those proofs are an extension to the language. Similarly, you can define a general purpose subset of C with annotations for ownership, lifetimes, etc. letting you write memory safe code.
2
1
You end up with something that looks a lot like Rust. You can't compile existing C codebases with an implementation of it. They have to be specifically written for it with the annotations, but they don't need complex proofs, unless they want to prove more than memory safety.
2
No, it doesn't look at all like Rust. It has completely different idioms and is much simpler. There's no such thing as "an implementation of it" that can't compile existing codebases because it's just C.
1
The choice to use a particular good form of the language is on the application side, not the implementation side.
1
It does end up looking like the memory safety system in Rust if you are actually introducing a system to provide memory safety. The kind of clean C code you are talking about still has plenty of memory corruption bugs and is still unacceptable for modern security requirements.
1
You absolutely don't "introduce a system". That's anti-idiomatic and just reconstructing some other heavy language on top of C, which is always awful.
1
By introduce a system, I mean defining a subset of C with annotations that is actually memory safe, which isn't all that complex and doesn't need to have much noisy syntax. A lot can be inferred, but still, you can't easily adapt existing code to be verified as safe like this.
2
If the code is incredibly simple and conforms to the necessary rules for aliasing, etc. to provide safety then sure. If it does anything with custom data structures other than totally flat array-based ones, it's not going to be trivial. It matters for human verification too.