If this has solved the issue of automatically proving that any C or C++ program has no buffer overflows, why do we still see CVEs for popular libraries and software that result from them?
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.
Because people can't resist chasing proven incorrect code ("find bugs"), instead of overhauling programs for proven correct code. Because the latter is a lot of work.
nickpsecurity|6 years ago
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.
lapinot|6 years ago
fulafel|6 years ago