4 ms·
There is nothing wrong with defense in depth. But, this is not where things stop. I make extensive use of bounded model checking in my C development. I also us
by nanolith 2y ago
There is nothing wrong with defense in depth. But, this is not where things stop.
I make extensive use of bounded model checking in my C development. I also use privilege separation, serialization between separate processes, process isolation, and sandboxing. That's not because bounded model checking has somehow failed, but because humans are fallible. I can formally verify the code I write, but unless I'm running bare metal firmware, I also have to deal with an operating system and libraries that aren't under my direct control. These also have vulnerabilities.
That's not a trivial thing. The average software stack running on a server -- regardless of whether it is written in C, Rust, Modula-2, Pascal, Ada, or constructively proven Lean extracted to C++ -- still goes through tens of millions of lines of system software that is definitely NOT safe. All of that code is out of a developer's control for now. Admins can continually apply patches, but until those projects employ similar technology, they are themselves a risk.
One day, hopefully, all software and firmware will go through bounded model checking as a matter of course. Until then, we work with what we can, and we fix what we can. We can also rely on hardware mitigations where applicable. That's not failure as you have claimed, but practical reality.
- pdimitar 2y ago> I make extensive use of bounded model checking in my C development... I would absolutely love it if you were the majority, alas you are not. I emulate exhaustive pattern matching in my main language of choice because it does not have it (it's not Rust or OCaml or Haskell) but because I saw how beneficial and useful it is. And sadly, many of the other devs using that language don't do so, and I have made a good buck going after them and fixing their mistakes. I don't doubt your abilities as a person. I doubt the abilities of the corpus of C/C++ devs at large.
- nanolith 2y agoWell, that's something I hope to change. The tools required to write safer software exist. They just aren't widely distributed yet. I can say, without ego, that I'm a reasonably good software developer. But, it is the tooling and process that I use that allows me to build safer software and that makes me a reasonably good developer. The same is true of Rust developers. I can teach these skills to other developers, and in fact, I have plans to do so. I don't expect things to change overnight, any more than I expect things to be rewritten in Rust overnight. C++ has been around for nearly 40 years, and software is still written in C. But, we can do better, and we must do better.