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.
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".