On the matter of the Heartbleed bug, Bruce Schneier wrote in his Crypto-Gram of 15th April: '"Catastrophic" is the right word. On the scale of 1 to 10, this is an 11.' I read several years ago that a kernel of a certain operating system has been rigorously verified with a modern program verification system. Could hence bugs of the genre of Heartbleed be prevented from occurring via application of program verification techniques today or is this yet unrealistic or even principally impossible?
$\begingroup$
$\endgroup$
1
-
2$\begingroup$ Here is an interesting analysis of this question by J. Regehr. $\endgroup$– Martin BergerApr 16, 2014 at 16:17
Add a comment
|
6 Answers
$\begingroup$
$\endgroup$
To answer your question in the most concise way - yes, this bug could have potentially been caught by formal verification tools. Indeed, the property "never send a block which is bigger than the size of the hearbeat that was sent" is fairly simple to formalize in most specification languages (e.g. LTL).
The problem (which is a common criticism against formal methods) is that the specifications you use are written by humans. Indeed, formal methods only shift the bug-hunting challenge from finding the bugs to defining what bugs are. This is a difficult task.
Also, formally verifying software is notoriously difficult due to the state-explosion problem. In this case, it is especially relevant, since many times in order to avoid the state explosion, we abstract away bounds. For example, when we want to say "every request is followed by a grant, within 100000 steps", we need a very long formula, so we abstract it to the formula "every request is eventually followed by a grant".
Thus, in the heartbleed case, even while attempting to formalize the requirements, the bound in question could have been abstracted away, resulting in the same behavior.
To sum up, potentially this bug could have been avoided by using formal methods, but there would have had to be a human specifying this property in advance.
$\begingroup$
$\endgroup$
4
Commercial program checkers like Klocwork or Coverity might have been able to find Heartbleed since it is a relatively simple "forgot to do a bounds check error," which is one of the main problems they are designed to check for. But there is a much simpler way: use opaque abstract data types that are well tested to be free from buffer overrun.
There are a number of "safe string" abstract data types available for C programming. The one I'm most familiar with is Vstr. The author, James Antill, has a great discussion about why you need a string abstract data type with its own constructors/factory methods and also a list of other string abstract data types for C.
answered Apr 16, 2014 at 14:35
-
2$\begingroup$ Coverity doesn't find Heartbleed, see this analysis by John Regehr. $\endgroup$ Apr 16, 2014 at 16:17
-
$\begingroup$ Nice link! It demonstrates the true moral of the story: program verification can't make up for poorly designed (or non existent) abstractions. $\endgroup$ Apr 16, 2014 at 16:35
-
2$\begingroup$ It depends what you mean by program verification. If you mean static analysis, then yes, that is always an approximation, as a direct consequence of Rice's theorem. If you verify full behaviour in an interactive theorem procer, then you get a cast-iron guarantee that the program meets its specifications, but that's extremely laborious. And you still face the problem that your specifications might be wrong (see e.g. the Ariane 5 explosion). $\endgroup$ Apr 16, 2014 at 18:59
-
1
$\begingroup$
$\endgroup$
2
If you count as a " program verification technique " the combination of runtime bound-checking and fuzzing, yes this particular bug could have been caught.
Proper fuzzing will cause the now infamous memcpy(bp, pl, payload); to read across the limit of the memory block pl belongs to. Runtime bound-checking can in principle catch any such access, and in practice, in this particular case, even a debug version of malloc that cares to bound-check the parameters of memcpy would have done the job (no need to mess with the MMU here). Problem is, performing fuzzing tests on each kind of network packet takes effort.
-
1$\begingroup$ While true in general, IIRC, in OpenSSL's case the authors implemented their own internal memory management such that it was much less likely for
memcpyto hit the true boundary of the (large) region originally requested from the systemmalloc. $\endgroup$ Apr 26, 2014 at 8:49 -
$\begingroup$ Yes, in the case of OpenSSL as it was at time of the bug,
memcpy(bp, pl, payload)would have had to check against the bounds used by OpenSSL'smallocreplacement, not the systemmalloc. That rules out automated bound-checking at the binary level (at least without deep knowledge of themallocreplacement). There must be recompilation with source-level wizardry using e.g. C macros replacing the tokenmallocor whatever replacement OpenSSL used; and it seems we need the same withmemcpyexcept with very clever MMU tricks. $\endgroup$– fgrieuApr 26, 2014 at 9:46
$\begingroup$
$\endgroup$
Using a tighter language doesn't just move goal posts around from getting implementation correct to getting the spec right. It is hard to make something that is very wrong yet consistent logically; which is why compilers catch so many bugs.
Pointer Arithmetic as it is normally formulated is unsound because the type system doesn't actually mean what it is supposed to mean. You can avoid this problem completely by working in a garbage collected language (the normal approach that makes you also pay for abstraction). Or you can be much more specific about what kinds of pointers you are using, so that the compiler can reject anything that is inconsistent or just can't be proven correct as written. This is the approach of some languages like Rust.
Constructed types are equivalent to proofs, so if you write a type system that forgets this, then all kinds of things go wrong. Assume for a while that when we declare a type, we actually mean that we are asserting the truth about what is in the variable.
- int* x; //A false assertion. x exists and does not point to an int
- int* y = z; //Only true if z is proven to point to an int
- *(x+3) = 5; //Only true if (x+3) points to an int in same array as x
- int c = a/b; //Only true if b is nonzero, like: "nonzero int b = ...;"
- nullable int* z = NULL; //nullable int* is not the same as an int*
- int d = *z; //A false assertion, because z is nullable
- if(z != NULL) { int* e = z; } //Ok because z is not null
- free(y); int w = *y; //False assertion, because y no longer exists at w
In this world, pointers can't be null. NullPointer dereferences don't exist, and pointers don't have to be checked for nullness anywhere. Instead, a "nullable int*" is a different type that can have its value extracted to either null or to a pointer. This means that at the point where the non-null assumption starts you either go log your exception or go down a null branch.
In this world, array out of bounds errors don't exist either. If the compiler cannot prove that it's in bounds, then try to rewrite so that the compiler can prove it. If it cannot, then you will have to put in a the Assumption manually at that spot; the compiler may find a contradiction to it later on.
Also, if you can't have a pointer that is not initialized, then you won't have pointers to uninitialized memory. If you have a pointer to freed memory, then it should be rejected by the compiler. In Rust, there are different pointer types to make these kinds of proofs reasonable to expect. There are exclusively owned pointers (ie: no aliases), pointers to deeply immutable structures. The default storage type is immutable, etc.
There is also the issue of enforcing an actual well defined grammar on protocols (which includes interface members), to limit the input surface area to exactly what is anticipated. The thing about "correctness" is: 1) Get rid of all undefined states 2) Ensure logical consistency. The difficulty of getting there has a lot to do with using extremely bad tooling (from the point of view of correctness).
This is exactly why the two worst practices are global variables and gotos. These things prevent putting pre/post/invariant conditions around anything. It's also why types are so effective. As types get stronger (ultimately using Dependent Types to take the actual value into account), they approach being constructive correctness proofs in themselves; making inconsistent programs fail compilation.
Keep in mind that it's not just about dumb mistakes. It's also about defending the code base from clever infiltrators. There will be cases where you have to reject a submission without a convincing machine-generated proof of important properties like "follows the formally specified protocol".
$\begingroup$
$\endgroup$
Static analysis tools like Coverity can indeed find HeartBleed and similar defects. Full disclosure: I cofounded Coverity.
See my blog post on our investigation of HeartBleed and how our analysis was enhanced to detect it:
http://security.coverity.com/blog/2014/Apr/on-detecting-heartbleed-with-static-analysis.html
$\begingroup$
$\endgroup$
automated/formal software verification is useful and can help in some cases but as others have pointed out, its not a silver bullet. one could point out that OpenSSL is vulnerable in that its open source and yet used commercially and industry-wide, widely used, and not nec heavily peer reviewed prior to release (one wonders if there are even any paid developers on the project). the defect was discovered basically through code review post-release, and the code was apparently reviewed pre-release (note though there is probably no way to track who did the internal code review). the "teachable moment" with heartbleed (among many others) is basically better code review ideally before release esp of highly sensitive code, possibly better tracked. maybe OpenSSL will now be subject to more scrutiny. another option is refactoring code to use more secure/safe API libraries to construct the code operations which are less subject to security lapses through programmer errors.
more bkg from media detailing its origins:
Heartbleed was an accident: Developer confesses to causing coding error and admits its effect is 'clearly severe' "German developer Dr Robin Seggelmann admitted he wrote the code, It was then reviewed by other members and added to OpenSSL software"
How Codenomicon Found The Heartbleed Bug Now Plaguing The Internet "The security firm’s chief explains how the flaw was found, how deep the risk goes, and what people can do about it now."
3 big lessons to learn from Heartbleed "The devastating OpenSSL vulnerability proves the importance of data center orchestration, the wisdom of running older versions, and the need to give back to the OpenSSL project"
