Null-Pointer Crashes, No More

As an earlier article [1] emphasized, code matters; so do programming languages. While Eiffel is best known for its Design by Contract techniques, they are only one part of a systematic design all focused on enabling developers to realize the best of their abilities — and eradicate from their code the sources of  crashes and buggy behavior.

Talking about sources of crashes, one of the principal plagues of modern programs is null pointer dereferencing. This term denotes what happens when you call x.f, meaning apply f (a field access or an operation) to the object that x references. If you want to define meaningful data structures, you need to allow “null”, also known as Nil and Void, as one of the possible values for reference variables (for example to terminate linked structures: the “next” field of the last list element must be null, to indicate there is no next element).  But then you should make sure that x.f never gets called for null x, since there is in that case no object to which we can apply f.

The problem is particularly acute in object-oriented programming languages, where x.f is the major computational mechanism. Every single execution of this construct (how many billions of them occurred in running programs around the world since you started reading this article?) faces that risk. Compilers for many languages catch other errors of a similar nature — particularly type errors, such as assigning the wrong kind of value to a variable —but they do nothing about prohibiting null pointer dereferencing.

This fundamental brittleness threatens the execution of most programs running today. Calling it a “billion-dollar mistake” [2]  is not an exaggeration. Alexander Kogtenkov surveyed [3] the null-pointer-derefencing bugs in the Common Vulnerability and Exposure database, the reference repository of information about Internet attacks. The resulting chart, showing the numbers per year, is edifying:

 

               Source: Alexander Kogtenkov

Beyond the numbers stand real examples, often hair-raising. The description of vulnerability CVE-2016-9113, reported less than two months ago, states:

There is a NULL pointer dereference in function imagetobmp of convertbmp.c:980 of OpenJPEG 2.1.2. image->comps[0].data is not assigned a value after initialization(NULL). Impact is Denial of Service.

Yes, that is for the JPEG standard. Try not think of it when you upload your latest pictures. Just for the last two months, the CVE database contains null pointer vulnerabilities affecting products of the Gotha of the IT industry, from Google and Microsoft (“theoretically everyone could crash a server with just a single specifically crafted packet“) to Red Hat and  Cisco. The entry for an NVIDIA example explains:

For the NVIDIA Quadro, NVS, and GeForce products, NVIDIA Windows GPU Display Driver R340 before 342.00 and R375 before 375.63 contains a vulnerability in the kernel mode layer (nvlddmkm.sys) handler where a NULL pointer dereference caused by invalid user input may lead to denial of service or potential escalation of privileges.

We keep hearing complaints that  “the Internet was not designed with security in mind”. What if the problem had far less to do with the design (TCP/IP is brilliant) than with the languages that people use to write tools implementing these protocols?

In Eiffel, we decided that the situation was no longer tolerable. After dealing with unsafe casts through the type system, memory management errors through garbage collection, data races through the SCOOP concurrency mechanism, null pointer deferencing was the remaining dragon that we had to slay. Today Eiffel is void-safe: a null pointer derefence can simply not happen. By accepting your program, the compiler guarantees that every single execution of every single x.f  will find x attached to an actual object, rather than void.

How do we do this? I am not going to describe the void-safe mechanism in detail here, referring instead to the online documentation [4], with the warning that it still being improved. But I can give the basic ideas. The original article describing void safety (and giving credit for some of the original ideas) was a keynote at ECOOP in 2005 [5]. Revisiting the solution some years later, I wrote [6]:

Devising, refining and documenting the concept behind the mechanism presented here took a few weeks. The engineering took four years.

That was optimistic. Seven more years later, the “engineering” continues. It is not a matter of ensuring void safety; the mechanism was essentially sound from the beginning. The continued fine-tuning has to do with facilitating the programmer’s task. Any mechanism that avoids bugs  — another example is static typing — buys safety and reliability at a possible cost in expressiveness: you have to prohibit harmful schemes (otherwise you would not avoid any bugs), but you do not want to prohibit useful schemes (otherwise it is very easy to remove bugs: just reject all programs!) or make them to awkward to express. The  “engineering” consists of ever more sophisticated static analysis, through which the compiler can endorse ever more subtle safe cases that simplistic rules would reject. In practice, the difficulties mostly involve the initialization of objects.

While the details can be elaborate, the essential idea is simple: void safety relies on type declarations and static analysis.

The type system introduces a distinction between “attached” and “detachable” types. If you declare a variable p1 as just of type (for example)  PERSON it can never be void: its value will always be a reference to an object of that type; p1 is  “attached”. This is the default. If you want p2 to accept a void value you will declare it as detachable PERSON. Simple compile-time consistency rules support this distinction: you can assign p1 to p2, but not the other way around. They ensure that an “attached” declaration is truthful: at run time, p1 will always be non-void. That is a compiler guarantee.

The static analysis produces more such guarantees, without particular actions from the programmers as long as the code is indeed safe. For example if you write

    if p2 /= Void then p2.f end

we know that things are OK. (Well, under certain conditions. In concurrent programming, for example, we must be sure that no other thread running in parallel can make p2 void between the time we test it and the time we apply f. The rules take care of these conditions.)

The actual definition cannot of course say that “the compiler” will recognize safe cases and reject unsafe ones. We cannot just entrust the safety of our program to the inner workings of a tool (even open-source tool like the existing Eiffel compilers), and besides there is more than just one compiler. Instead the definition of void safety uses a set of clear and precise rules, known as Certified Attachment Patterns, which compilers must implement. The above example is just one such CAP. A formal model backed by mechanized proofs (using the Isabelle/HOL proof tool) provides [3] solid evidence of the soundness of these rules, including the delicate parts about initialization.

Void safety has been there for several years now, and no one who has used it ever wants to go back. Writing void-safe code quickly becomes a second nature (although the conversion to void safety of older, non-void-safe projects is not as painless.)

And what about your code: are you sure it can never produce a null-pointer dereference?

References

[1] On this blog: Those who say code does not matter, 15 April 2014, see here.

[2] C.A.R. Hoare, The billion-dollar mistake, talk abstract, available here.

[3] Alexander Kogtenkov, Void Safety, forthcoming (January 2017) PhD thesis at ETH Zurich.

[4] Void safety documentation at eiffel.org: here.

[5] Bertrand Meyer: Attached Types and their Application to Three Open Problems of Object-Oriented Programming, in ECOOP 2005 (Proceedings of European Conference on Object-Oriented Programming, Edinburgh, 25-29 July 2005), ed. Andrew Black, Lecture Notes in Computer Science 3586, Springer, 2005, pages 1-32, available here.

[6] Bertrand Meyer, Alexander Kogtenkov and Emmanuel Stapf: Avoid a Void: The Eradication of Null Dereferencing, in Reflections on the Work of C.A.R. Hoare, eds. C. B. Jones, A.W. Roscoe and K.R. Wood, Springer, 2010, pages 189-211, available here (follow the link to the PDF).