Frama-C news and ideas

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

Why verify zlib?

As an interlude in the zlib verification thread, this post asks two questions. Is there any chance of finding a bug in zlib, and does it matter?

Could there be a bug in zlib?

It is not entirely impossible. The previous post in this blog pointed to a relatively minor issue in the zlib source code, and the next post will show a more serious (albeit still minor) one.

In July of 2005, a buffer overflow in zlib was found by Tavis Ormandy. Key quote: “An attacker could construct a malformed data stream, embedding it within network communication or an application file format, potentially resulting in the execution of arbitrary code when decoded by the application using the zlib library.”

If you have been following the zlib thread, this is exactly the context we are investigating: decompression of a maliciously crafted stream.

Does it matter?

In 2005, people did think it mattered. The CVE summary points out that zlib is involved when decompressing a PNG image (most users think of PNG images as innocuous objects that they should be allowed to look at regardless of origin without compromising the host computer). Other examples are the “Windows binary of Virtual Floppy Drive 2.1” and “Official Windows binaries of curl”. I do not think that list is exhaustive. Does the HTTP/1.1 protocol not allow for zlib-compressed data to be exchanged between client and server? A malicious client could cause a buffer overflow on the server with a simple request, and/or a malicious server could cause a buffer overflow in the client by replying to a request with specially crafted pretend-compressed data.

And a benchmark for the future

I am making a deliberate effort not to look at that bug now, but it goes without saying that when the verification of zlib is done, I will check that the same method find the bug that was in the pre-July-2005 version.


1. On Tuesday, January 15 2013, 11:22 by David Mentré

Pascal, is the Frama-C-annotated code of zlib available somewhere?

2. On Wednesday, January 16 2013, 00:08 by pascal

Hello, David.

You will be happy to know that you are not the first to ask about this ACSL-annotated zlib source code. In truth I have done very little annotating for now, although I did try different approaches and wrote a bit of C code to drive the library, the equivalent of what would have been tests in a testing-based approach. All this will be made available when it provides a coherent picture.

3. On Friday, January 18 2013, 14:44 by David Mentré

OK, thank you Pascal.

4. On Sunday, January 20 2013, 22:05 by John Regehr

Pascal, could you post a minimal example triggering the PUP undefined behavior?

For some reason I can't leave a comment on that post, or I would have...

5. On Monday, January 21 2013, 01:14 by pascal


Posts on this blog can only be commented on during a window of a few days. This is how I avoid quadratic blog spam, receiving and browsing through linear spam instead. Sorry.

I have added a line of instrumentation to show that the invalid pointed being compared in inffast:320 was computed by strm->next_out - OFF at line inffast.c:101.