Today in my Writing Solid Code class we went through some of the 151 defects that Coverity Scan reports for OpenSSL. I can’t link to these results but take my word for it that they are a pleasure to read — the interface clearly explains each flaw and the reasoning that leads up to it, even across multiple function calls. Some of the problems were slightly alarming but we didn’t see anything that looks like the next heartbleed. Unfortunately, Coverity did not find the heartbleed bug itself. (UPDATE: See this followup post.) This is puzzling; here’s a bit of speculation about what might be going on. There are basically two ways to find heartbleed using static analysis (here I’ll assume you’re familiar with the bug; if not, this post is useful). First, a taint analysis should be able to observe that two bytes from an untrusted source find their way into the length argument of a memcpy() call. This is clearly undesirable. The Coverity documentation indicates that it taints the buffer stored to by a read() system call (unfortunately you will need to login to Coverity Scan before you can see this). So why don’t we get a defect report? One guess is that since the data buffer is behind two pointer dereferences (the access is via s->s3->rrec.data), the scanner’s alias analysis loses track of what is going on. Another guess is that two bytes of tainted data are not enough to trigger an alarm. Only someone familiar with the Coverity implementation can say for sure what is going on — the tool is highly sophisticated not just in its static analysis but also in its defect ranking system.
The other kind of static analysis that would find heartbleed is one that insists that the length argument to any memcpy() call does not exceed the size of either the source or destination buffer. Frama-C in value analysis mode is a tool that can do this. It is sound, meaning that it will not stop complaining until it can prove that certain defect classes are not present, and as such it requires far more handholding than does Coverity, which is designed to unsoundly analyze huge quantities of code. To use Frama-C, we would make sure that its own header files are included instead of the system headers. In one of those files we would find a model for memcpy():
/*@ requires \valid(((char*)dest)+(0..n - 1));
@ requires \valid_read(((char*)src)+(0..n - 1));
@ requires \separated(((char *)dest)+(0..n-1),((char *)src)+(0..n-1));
@ assigns ((char*)dest)[0..n - 1] \from ((char*)src)[0..n-1];
@ assigns \result \from dest;
@ ensures memcmp((char*)dest,(char*)src,n) == 0;
@ ensures \result == dest;
@*/
extern void *memcpy(void *restrict dest,
const void *restrict src,
size_t n);
The comments are consumed by Frama-C. Basically they say that src and dest are pointers to valid storage of at least the required size, that the buffers do not overlap (recall that memcpy() has undefined behavior when called with overlapping regions), that it moves data in the proper direction, that the return value is dest, and that a subsequent memcmp() of the two regions will return zero.
The Frama-C value analyzer tracks an integer variable using an interval: a representation of the smallest and largest value that the integer could contain at some program point. Upon reaching the problematic memcpy() call in t1_lib.c, the value of payload is in the interval [0..65535]. This interval comes from the n2s() macro which turns two arbitrary-valued bytes from the client into an unsigned int:
#define n2s(c,s) ((s=(((unsigned int)(c[0]))<< 8)| \
(((unsigned int)(c[1])) )),c+=2)
The dest argument of this memcpy() turns out to be large enough. However, the source buffer is way too small. Frama-C would gripe about this and it would not shut up until the bug was really fixed.
How much effort would be required to push OpenSSL through Frama-C? I don’t know, but wouldn’t plan on getting this done in a week or three. Interestingly, a company spun off by Frama-C developers has recently used the tool to create a version of PolarSSL that they promise is immune to CWEs 119, 120, 121, 122, 123, 124, 125, 126, 127, 369, 415, 416, 457, 562, and 690. I think it would be reasonable for the open source security community to start thinking more seriously about what this kind of tool can do for us.
UPDATES:
- In a comment below, Masklinn states that OpenSSL’s custom allocators would defeat the detection of the too-large argument to memcpy(). This is indeed a danger. To avoid it, as part of applying Frama-C to OpenSSL, the custom malloc/free functions would be marked as being malloc-like using the “allocates” and “frees” keywords supported by ACSL 1.8. Coverity lets you do the same thing, and so would any competent analyzer for C. Custom allocators are regrettably common in oldish C code.
- I’m interested to see what other tools have to say about heartbleed. If you have a link to results, please put it in a comment.
- I re-ran Coverity after disabling OpenSSL’s custom freelist and also hacking CRYPTO_malloc() and friends to just directly call the obvious function from the malloc family. This caused Coverity to report 173 new defects: mostly use-after-free and resource leaks. Heartbleed wasn’t in the list, however, so I stand by my guess (above) that perhaps something related to indirection caused this defect to not be ranked highly enough to be reported.
- HN has some discussion of PolarSSL and of this blog post. Also Reddit.
18 responses to “Heartbleed and Static Analysis”
The issue with things like Frama-C is that they are by far the easiest to use if you start out a project using them, and you often don’t know which projects you retroactively wished you had done so until they are big and crufty.
Hopefully cryptographic and safety-critical projects can show the value of these tools, and make static-analysis more widely known. The LLVM project advertising their static-analysis features in clang has certainly raised awareness a bit.
However, it does seem that for a large number of commercial embedded projects, you’re lucky to see -Wall or PCLint used, both of which are primitive tools compared to what is out there.
I’m not sure the second one is correct, unless I misunderstood the bug the allocated buffers are correct (they’re all the user-provided length + whatever padding and pre-info is necessary). But when the amount of payload data read into the input buffer (via read(2) or something similar) is smaller than the user-provided length, that’s was not checked, and because malloc[0][1] the data from previous allocations remain in the input buffer (not overridden) and are copied into the output buffer[2].
So the issue is not the memcpy itself, it copies between two valid buffers of the same length, the issue is that the input buffer may be filled with no payload data and thus leak whatever “garbage” was still in memory.
[0] compounded by openssl’s freelists in that it would have bypassed BSD’s malloc.conf J or Z flags, but afaik there’s no malloc.conf on linux or osx so the bug would remain there
[1] I don’t understand why so many are so adverse to calloc. Plus by not using calloc, there’s no pressure to improve its performance e.g. I think freebsd has a background process zeroing memory and marking it as “calloc-ready”. That’s only done if people use calloc and ask for a fast calloc
[2] which is why malloc.conf’s G option (guard pages) does not trip[3], even after disabling freelists, because the buffer accesses are valid
[4] http://www.tedunangst.com/flak/post/heartbleed-vs-mallocconf last paragraph
I think you mean “subsequent memcmp()” instead of “subsequent memcpy()” in the paraqraph explaining the Frama-C comments.
“a subsequent memcpy() of the two regions will return zero”
That sentence should say memcmp() instead of memcpy() right, i.e. dest should have the same content as src?
Typo in function name. The text explaining comments for Frama-C says “subsequent memcpy()” when it should say “subsequent memcmp()”.
s/”that a subsequent memcpy”/”that a subsequent memcmp”/
Is it really practical to implement openssl’s functionality using something laborious but safe, with just the smallest possible idioms implemented in assembly for performance and side channel attack mitigation?
Whoops, fixed the memcpy()/memcmp() typo, thanks folks!
Heartbleed for the non-technical: http://xkcd.com/1354/
Would be interested to see if CodeSonar would be able to find it, as it often finds things that Coverity misses.
The annotations that Frama-C uses is really interesting. It’d be really nice if there were some “standard” way of annotating all kinds of human-known-facts about the software, so you can go crazy with all the formal methods. Microsoft now has “SAL” (Source-code Annotation Language) which uses ugly keywords and is of course specific to their compiler…
Re: use-after-free with normal malloc, I am told (though I haven’t seen the code) that hidden by the freelisting are a number of code paths that go like this:
char * packet = malloc(size);
// fiddle with packet;
free(packet);
// Actually, some more work to do!
packet = malloc(size);
// fiddle more…
Their freelists are LIFO and apparently sufficiently unshared that this “works”. Kind of terrifying for the rest of us, though, no? (And explains why Theo De Raadt et al claim that due to poor testing (and stuff like the above) openssl no longer works if you try to configure it without freelisting.
I don’t think I want to take your word for it. Could you at least give us a screenshot ?
Hi ilja, I strongly encourage you (and anyone else) to register for an account at Coverity Scan and to use it to scan some open source software. It is easy and free.
A screenshot does not really illustrate the nice features of this interface, but here is one showing a defect on OpenSSL:
http://www.cs.utah.edu/~regehr/coverity.png
With little knowledge of the details here, but general intuition based on being a former developer of a Coverity competitor, my guess is the pointer indirection is the issue. That’s a never-ending source of unpleasant engineering tradeoffs when you’re trying to do “fast” analysis of large real-world code bases.
Ben, thanks. I’m still hoping someone will run OpenSSL 1.0.1f through the tool you are referring to and write up a report about the results.
Masklinn, OS X has very similar malloc debugging facilities, in the form of environment variables (see: MallocScribble, MallocGuardEdges, etc., in ‘man malloc’) and also ‘guard malloc’, see ‘man libgmalloc’.
I’ve run a static analyzer but failed to find the bug. The heavy use of pointer arithmetic in code, which causes cross-function aliasing in a large scale, is definitely one of the major reasons why current analysis tools fail. Coverity’s fixing is essentially converting the issue to a local analysis by customization, which is a common practice.
The current patch to the Heartbleed bug appears to be strange to me. My first thought would be checking the payload that is actually received against its claimed length. If not equal, then the message is discarded. This would prevent garbage Heartbeat messages from entering a system at the first place. Why does the current patch allows a garbage message to enter the system and discard it later?
I ran openssl in a debugger for little time and to my surprise that the admission interface of messages/records into the system is so obscure that I can’t figure out how to do this in a couple of hours. This might explain why the current fixing is done before replying not after receiving. Of course, I’m not an openssl developer and missed something. But a patch that works is ok.
Some time ago, a vulnerability was revealed in OpenSSL, and I guess there’s no programmer who hasn’t been talking about it since then. I knew that PVS-Studio could not catch the bug leading to this particular vulnerability, so I saw no reason for writing about OpenSSL. Besides, quite a lot of articles have been published on the subject recently. However, I received a pile of e-mails, people wanting to know if PVS-Studio could detect that bug. So I had to give in and write this article: http://www.viva64.com/en/b/0250/
Gah! Why do people keep repeating this canard about OpenSSL’s freelists. Does no-one bother to read the code? Or even the patch? The memory allocated for Heartbleed _used malloc_, despite everyone’s deranged insistence it didn’t.