Developers aim to rid source code of bugs 

Dawson Engler is chief scientist with Coverity and Ben Chelf is chief evangelist. We asked them to elaborate on the advances to source code analysis that they orginally developed at Stanford.

IW: To what extent have security concerns motivated the current wave of interest in source code analysis?

DE: It wasn’t really an impetus for us when we started five or six years ago. And when Intrinsa made the first serious commercial play back in the late 1990s — they were used in a lot of places like Cisco — most of the errors they looked for weren’t security errors. Of course there’s a much clearer monetization story these days. You see a whole bunch of VCs doing static analysis, where before they wouldn’t have touched it at all. Nowadays you can make a much stronger business case to people with checkbooks.

IW: How do you control the high false-positive rate that has made developers so skeptical of lint-like solutions?

BC: Let’s say you know that a parameter passed to a function should never be negative. We can’t always know when it will be negative, but we can often infer that from context. A lot of our work has gone into making sure that when we report an error, we have hard evidence to show you the place we inferred that a certain variable or structure had a value, the place where that value was used incorrectly, and the path between those two points.

IW: How much knowledge of the operating system or the environment is needed for effective analysis?

DE: Very little, fortunately. We’ve checked lots of code that we don’t even understand. You just have to be able to describe the sentence fragment that expresses the rule. So in Linux, for example, one of the rules is that if you’re between cli and sti (disable and enable interrupts), then you can’t call copy_from_user. It’s heavily system-specific, but I just told you the rule, and if you can express that pattern, you’d be all set to go.

BC: You can find bugs in code when the code contradicts itself — for example, if it uses values one way, and checks them in another. We get a lot of mileage out of that. If you contradict yourself in two places, one of them has to be wrong.

DE: It’s often hard to figure out if something about a system is true. But it’s often very much easier to figure out what the programmer believes to be true. So you look for what the programmer believes, and then check that belief system for contradictions. It’s surprisingly effective.