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"  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"  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.