--- layout: post author: Pascal Cuoq date: 2013-01-16 23:00 +0200 categories: undefined-behavior zlib format: xhtml title: "Bad zlib, bad! No compare pointer!" summary: --- {% raw %}
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?
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.
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.
Season with a specially crafted deflated buffer:
unsigned char deflated_buffer[40] = { 120 156 67 84 ...
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:
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.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.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.
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.
{% endraw %}