Yep, this is why in Vulnerability Research one of the main ways of finding bugs is concolic execution (Looking at logic for error cases). Memory safety is pretty easy to catch if you arn't a clown and use good coding patterns. Logic isn't, which is where the big money and big boy vulns come in. And honestly, most modern OS's have memory safety protections built in. This is 1992 anymore.

Yes, memory safety is a solved problem, and research has mostly moved on. The best solution is to use a memory-safe programming language. Yet we find security vulnerabilities all the time in software written with memory unsafe programming languages.

Sure, but safety-critical development is a different domain than vulnerability research.

"Memory safety is pretty easy to catch" - my experience over the last 18 months or so on a large C++ open source project says very much otherwise, almost every week a new NPE or core dump/access violation seems to leak into the codebase. These simply can't happen in many other languages and many now even have good support for non-optional references, ruling out entire classes of bugs that can suck up significant developer time to track down. And for long running systems memory leaks can also be a substantial cause of instability. If I were working on a safety critical system I'd actively push to avoid using C/C++ unless there really was no alternative. And yes modern OS kernels are pretty good evidence that it is possible to do but I'd suggest it requires exceptional programmers and some very rigorous processes to enforce.

Assume you have a functional safety requirement for which a standard exists. What language implementation would you use that is certified for that standard?

Not sure how that question can be meaningfully answered unless it's for a specific safety requirement/standard. Are you suggesting that for most standards that require certification, there are no compiler implementations certified except for C/C++ ones?

Try the exercise. Choose one and then choose your tooling. If it's not C, C++, or Ada, I'll be surprised.

I had some involvement with development of an air traffic management system, which was being written in Java, as that was certified for use in that field. As a language, I'd rather use C++ over Java, but if safety criticality were the priority, I'd choose Java every time. I haven't coded in Ada but unless there's something about it that's truly awful to work with, it seems a better choice than C/C++ from what I know about it.

Well, I have worked on safety-critical projects in the industry, though there wasn't a lot of C/C++ (health-care software connected to the internet). I currently work with researchers, some in the software security domain.

I don't think it's clear that the OP organisation is stuck with C. Perhaps it's the case, but I think it's also time, in 2022, to push a bit to move toward safer programming languages.

You describe an excellent set of rules and processes, perhaps too much for most projects. It sounds like it could be even better with a memory-safe programming language. Also, I doubt that most secure critical C/C++ projects proof their source code correctly in Coq or similar.

I also think many security issues are tightly related to the programming language. For example, SQL injections are because of SQL, XSS because of HTTP/HTML, and Buffer overflows because of C.

Security and safety are different domains and only tangentially related - i.e. it helps in both domains for code to be correct, but it's not sufficient in either.

One take away I got from reading some Nancy Leveson stuff is a lot of danger lurks at the interfaces between things. You can take two things that work perfectly and put them together and get catastrophic behavior. That argues to the point that there isn't a magic language that will make problems go away.

Another take away from an old old paper was that safety must be a primary design goal from the start. It's not something you can bandaid in afterwards. There is a lot of stuff out that what that didn't happen and as a result you see constant whack a mole with critical bugs.