4 ms·

That's a rather cynical interpretation of these initiatives. CHERI, for instance, has been in development for twenty years. It predates the general availability

That's a rather cynical interpretation of these initiatives. CHERI, for instance, has been in development for twenty years. It predates the general availability of open source tools like CBMC or languages like Rust. But, that doesn't make the concept better or obsolete. It makes it complementary. Hardware security is complementary to software security. Mitigations at the hardware level, the hypervisor level, and the operation system level complement architectural, process, and tooling decisions made at the software level. Defense in depth is a good thing. There can always be errors in one layer or another, regardless of software solution, operating system, hypervisor, or hardware. I can wax poetic about current CPU vulnerabilities that must be managed in firmware or operating systems.

pjmlp 2y ago
Complementary, as the ultimate defence wall. Many of the issues caused by C, are solved by Modula-2, Object Pascal and Ada, we didn't need to wait for Rust. But those aren't the languages that come for free with UNIX. Or even better, they would be solved by C itself, if WG 14 cared even a little about providing proper support for slices, proper arrays and proper string types, or even as library vocabulary types. But what to expect, when even Dennis Ritchie wasn't able to get his approach to slices being worked on by WG 14. So hardware memory tagging, and sandboxed enclaves it is.
- 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 ago
      Well, 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.
      - pdimitar 2y ago
        Fully agreed. I hope you don't take my criticisms and our back and forth as hostile -- they are not.
        nanolith 2y ago
        I don't. Passion is good, and I'm glad we can have a passionate discussion while remaining civil. We both want the same thing: safer software.

pjmlp 2y ago

Complementary, as the ultimate defence wall. Many of the issues caused by C, are solved by Modula-2, Object Pascal and Ada, we didn't need to wait for Rust. But those aren't the languages that come for free with UNIX. Or even better, they would be solved by C itself, if WG 14 cared even a little about providing proper support for slices, proper arrays and proper string types, or even as library vocabulary types. But what to expect, when even Dennis Ritchie wasn't able to get his approach to slices being worked on by WG 14. So hardware memory tagging, and sandboxed enclaves it is.

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 ago
    Well, 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.
    - pdimitar 2y ago
      Fully agreed. I hope you don't take my criticisms and our back and forth as hostile -- they are not.
      - nanolith 2y ago
        I don't. Passion is good, and I'm glad we can have a passionate discussion while remaining civil. We both want the same thing: safer software.