Firefox Analyzed for Bugs by Software 226
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.
Math (Score:5, Informative)
Re:not just any software? (Score:3, Informative)
How does this bug detection software work anyway?
this slashdot news is already outdated (Score:5, Informative)
Re:not just any software? (Score:3, Informative)
Bugzilla is a issue tracking software; it's useful only after you've already found a bug. The only other bug-related tool they use is the FullCircle crash reporter thingy, again, after-the-fact thing. This is different - this tool finds flaws from the source code automatically.
Which type of bugs? (Score:3, Informative)
Computer != Turing machine (Score:3, Informative)
Unless the program's domain is restricted to context-sensitive languages. In fact, it is impossible for a computer to try to decide anything more general than a context-sensitive language because anything bigger requires the resources of a Turing machine, which has infinite memory. Computers implementable in a finite amount of matter are equivalent to linear bounded automata [wikipedia.org], not Turing machines.
AMANDA _is_ in active development (Score:3, Informative)
In defense of amanda (Score:3, Informative)
Thats not to say that as new features are added, new bugs haven't been too, but to actually call amanda a truely buggy application does stretch this users belief a wee bit. I'm currently running a 20060424 dated snapshot of the 2.5.0 tree, with no hiccups at all.
--
Cheers, Gene
Re:this slashdot news is already outdated (Score:3, Informative)
--
Cheers, Gene
Re:I dislike the idea of Coverity (Score:5, Informative)
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,
Re:If this is the same (Score:1, Informative)
Re:Math (Score:5, Informative)
VMware Uses It Too (Score:1, Informative)
The halting problem is not an issue (Score:5, Informative)
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 [wikipedia.org].
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. [onr.com] AMD thus avoided the "Pentium division bug".
Mozilla developers' comments (Score:3, Informative)
Re:not just any software? (Score:1, Informative)
Re:Errr... (Score:5, Informative)
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.
Re:If this is the same (Score:3, Informative)
That's true. It's impossible to have both (all bugs and no false positives, soundness and completeness), and even one of them is usually extremely expensive (computationally).
It helps to follow "good practices" and be more precautious
That's not true of Coverity (disclaimer: I work for them), we find real bugs. You can see a couple examples here [slashdot.org]. The engineers are usually the ones excited about it, once they've seen the bugs.
Re:If this is the same (Score:4, Informative)
Corrected link [coverity.com]. Unfortunately there are only 2 examples since there are trade secrets involved with bug reports.
This might look like a slashvertisement, but I didn't submit the original story (which does pick up on a press release)
Re:Math (Score:3, Informative)
Re:Math (Score:3, Informative)
Music On Console [daper.net] does everything I need :) What's more universal to a *NIX system than the console?