Frama-C news and ideas

Blogger of multiple qualities Harry McCracken was recently still looking for “an iPad PDF reader which can handle giant files which are 100s of pages long without choking”. Sorry, I meant “STILL looking”.

PDF is a nineteen-nineties technology to display text and pictures. Key quote: “Each PDF file encapsulates a complete description of a fixed-layout flat document, including the text, fonts, graphics, and other information needed to display it”.

Now, you might think that any proposal made in 1991 to master the intricacies of displaying text and pictures would have succeeded by 2013, but apparently not, according to Harry's call for help.

Fortunately, another nineteen-nineties technology came to the rescue: the Djvu format was created in 1996 for the purpose, I wish I was kidding, to store text and images. Key quote: “a computer file format designed primarily to store scanned documents, especially those containing a combination of text, line drawings, indexed color images, and photographs”.

It is good to see progress at work. Even if we acknowledge that it takes years to get these things right and that a project started in 1996 is bound to be more technologically advanced than one started in 1991, there remains the question, what the file have we been collectively doing during the years 2000?

This leads me into a personal anecdote. In 1995, I was admitted at the ENS of Lyon (and I may be thinking about it because I am visiting back there on January 29. Drop by if you are around…). These were interesting times: 1995 is more or less the year the internet slash the world wide web started to become widespread in the US and then in other parts of the world. We were privileged to have access to it already at the ENSL.

In 1996, I left France for a 2-and-a-half months internship at Indiana University. Before I left, I taught my father to use the 28800 BPS external modem I was leaving him to dial long-distance to Lyon, impersonate me on the ENSL's server, upload a text file containing news of the family, download a text file that might contain news from me, and disconnect as soon as possible because heck, that was expensive (although cheaper than any available alternative). This was done with software that was called either “Kermit” or “ZMODEM”. Kermit, I am pretty sure it was. You could not trust these new-fangled protocols then any more than you can now.

Nowadays, my father has his own e-mail address and he may write to anyone he likes, as opposed to leaving messages in a dropbox for me. And he does not pay long-distance rates for it.

But I can't help thinking that all progress that has occurred since then was incremental. Slightly better for much cheaper. There has been the iPhone. But then again, the first PalmPilot was launched in 1997.

So, what have we been doing during the years 2000? What technologies were so life-changing that we are going to take them for granted in the 2010s?

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.

A couple of months ago, I packed a computer into a brown plastic bag of the kind usually used for trash. I then carried the carefully packed computer down to the basement. Physically, the computer still works. It is still beautiful (it is an iMac G4). It has been with me for the last ten years: I bought it second-hand in December 2002 from my friend Damien Doligez. I have used it for both work and entertainment for several years, and then gave it to my computerwise-unsophisticated sister who has been using it since. The design, much friendlier than later iMacs, and even than earlier iMacs, evokes the Luxo Pixar character. This computer was built to last: after ten years, the white plastics are still white. I pick this insignificant detail not because I particularly care about the tint of my computing devices, but because I don't. This is not an accident. People took care of the details when designing this computer, all the way down to how it would look as it aged.

The iMac G4 came with the cutest matched loudspeakers. The integrated modem would not find much use nowadays, but the computer also has USB, firewire and ethernet ports, and Wi-Fi. The thinking behind the integrated modem remains avant-gardist even if the technology is now outdated: this computer was the hub of its buyer's future digital lifestyle. It was intended to be connected, and it was intended not to look like an untidy mess in your living room.

I opened it a couple of times to upgrade the hard disk and optical drive. It reminded me of the glimpse I once took as a student of the insides of a Sun workstation. I don't think I could explain this particular feeling to someone who did not see the inside of a Sun workstation—or of an iMac. As a concrete example that does not do justice to the experience, the unused screw holes of the factory-installed optical drive I retrieved from the computer had been taped over, so that air would not be sucked through the drive, lest dust accumulate on the drive's door as years passed.

