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.
"It had only six bugs in its 116,899 lines of code, or .51 bugs per thousands lines of code."
Sounds like someone needs to run this debugger on their calculator.
Finding all POSSIBLE bugs in a software program means traversing all possible paths in the code with all possible inputs. That's a HUGE problem. You can "model" the code using Logic Equations and that helps some but any errors in the conversion from code to logic equations invalidate results. The DoD and NASA have spent many millions on solving this problem over the last 10-12 yrs. When I was at NASA we used several different tools (CodeSurfer, Purify, Lint, Polyspace as I recall) as each tool was better at one thing (i.e memory leaks vs null pointer dereferences). A The complete process took a couple of days to weeks and then human eyes and expertise were still needed to remove false positives. A good site for all the tools out there, old & new is http://spinroot.com/static/. Looks like Coverty might be a good one to look into, as the best I had seen was CodeSurfer. All the good tools I have seen are commercial (NOT open Source) and EXPENSIVE!! I'd love to see a decent open source tool to run as a first pass before applying the other tools. Another point is that these tools are STATIC analysis. Run-Time Analysis is a whole 'nother animal but that area is improving with tools like DTRACE in Solaris.
Here are some links to show the bugs in the Bugzilla database which were turned up by Coverity.
Open Coverity Bugs
All Coverity Bugs
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".