Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Bad zlib, bad! No compare pointer!

In a previous post, we remarked that the decompression function of zlib, for some inputs, computes an invalid pointer. But at least it neither dereferences it nor compares it to another pointer.

Or does it?

Recipe for an invalid pointer comparison

Instrument

Take an ordinary zlib library version 1.2.7, and instrument it according to the diff below.

$ diff -u zlib-1.2.7/inffast.c zlib-modified/inffast.c
--- zlib-1.2.7/inffast.c	2010-04-19 06:16:23.000000000 +0200
+++ zlib-modified/inffast.c	2013-01-16 23:37:55.000000000 +0100
@@ -64,6 +64,9 @@
       requires strm->avail_out >= 258 for each loop to avoid checking for
       output space.
  */
+
+int printf(const char *fmt, ...);
+
 void ZLIB_INTERNAL inflate_fast(strm, start)
 z_streamp strm;
 unsigned start;         /* inflate()'s starting value for strm->avail_out */
@@ -316,6 +319,7 @@
     strm->next_in = in + OFF;
     strm->next_out = out + OFF;
     strm->avail_in = (unsigned)(in < last ? 5 + (last - in) : 5 - (in - last));
+    printf("out=%p, end=%p\n", out, end);
     strm->avail_out = (unsigned)(out < end ?
                                  257 + (end - out) : 257 - (out - end));
     state->hold = hold;

This instrumentation causes two pointers, out and end, that are compared at that point of the library, to be printed. Apart from that, it does not change the behavior of the library. The library behaves the same when the printf() call is not there, albeit less observably.

Following the documentation, write an ordinary main()

Prepare a main() function that uncompresses a buffer deflated_buffer more or less according to the official tutorial:

main(){
  unsigned char out_buffer[CHUNK_OUT];

  printf("out_buffer: %p\n", out_buffer);

  /* allocate inflate state */
  ...

  ret = inflateInit(&my_strm);

  if (ret != Z_OK)
    return ret;

  my_strm.next_in = deflated_buffer;
  my_strm.avail_in = 40;
  my_strm.next_out = out_buffer;
  my_strm.avail_out = CHUNK_OUT;
	
  ret = inflate(&my_strm, Z_FINISH);

  ...
}

You can download the file zlib_UB.c.

Secret ingredient

Season with a specially crafted deflated buffer:

unsigned char deflated_buffer[40] = {
  120,
  156,
  67,
  84,
...

Test

Having built the instrumented zlib, you can compile and link the main() function:

$ gcc -I Downloads/zlib-modified/ zlib_UB.c Downloads/zlib-modified/libz.a
$ ./a.out 
out_buffer: 0x7fff5bd9fa34
out=0x7fff5bd9fa33, end=0x7fff5bd9fa5e

Although we followed the documentation when writing the main() function that calls it, zlib appears to be, at inffast.c:320, comparing a pointer out that points before out_buffer to a pointer end that points inside out_buffer. In fact, the pointer out has been computed as an offset of out_buffer, namely, out_buffer - 1. Zlib is not supposed to do this, for two reasons:

  1. The compiler could place out_buffer at address 0, or at the beginning of a segment in a segmented architecture. Then out_buffer - 1 would evaluate to 0xffffffffffff and appear to be larger than end, or cause a hardware exception. To be fair, in general the same value still ends up being stored in strm->avail_out, because both branches of the expression (out < end ? 257 + (end - out) : 257 - (out - end)) compute the same thing.
  2. Even without the array out_buffer being placed at address 0—which is rather unlikely—the compiler could suddenly become too smart for its own good and generate code that treats the condition out < end as false in this case. This has happened before. Key quote: “Some versions of gcc may silently discard certain checks for overflow. Applications compiled with these versions of gcc may be vulnerable to buffer overflows.” In this case, the invalid pointer out_buffer - 1 would be interfering with a compiler optimization, so anything might happen. Since it is strm->avail_out the statement is computing, a buffer overflow might result.

Fix

This problem and the previously described one have the same cause; they stem from the following optimization in inffast.c:

#ifdef POSTINC
#  define OFF 0
#  define PUP(a) *(a)++
#else
#  define OFF 1
#  define PUP(a) *++(a)
#endif

Defining POSTINC makes both the minor issues go away.

Conclusion

The defect identified here is related to the previous one, and like it, it is probably innocuous. Nevertheless, we initially set out to formally verify zlib, so we should stick to it: a formally verified zlib wouldn't compute negative offsets of arrays, much less compare them to valid offsets of the same array. So far, I have not been able to confirm any of the potential issues listed by Frama-C's value analysis in zlib with POSTINC defined, so that version of the library may reveal itself to be the formally verified version we are after.


This post was proofread by Fabrice Derepas and Olivier Gay.