Effective Bug Finding

Lightweight bug finders (also known as code scanners) are becoming popular, they scale well and can find simple yet common programming errors. It is now considered a good practice to integrate these tools as part of your development process. The Linux project, for instance, has an automated testing service, known as the Kbuild robot, that runs a few of these code scanners.

In this project, I have carefully studied tens of historical Linux bugs, and I have found that many of these bugs, despite being conceptually simple, were not caught by any code scanning tool. The reason is that, by design, code scanners will find mostly superficial errors. Thus, when bugs span multiple functions, even if simple, they become undetectable by most code scanners. The studied set of historical bugs contained many of such cases.

This PhD thesis proposes a bug-finding technique that is both lightweight and capable of finding deep interprocedural resource manipulation bugs. The core of this technique is a shape-and-effect analysis for C, that enables efficient and scalable inter-procedural reasoning about resource manipulation. This analysis is used to build an abstraction of the program. Then, bugs are found by matching temporal bug-patterns against the control-flow graph of this program abstraction.

I have implemented a proof-of-concept bug finder based on this technique, EBA, and confirmed that it is both scalable and effective at finding bugs. On a benchmark of historical Linux double-lock bugs, EBA was able to detect significantly more bugs, and more complex, than two other baseline tools. EBA was able to analyze nine thousand files of device drivers from Linux-4.7 in less than half an hour, in which time it uncovered five previously unknown bugs. So far, EBA has found more than a dozen double-lock bugs in Linux 4.7--4.10 releases, most of them already confirmed and many fixed.