-
Academic Bug-Finding Projects in the Long Run
A number of computer science researchers, including me, have made careers out of creating tools that automate, at least partially, the process of finding bugs in computer programs. Recent work like this can be found in almost any good systemsy conference proceedings such as SOSP, OSDI, ASPLOS, ICSE, or PLDI. Examples go back many years,…
-
Why Isn’t C Memory Safe Yet?
Memory safety errors in C/C++ code include null pointer dereferences, out-of-bounds array accesses, use after free, double free, etc. Taken together, these bugs are extremely costly since they are at the root of a substantial fraction of all security vulnerabilities. At the same time, lots of nice research has been done on memory safety solutions…
-
The Last Mile for a Verification Problem
A few weeks ago my student Lu Zhao defended his PhD thesis and we were lucky to get his external committee member, Magnus Myreen, to attend in person since he was in the USA anyway for a meeting. While he was out here, Magnus gave a talk on some not-yet-published work that is really cool.…
-
When Will Software Verification Matter?
When will average people start to use formally verified software? Let me be clear right from the start that I’m not talking about software that has been subjected to static analysis or about software that implements proved-correct algorithms, but rather about software whose functional correctness has been verified at the implementation level in a way…
-
Software Testing Using Function/Inverse Pairs
One of the hardest problems in software testing is finding convenient, strong oracles—programs that can tell us whether the software under test worked correctly. Weak oracles, such as checking to make sure a program doesn’t crash, are always available, but not always of much use. An example of a strong oracle would be a reference…
-
57 Small Programs that Crash Compilers
It’s not clear how many people enjoy looking at programs that make compilers crash — but this post is for them (and me). Our paper on producing reduced test cases for compiler bugs contained a large table of results for crash bugs. Below are all of C-Reduce’s reduced programs for those bugs. Can we conclude…
-
Integer Overflow Paper
My coauthors and I just finished the final version of our paper about integer overflows in C/C++ programs that’s going to appear at ICSE 2012, a software engineering conference. Basically we made a tool for dynamically finding integer overflows (and related integer undefined behaviors) and used it to look at a lot of software. As…
-
C Puzzle: Double Trouble
I ran into an interesting C program that both of my C oracles (KCC and Frama-C) consider to be well-defined, but that are inconsistently compiled by the current development versions of GCC and Clang on x86-64. The results: [regehr@gamow 1]$ current-gcc -O1 small.c ; ./a.out 1 [regehr@gamow 1]$ current-gcc -O2 small.c ; ./a.out 0 [regehr@gamow…
-
Randomly Testing a Static Analyzer
Static analyzers are intended to find bugs in code, and to show that certain kinds of bugs don’t exist. However, static analyzers are themselves large, complicated programs, leading to a “who watches the watchmen” problem. Pascal Cuoq, one of the people behind the excellent Frama-C analyzer, took it upon himself to run the fuzz-fix cycle…
-
Tricking a Whitebox Testcase Generator
The awesome but apparently discontinued Underhanded C Contest invited us to write C code that looks innocent but acts malicious. Today’s post is an alternate take on the same idea: we don’t really care what the malicious code looks like, but it needs to escape detection by an automated whitebox testcase generator. In some respects…