Unfortunately, some functions mostly everyone expects from a computer nowadays is to display e-mail and web pages, and this computer is no longer fit for this purpose. This isn't a case of running new software on old hardware. This has never worked, but one used to be able to use loved hi-tech gadgets way past obsolescence as long as one avoided the mistake of installing new software on them. For lustra, you could keep using the spreadsheet you were used to for accounting or your simple-but-sufficient word processor. Even games kept working!

The problem nowadays is that the option not to upgrade software is no longer available: software more than a few years old ceases to receive security patches. The iMac G4 in question cannot be upgraded past Mac OS X 10.4. On Mac OS X 10.4, Firefox cannot be upgraded past version 3.6. Firefox 3.6 received its last security update in March 2012 and has now joined the Great Repository in the Sky.

Here is an idea for 2013: how about making software that works? Of course, it would not automatically adapt to new protocols, but as long as the user was satisfied with the old ones, this software would simply keep working. It would not have to be constantly updated with security patches because it would have been made right the first time, just like hardware sometimes is.

I would not want to give the impression that I am unfairly picking on the fine developers of Firefox. Firefox 3.6 continued to be maintained long after Safari for OS X 10.4 had ceased to receive security updates. In fact, the TenFourFox project, a maintained variant of Firefox for precisely the kind of computer I took to the basement, is a testament to the power of Open Source Software. Unfortunately, there is no Adobe Flash support in TenFourFox, and I fear that this might complicate the life of a computerwise-unsophisticated user.

Acknowledgements: besides selling me his computer, Damien Doligez officially owned the first OS X-able mac I used, as a PhD student. Harry McCracken suggested to liven up this post with a picture. Gerhard Piezinger photographed an iMac very much like mine, and I used his picture.

A few days ago, I announced that the world had been using an unverified zlib library for too long, and that we were going to fix this. This post is the first progress report. I have found a harmless undefined behavior in zlib and I have learnt something about the comma operator. This post only covers the latter aspect.

The comma operator

The comma operator can be used to build an expression e1, e2. When e1, e2 is evaluated, first e1 is evaluated (for its result and side-effects), then the result is discarded and e2 is evaluated.

The comma counts as a sequence point. Sequence points are the points in a C program in-between which it is illegal to both read and write the same memory location; for instance x++ + x is undefined behavior because there is no sequence point between the post-incrementation x++ and the use of the value of x. Coming back to the comma operator, since it counts as a sequence point, I thought this might allow writing (x++, y) + (y++, x), but I am not so sure about that now.

Easing the value analysis' job on zlib

Formally verifying such a library as zlib is difficult. Indeed, otherwise, considering its usefulness and fame, if it was easy, someone would already have advertized that they had formally verified it.

One verification plan that I wanted to try out on this library is the model-checking approach that we first experimented with last summer.

The words “model-checking” may evoke different things to different people. In this context, they mean the propagation of only unabstracted known-to-be-feasible states, so that if a division by zero is reached in the program, we know for sure that this dangerous division can be reached for some inputs. In other words, we are talking here about a technique to avoid false positives, in addition to avoiding false negatives as we always do.

There is a catch: the propagation of unabstracted states does not really scale to a codebase the size and complexity of zlib. My plan was to ease the job of Frama-C's value analysis by carefully re-introducing a little bit of abstraction. I intended to modify the zlib library so that the modified version has all the same opportunities to do something wrong with pointers as the original version, but the modified version always computes zero as output sequence. This would make many memory states that would otherwise have been different become identical, something that the value analysis efficiently recognizes and takes advantage of.

A beginner's mistake

And this is how I found myself modifying *output_pointer++ = expression_with_side_effects; so that it would only write 0 to the output buffer, but otherwise have all the same side-effects as the original. I chose to replace it with the statement below. And I was pretty pleased with myself.

  *output_pointer++ = expression_with_side_effects, 0;

Unfortunately, after one additional cycle of verification, it turned out that in the C syntax, assignment has higher precedence than comma. My modified statement was parsed as:

  (*output_pointer++ = expression_with_side_effects), 0;

It behaved exactly as the original statement in assigning non-zero values to the output buffer. I had instead intended:

  *output_pointer++ = (expression_with_side_effects, 0);