It's not that hard to automatically prove that a large piece of software has no buffer overflows and no null pointer dereferences. We had that working decades ago.
Unless the code is in C. Then it's really hard.
Unless the code is in C. Then it's really hard.
[1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...
http://www.ganssle.com/tem/tem372.html#article4
The tools can also miss things. They miss more as complexity goes up. High-assurance systems used to structure things in a hierarchical way with simple functions and only call downs to aid the analysis. Basically, reduce combinatorial explosion. Most software isn't structured anything like that. It does combinatorial explosion with C not giving analyzer a lot of information to begin with. So, it causes tools to miss things.
Rust might be easier to analyze due to the type system. Those labels become inputs and heuristics for future static analyzers.
The tool doesn't claim to handle everything, and doesn't claim to be complete. You can absolutely write code that it can't analyze because it's either too complicated or you're using unsupported language features. If you want your code to be analyzable, then you have to write it that way. The tool isn't magic.
Don't you think it's an over-statement to say that it can't handle real-world code if it doesn't support higher-order functions? Not all C++ code uses virtual methods, and C doesn't even have this feature in the language.
So, for example, suppose you have a higher order function that takes a function returning a pointer, calls it, and dereferences its return value. For simplicity, let's assume we only care about NULL dereferencing and not other kinds of invalid memory, but the idea is the same. You then have two options: either you annotate the argument to require that it cannot return NULL -- in which case the tool would attempt to prove that any function passed as an argument satisfies this (possibly with the help of further annotations) -- or you add a runtime check, in which case the automatic proof is simple.
And a perfect static analyser with no false negative or false positive is equivalent to solving the halting problem. So what we need is a «good enough» solution working with existing code. But the amount of CVEs and the low adoption of such tools empirically shows that we are far from there.