5 ms·

Difficult, yes, but solved [1]. There exist sound static analyzers for C and C++. "Sound" meaning no false-negatives. [1] https://github.com/NASA-SW-VnV/ikos/b

Difficult, yes, but solved [1]. There exist sound static analyzers for C and C++. "Sound" meaning no false-negatives. [1] https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/README.md#checks https://github.com/NASA-SW-VnV/ikos/blob/master/analyzer/REA...

jakevn 7y ago
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?
- lapinot 7y ago
  `Sound' does not mean `complete'. Don't forget that no false positive or negative isn't all, the solver might just give up.
- nickpsecurity 7y ago
  Neither FOSS projects nor commercial software use proven methods most of the time. That's why you see the results you see. I described that here: http://www.ganssle.com/tem/tem372.html#article4 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.
- fulafel 7y ago
  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.
pcwalton 7y ago
How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.
- pron 7y ago
  It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well. 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.
- OnlyOneCannolo 7y ago
  Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool. 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.
littlestymaar 7y ago
No false negative sounds nice, but the problem is the amount of false positives. The Unix `true` command is also a static analyser with no false negative (but 100% false positive on perfect code). 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.
- OnlyOneCannolo 7y ago
  This particular tool lets you trade analysis time for accuracy (amount of false positives) depending on your choice of settings, which is pretty neat.

jakevn 7y ago

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?

lapinot 7y ago
`Sound' does not mean `complete'. Don't forget that no false positive or negative isn't all, the solver might just give up.
nickpsecurity 7y ago
Neither FOSS projects nor commercial software use proven methods most of the time. That's why you see the results you see. I described that here: http://www.ganssle.com/tem/tem372.html#article4 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.
fulafel 7y ago
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.

pcwalton 7y ago

How does this deal with higher-order functions? This is usually where these analyzers fall down. If you don't allow higher-order functions, then you just forbade virtual methods, so your analyzer can't handle real-world C/C++ code.

pron 7y ago
It's really not that hard, but it's important to remember that while these tools do guarantee no undefined behavior, they may require either adding annotations or changing the program a bit. Their goal is to guarantee lack of UB not for free, but at a cost that's drastically lower than a rewrite in a safe language, something they deliver on quite well. 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.
OnlyOneCannolo 7y ago
Off-hand, I don't know how it handles higher-order functions. It analyzes LLVM IR, not the source directly, so I guess it depends on how virtual methods are represented in LLVM IR and whether those instructions are supported or ignored by the tool. 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.

littlestymaar 7y ago

No false negative sounds nice, but the problem is the amount of false positives. The Unix `true` command is also a static analyser with no false negative (but 100% false positive on perfect code). 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.

OnlyOneCannolo 7y ago
This particular tool lets you trade analysis time for accuracy (amount of false positives) depending on your choice of settings, which is pretty neat.