6 ms·

Heartbleed and Static Analysis

134 points by pascal_cuoq 12y ago

willvarfar 12y ago
I presume, from their silence, that competing products also fail to find this bug?
- jetru 12y ago
  There are numerous reasons for this, as Regehr points out. None of these products are "sound". In other words, they aren't guaranteed to find everything. Most of the time, these are tradeoffs to reduce the number of false positives and to speed up the analysis, which come with the risk of false negatives, as is the case here.
  - aidenn0 12y ago
    Indeed, trading off sensitivity for specificity is always a win when trying to sell static analysis to people. Considering that any non-trivial piece of software has a fairly large number of bugs, you can dial the sensitivity way down and still find some bugs, and the high specificity looks really impressive "Most of what it labelled as bugs really were!" Consider the hypothetical situation where your piece of software has 40 bugs in it (but you don't know that). If you see a report of 10 bugs and 6 of them are real, that looks more impressive than a report of 100 bugs where 20 of them are real, despite the fact that the latter actually found more bugs. In fact there is a non-trivial chance that the first 5 or 10 bugs you look at in the latter will be false-positives. Obviously if your specificity goes too low, the payoff of inspecting each report starts to become questionable, but I think that to successfully market an analysis took, you need to sacrifice more sensitivity for specificity than merited by a rational analysis of the cost/benefit of detecting the bugs early.
- ScottBurson 12y ago
  I can confirm that HP Fortify SCA does not find this bug. (I am the architect for the SCA team.)
malanj 12y ago
Static analysis (and other "expensive" techniques) should really be standard on something as critical as OpenSSL. If I compare the effort we've had to go through building things that are allowed into a banking environment the OpenSSL project is very underfunded. Somehow we have to solve this "tragedy of the commons" problem in open source. OpenSSL must be worth millions of dollars to so many companies, but almost no-one cares about it. It seems very strange that the project is not getting BIG corporate sponsorship, given the value of the data it helps to protect.
- ScottBurson 12y ago
  The problem is that it's worth a relatively small amount of money to each of a huge number of people. We don't have a good way to pool funds for maintaining open source software in such a situation. Crowdfunding seems to be the obvious solution. But I asked in a previous Heartbleed discussion whether people would be willing to try it for OpenSSL, and got no response. Someone else commented that maybe Google will take over OpenSSL, or at least become a major contributor to it. It probably is in their interests to make sure this doesn't happen again -- maybe it's worth a large enough amount of money to them to justify dedicating a couple of engineers to it for a couple of years, which is what it seems to need.
unwind 12y ago
Very interesting article! A small typo, there's a sentence after the Frama-C code block that ends "[...] and that a subsequent memcpy() of the two regions will return zero" which should have a s/memcpy/memcmp/. Quite obvious, but in an article such as this it's best to be precise of course.
WalterBright 12y ago
It's interesting that these sorts of problems with memcpy, etc., always boil down to the same thing - C arrays are lowered to simple pointers when they are passed as function arguments. This means they lose their array bounds, frustrating attempts at overflow detection. This has caused endless bugs and endless workaround schemes of varying complexity. I wrote about it as "C's Biggest Mistake" a while back: http://www.drdobbs.com/architecture-and-design/cs-biggest-mistake/228701625 http://www.drdobbs.com/architecture-and-design/cs-biggest-mi... and offered a simple adjustment to C to fix it. I quote from the article: All it needs is a little new syntax: void foo(char a[..]) meaning an array is passed as a so-called "fat pointer", i.e. a pair consisting of a pointer to the start of the array, and a size_t of the array dimension. Of course, this won't fix any existing code, but it will enable new code to be written correctly and robustly.
- rwmj 12y ago
  This is basically what Bounds Checking GCC[1] did. Except instead of changing the syntax or using fat pointers, it kept a map of (pointer -> bounds), allowing memcpy to check the bounds of any arbitrary runtime pointer, and to interwork with code that isn't compiled with the -fbounds-checking flag. [1] https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html
- chalst 12y ago
  Your analysis of the issue of not being able to pass arrays as arguments is compelling, but I'm not so sure about "All it needs is a little new syntax" as a solution: you say how to keep backwards compatibility with existing C standards you need a #if cpp-directive: that's already a code health and maintenance problem that isn't going to go away. Regehr's suggestion of using assertions hidden in code avoids that: isn't it better? You could have just a comment directive like @ arraycast char* a \represents char a[..] and then you wouldn't need any cpp-directives.
- Serow225 12y ago
  I've always been curious why C was designed this way, was it thought to offer any advantages or just done to make the compiler writer's job easier?
Ono-Sendai 12y ago
I think this is a good demonstration of the limitations of static analysis - for a language like C, there will always be bugs that can't be found statically.
- Peaker 12y ago
  Unless you're willing to move the burden to the programmer, to prove correctness. Bugs can always be found statically, but there may always be bugs that evade all the static analysis you happened to do.
joosters 12y ago
Presumably, the static analysis won't find this bug because the 'out of bounds' memory that heartbleed accesses isn't necessarily out of bounds? As has been explained elsewhere, OpenSSL has a wrapper around malloc() and free() so that it re-uses allocations. This means that the 64k of buffer used to send the heartbeat response is data that has never been free()d and has previously been written to by the process. To make the static analysis spot this kind of thing, I'd guess you'd have to mark/label the OpenSSL allocators as being 'like' malloc. Likewise, valgrind would also not spot the faults without extra knowledge.
platz 12y ago
Also of note was Leslie Lamport's recent talk on how Amazon uses TLA+ to verify algorithms.
- bojblaz 12y ago
  Googled to no avail... link please?
  - platz 12y ago
    http://channel9.msdn.com/Events/Build/2014/3-642 http://channel9.msdn.com/Events/Build/2014/3-642

134 points by pascal_cuoq 12y ago

willvarfar 12y ago

I presume, from their silence, that competing products also fail to find this bug?

jetru 12y ago
There are numerous reasons for this, as Regehr points out. None of these products are "sound". In other words, they aren't guaranteed to find everything. Most of the time, these are tradeoffs to reduce the number of false positives and to speed up the analysis, which come with the risk of false negatives, as is the case here.
- aidenn0 12y ago
  Indeed, trading off sensitivity for specificity is always a win when trying to sell static analysis to people. Considering that any non-trivial piece of software has a fairly large number of bugs, you can dial the sensitivity way down and still find some bugs, and the high specificity looks really impressive "Most of what it labelled as bugs really were!" Consider the hypothetical situation where your piece of software has 40 bugs in it (but you don't know that). If you see a report of 10 bugs and 6 of them are real, that looks more impressive than a report of 100 bugs where 20 of them are real, despite the fact that the latter actually found more bugs. In fact there is a non-trivial chance that the first 5 or 10 bugs you look at in the latter will be false-positives. Obviously if your specificity goes too low, the payoff of inspecting each report starts to become questionable, but I think that to successfully market an analysis took, you need to sacrifice more sensitivity for specificity than merited by a rational analysis of the cost/benefit of detecting the bugs early.
ScottBurson 12y ago
I can confirm that HP Fortify SCA does not find this bug. (I am the architect for the SCA team.)

malanj 12y ago

Static analysis (and other "expensive" techniques) should really be standard on something as critical as OpenSSL. If I compare the effort we've had to go through building things that are allowed into a banking environment the OpenSSL project is very underfunded. Somehow we have to solve this "tragedy of the commons" problem in open source. OpenSSL must be worth millions of dollars to so many companies, but almost no-one cares about it. It seems very strange that the project is not getting BIG corporate sponsorship, given the value of the data it helps to protect.

ScottBurson 12y ago
The problem is that it's worth a relatively small amount of money to each of a huge number of people. We don't have a good way to pool funds for maintaining open source software in such a situation. Crowdfunding seems to be the obvious solution. But I asked in a previous Heartbleed discussion whether people would be willing to try it for OpenSSL, and got no response. Someone else commented that maybe Google will take over OpenSSL, or at least become a major contributor to it. It probably is in their interests to make sure this doesn't happen again -- maybe it's worth a large enough amount of money to them to justify dedicating a couple of engineers to it for a couple of years, which is what it seems to need.

unwind 12y ago

Very interesting article! A small typo, there's a sentence after the Frama-C code block that ends "[...] and that a subsequent memcpy() of the two regions will return zero" which should have a s/memcpy/memcmp/. Quite obvious, but in an article such as this it's best to be precise of course.

WalterBright 12y ago

It's interesting that these sorts of problems with memcpy, etc., always boil down to the same thing - C arrays are lowered to simple pointers when they are passed as function arguments. This means they lose their array bounds, frustrating attempts at overflow detection. This has caused endless bugs and endless workaround schemes of varying complexity. I wrote about it as "C's Biggest Mistake" a while back: http://www.drdobbs.com/architecture-and-design/cs-biggest-mistake/228701625 http://www.drdobbs.com/architecture-and-design/cs-biggest-mi... and offered a simple adjustment to C to fix it. I quote from the article: All it needs is a little new syntax: void foo(char a[..]) meaning an array is passed as a so-called "fat pointer", i.e. a pair consisting of a pointer to the start of the array, and a size_t of the array dimension. Of course, this won't fix any existing code, but it will enable new code to be written correctly and robustly.

rwmj 12y ago
This is basically what Bounds Checking GCC[1] did. Except instead of changing the syntax or using fat pointers, it kept a map of (pointer -> bounds), allowing memcpy to check the bounds of any arbitrary runtime pointer, and to interwork with code that isn't compiled with the -fbounds-checking flag. [1] https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html
chalst 12y ago
Your analysis of the issue of not being able to pass arrays as arguments is compelling, but I'm not so sure about "All it needs is a little new syntax" as a solution: you say how to keep backwards compatibility with existing C standards you need a #if cpp-directive: that's already a code health and maintenance problem that isn't going to go away. Regehr's suggestion of using assertions hidden in code avoids that: isn't it better? You could have just a comment directive like @ arraycast char* a \represents char a[..] and then you wouldn't need any cpp-directives.
Serow225 12y ago
I've always been curious why C was designed this way, was it thought to offer any advantages or just done to make the compiler writer's job easier?

Ono-Sendai 12y ago

I think this is a good demonstration of the limitations of static analysis - for a language like C, there will always be bugs that can't be found statically.

Peaker 12y ago
Unless you're willing to move the burden to the programmer, to prove correctness. Bugs can always be found statically, but there may always be bugs that evade all the static analysis you happened to do.

joosters 12y ago

Presumably, the static analysis won't find this bug because the 'out of bounds' memory that heartbleed accesses isn't necessarily out of bounds? As has been explained elsewhere, OpenSSL has a wrapper around malloc() and free() so that it re-uses allocations. This means that the 64k of buffer used to send the heartbeat response is data that has never been free()d and has previously been written to by the process. To make the static analysis spot this kind of thing, I'd guess you'd have to mark/label the OpenSSL allocators as being 'like' malloc. Likewise, valgrind would also not spot the faults without extra knowledge.

platz 12y ago

Also of note was Leslie Lamport's recent talk on how Amazon uses TLA+ to verify algorithms.

bojblaz 12y ago
Googled to no avail... link please?
- platz 12y ago
  http://channel9.msdn.com/Events/Build/2014/3-642 http://channel9.msdn.com/Events/Build/2014/3-642