The other day Neel Krishnaswami mentioned that he’s going to be teaching the C class at Cambridge in the fall, and asked if I had any advice about that topic. Of course I do! In fact the response got so long that it ended up being a blog post. My main idea is that we […]
Category Archives: Software Correctness
Checking Up on Dataflow Analyses
An important tool for reasoning about programs without running them is dataflow analysis, which can be used to compute facts such as: an integer-valued variable is non-negative at a particular program point a conditional branch always goes one way an indirect write cannot modify a particular array Dataflow facts drive optimizations such as constant propagation […]
Efficient Integer Overflow Checking in LLVM
(Here’s some optional background reading material.) We want fast integer overflow checking. Why? First, if the undefined behavior sanitizers go faster then testing goes faster. Second, when overhead drops below a certain point people will become willing to use UBSan to harden production code against integer overflows. This is already being done in parts of […]
SQLite with a Fine-Toothed Comb
One of the things I’ve been doing at Trust-in-Soft is looking for defects in open-source software. The program I’ve spent the most time with is SQLite: an extremely widely deployed lightweight database. At ~113 KSLOC of pointer-intensive code, SQLite is too big for easy static verification. On the other hand, it has an incredibly impressive […]
The Strict Aliasing Situation is Pretty Bad
I’ll start with a quick review of the strict aliasing rules in C and C++ and then present some less well-known material. Strict Aliasing Compiler optimizations are often shot down by the potential for pointers to be aliases. For example, although we might naively expect a compiler to optimize this function to return zero, that […]
A Variable Argument Hazard
Variable argument functions in C and C++ can be tricky to use correctly, and they typically only get compiler-based type checking for special cases such as printf(). Recently I ran across an entertaining variable argument bug using tis-interpreter. Although I will use code from SQLite to illustrate this bug, this bug has not been found […]
Planning for Disaster
Alan Perlis once said: I think that it’s extraordinarily important that we in computer science keep fun in computing. When it started out, it was an awful lot of fun. Of course, the paying customers got shafted every now and then, and after a while we began to take their complaints seriously. We began to […]
Do Fiddly Buffer Overruns Matter?
by Pascal Cuoq and John Regehr Using tis-interpreter we found a “fiddly” buffer overrun in OpenSSL: it only goes a few bytes out of bounds and the bytes it writes have just been read from the same locations. Fiddly undefined behaviors are common and it can be hard to convince developers to fix them, especially […]
The Problem with Friendly C
I’ll assume you’re familiar with the Proposal for Friendly C and perhaps also Dan Bernstein’s recent call for a Boring C compiler. Both proposals are reactions to creeping exploitation of undefined behaviors as C/C++ compilers get better optimizers. In contrast, we want old code to just keep working, with latent bugs remaining latent. After publishing […]
Reducers are Fuzzers
A test case isn’t just a test case: it lives in the (generally extremely large) space of inputs for the software system you are testing. If we have a test case that triggers a bug, here’s one way we can look at it: The set of test cases triggering a bug is a useful notion […]