Links

Ben Laurie blathering


Deputy, Delta and Type Checking in C

Another thing I never write about but am very interested in is static analysis. For the non-geeks amongst my readers, static analysis is all about looking at code to see what you can figure out about it. For example, you might try to find input values that cause a buffer overflow. Or you might check to see that strings are correctly escaped before being posted to a Web page (that is, the bug that is at the heart of cross-site scripting has been avoided).

Of course static analysis is usually done by programs, perhaps with the assistance of the programmer, rather than by people, so I am always on the look out for new approaches and new software. Unfortunately, as in many areas of academia, the gap between theory and practice is rather large so I do not find myself exactly overwhelmed with choice.

So far the only thing that I’ve been even a little happy with is Coverity. This still gets it wrong about half the time, but that’s a pretty tolerable ratio given how painful a manual audit would be. In contrast, some of the other tools I have tried over the years have false positive rates well over 99.9%.
Most of them just plain don’t work. Pretty much all of them are not supported. And those that are, like Coverity, cost a fortune.

If I was not a convert to the cause of static analysis, I would despair. As it is, I do occasionally feel tempted to sit down for a year or two and tackle the problem myself but sanity soon prevails and I put that idea off for another decade. So, I was happy to come across Deputy recently, after an animated thread or two on the Robust Open Source mailing list (which I am shocked to discover I have been on since it started, way back in 1998 – archives here and here).

Deputy attempts to provide type safety in C programmes. This is, of course, impossible … but it has a good attempt at it. Although ordinary programmers might not think so, to the academic type safety means enforcing things like array lengths, so our favourite C security problem, the buffer overflow, would be a thing of the past if we had typesafe programs.

Anyone who had read the code I wrote for safe stacks in OpenSSL or the module API in Apache 2.0 will know that I am a big fan of type safety in C. Both of these try to ensure that if you get confused about what type you should be using, you will get a compile-time failure. Unfortunately C provides the programmer with a plethora of ways to both deliberately and accidentally avoid any safety nets you might put out for him. The idea behind Deputy is to make it possible to do the type checking rather more rigorously. In order to allow this, you have to provide deputy with extra clues.

The syntax is a little idiosyncratic, but generally the annotation is quite straightforward, for example

void * (DALLOC(n) malloc)(size_t n);

would tell it that malloc is a memory allocator that returns n bytes of memory. Deputy catches many errors at compile time, but those it can’t it will attempt to catch at runtime instead, by injecting extra code to make sure pointers stay within bounds, for example. I haven’t got that far, though, because my benchmark for these projects is to use them on something real, like OpenSSL. I am pleased to report, though, that Deputy has so far built several OpenSSL source files without driving me completely crazy. But more on that later.

In the course of using Deputy I have been reminded of two things worth mentioning in passing. One is a trick we use in OpenSSL to do type checking. If you want to ensure that something is of type T, then you can write this

(1 ? x : (T)0)

weird, huh? How it works is that both sides of a ? : operator must have the same type, so if x is not of type T, then you will get a compile-time error. Very handy in macros, especially where you are abusing types heavily – for example when you are implementing a generic stack, but you wan to ensure that any particular stack consists only of one type of object (see safestack.h in OpenSSL for an example).

The other is delta. Delta is a very cute tool that cuts down a file with an “interesting” feature to a smaller one with the same feature. For example, suppose (as happened to me) I have an error that I can’t reproduce in a small example. Now what? Delta to the rescue. Today I had a problem with Deputy wanting me to add extra annotation that seems unnecessary. Small examples of essentially the same code did not show the same issue. What do do? Delta reduced the original offending source from 2424 lines to just 18 that produce the same bug. And it did it in about 5 minutes.

For interest, here are the 18 lines

typedef unsigned int __uint32_t;
typedef __uint32_t __size_t;
typedef __size_t size_t;
void *malloc(size_t);
void *memcpy(void * , const void * , size_t);
# 77 "mem.c"
static void * (DALLOC(n) *malloc_func)(size_t n) = malloc;
static void *default_malloc_ex(size_t num, const char *file, int line) {
return malloc_func(num);
}
static void *(*malloc_ex_func)(size_t, const char *file, int line) = default_malloc_ex;
void *CRYPTO_realloc_clean(void *str, int old_len, int num, const char *file, int line) {
void *ret = ((void *)0);
ret=malloc_ex_func(num,file,line);
if(ret) {
memcpy(ret,str,old_len);
}
}

Funnily enough delta was created to assist in debugging another static analysis system, Oink. So far, I’ve never used it for anything else.

1 Comment

  1. “This is, of course, impossible”… I couldn’t help reading that in the ‘voice of the book’. Douglas Adams lives on in geeks everywhere 🙂

    Comment by Pat Patterson — 11 Feb 2008 @ 7:08

RSS feed for comments on this post.

Sorry, the comment form is closed at this time.

Powered by WordPress