[ryao]

There is another option, which is to use a sound static analyzer that can prove the absence of memory safety issues like astree, and fix things that cause it to complain until it stops complaining:

https://www.absint.com/astree/index.htm

For those who think static analyzers cannot do that, notice the word “sound”. This is a different type of static analyzer than the more common ones that do not catch everything.

Sadly, there is no open source option that works across a broad range of software. NASA’s IKOS is open source for example, but it does not support multithreading and some other things that I do not recall offhand, which makes it unable to catch all memory safety bugs in software using the features that it does not support. For now, people who want to use sound static analyzers need to use closed source tools or restrict themselves to a subset of what C/C++ can do so they can use IKOS:

https://github.com/NASA-SW-VnV/ikos

[voxl]

Even in their own list of features "Memory Safety" does not pop up, and none of the listed features indicate to me that they would entail memory safety. Academics aren't publishing droves of work on separation logic for a problem that can be solved by 1980s static analyzers.

[ryao]

They say that they can prove the absence of classes of bugs that make up memory safety:

* out-of-bounds array indexing,

* erroneous pointer manipulation and dereferencing (NULL, uninitialized and dangling pointers),

* read access to uninitialized variables,

NIST gave them a glowing review:

https://nvlpubs.nist.gov/nistpubs/ir/2020/NIST.IR.8304.pdf

It is possible to make sound static analyzers that can prove code to be free from memory safety bugs, but it is difficult and you need to implement checks that either complain or mathematically prove the absence of each class to do it.

These tools have been used for years in the aviation and nuclear industries, but almost nobody outside of those industries knows anything about them. If others had broader awareness of the existence of these tools, we could get open source equivalents and memory safety issues would be a thing of the past in C/C++ code.

Finally, your 1980s remark reveals enormous ignorance of what the field of formal methods has produced. Astree was not available in the 1980s. It took over 40 years of work to make and only became available about 20 years ago. C++ support took much longer for it to add, with it only adding it around 6 years ago if my recollection of the public documentation is correct. Some other things in this space are the Polyspace Code Prover and Frama-C.

[voxl]

I'm published in formal methods and see plenty of papers on static analysis of C. They ALL fail against a well designed type system.

[ryao]

Given your experience in the area, I highly encourage you to get the 30 day free trial and evaluate Astree yourself. You should be better positioned than I am to assess their claim of zero false negatives in all of the classes of issues that its creators claim that it can detect, which to my eye, appears to cover a superset of what is typically considered under memory safety. I very much look forward to the result of your effort. Given its use by Boeing and the ESA to prevent runtime errors in C/C++ code, I would be surprised if it failed your scrutiny.

Astree uses the theory of abstract interpretation that most of those in the formal methods community publishing papers do not touch as far as I know. It is therefore a different kind of tool for verifying properties of code than the techniques put forth in most formal methods papers.

NIST evaluated Astree and it got a perfect score on their test suite. It was actually a better than perfect score, as it found flaws in the test suite that NIST had not known existed. I have not heard of runtime errors in the Astree verified C/C++ code running on Boeing airliners or ESA space probes, unlike the prominent Toyota issues where they did not use any such tools and their slogan “always moving forward” became literal. So far, those who can afford it seem to be avoiding runtime issues in C/C++ code, which would be impossible if it did not work as advertised.

I acknowledge that correctness by external observation is not airtight logic. However, substantially similar reasoning applies to the security of RSA, since the RSA hardness assumption is an assumption and not a verifiable proof. A key difference is that with Astree, a claim is made that the software can make proofs internally to justify its claims, but we can scrutinize neither the proofs nor its source code. I choose to believe claims about Astree until they are proven otherwise given that Astree appears to be preventing runtime errors in a great number of mission critical applications and the independent NIST review found no flaws in its ability to statically detect sources of runtime errors.