Slashdot Mirror
Firefox Analyzed for Bugs by Software
eldavojohn writes "In a brief article on CNet, a company named Coverity announced that Firefox is using software to detect flaws in Firefox's source code. Even more interesting is the DHS initiative for Coverity to use this same bug detection software on 40 open source projects." An interesting tidbit from the article: "Most of the 40 programs tested averaged less than one defect per thousand lines of code. The cleanest program was XMMS, a Unix-based multimedia application. It had only six bugs in its 116,899 lines of code, or .51 bugs per thousands lines of code. The buggiest program is the Advanced Maryland Automatic Network Disk Archiver, or AMANDA, a Linux backup application first developed at the University of Maryland. Coverity found 108 bugs in its 88,950 lines of code, or about 1.214 bugs per thousand lines of code." We've covered this before, only now Firefox is actually licensing the Coverity software and using it directly.
That's .051 bugs per thousand lines of code for XMMS, an order of magnitude better.
if you look at the coverity site ( http://scan.coverity.com/ ) you will see that there are already multiple projects who have brought there bugs down to zero. samba being on of the earliest.
If you'd followed the lkml, you could have seen actual patches fixing real bugs, found by Coverity. Just run this search on google: "by coverity" patch site:lkml.org to convince yourself.
The fact that it is impossible to solve the whole problem of program correctness and that false positives will come up doesn't mean that the problem Coverity is adressing isn't usefull.
Regards,
The halting problem is not an issue for program verification. This claim is raised repeatedly by the clueless, and it just isn't an issue.
Yes, you can construct a program that's formally undecideable. It's a hard way to write a bad program. It takes some work, and the resulting program is unlikely to be useful.
Most crash-type and security-hole problems in programs are entirely decidable. This is because almost all subscript calculations are composed from addition, multiplication by constants, and logic operations. Those are totally decideable, and there are good decision algorithms for that problem. Only when multiplication of two variables (both non-constant) is introduced can formal undecidability appear. See Presburger arithmetic.
In fact, halting is decidable for all deterministic machines with finite memory. Either you repeat a previous state, or halt within a finite number of cycles. The decision process may be made arbitrarily hard, but that's not undecidability. True undecidability in the Turing sense requires infinite memory.
Most of the practical problems with program verification come from dealing with interactions between various parts of the program. Containing those interactions well enough that you can localize problems is constraining on the programmer. "Design by contract" languages like Eiffel try to do that, but they're not popular. Retrofitting design by contract into C and C++ has been discussed, but the proposed schemes all have holes you could drive a truck through. A big truck.
Although software work seldom uses proof of correctness techniques, there's a whole industry doing it for hardware. There was a machine-generated formal proof of correctness for the FPU in AMD's K7 processor. AMD thus avoided the "Pentium division bug".
I hope these Coverity guys aren't pompous enough to think that their tool can find ALL bugs in a program
We aren't (I'm a Coverity employee). We find real bugs, and we find false positives (but not too many of those).
Hmm, they should run their tool on its own source code, that would be fun.
We do that regularly.