I listened to a Freakonomics podcast the other day in which a story about hand-washing at Cedars-Sinai Medical Center was told. It turns out that of all the staff, the doctors had the lowest rate of hand-washing (around 65%, if I recall correctly) in the hospital. This was surprising, since the doctors supposedly have the best education and so should know the most about the dangers of bacterial infection.
The chief of the staff tried different means to increase hygiene. Incentives like gift cards were tried. Then he tried another approach: shame. Doctors had their hands cultured so that they could see the bacteria on their hands. Images of the cultures were even used as a hospital-wide screensaver on the computers.
I listened to this wondering if there are any parallels to formal verification engineers and researchers. Ostensibly, we are the experts on the perils of software bugs. Academic papers often begin with some story about bugs in the wild, motivating the new formal verification technique described therein.
But to what extent do we practice what we preach? How many of us might write a Python script with no unit tests? C/C++ programs without running Lint/CppCheck? Compile without fixing all the -Wall warnings the compiler emits?
These kinds of activities represent the lowest rung of software assurance; they’re the “hand washing of software assurance”, if you will. I’m certainly guilty myself of not always practicing good “software hygiene”. The justifications you might give for failing to do so is that you’re just writing a program for personal use, or you’re writing prototype software, “just for research”. I could imagine doctors telling themselves something similar: “I always scrub thoroughly before a major surgery, but it’s not such a big deal for a simple office visit.” But this justification can become a slippery slope.
There are a few examples in which verification-tool assurance shoots straight for the top. For example, John Harrison verified a model of HOL Light in HOL Light. Filip Maríc verified a SAT solver. But these are more intellectual curiosities than standard operating procedure.
It could be an interesting empirical study to analyze the software quality of open-source formal verification tools to see just how buggy they are (spoiler alert: they are buggy). What I’m interested in are not deep flaws that might be caught via theorem-proving, but simple ones that could be caught with a little better test coverage or lightweight static analysis.
For now, I’m just happy my colleagues’ screensaver isn’t a bug tracker for software that I’ve written.
A Critical Systems Blog 
October 13, 2012 at 2:06 pm |
At some companies people have had to put money in a pot every time they break the build. Some Microsoft books I’ve read (Showstopper! for sure, and some others I believe) have talked about other strategies used for shaming people who insert nasty regressions.
The other day I read Tony Hoare’s “How Did Software Get So Reliable Without Proof?” which is excellent and he reminds us of an important point: Any time a defect is discovered, it’s not enough to fix the defect. Rather, the original root cause should be discovered and addressed. At some level I think easy bugfinding tools encourage quick fixes instead of the sort of deep thinking we should be doing when we find a fault.
As a specific example, there’s a single bugfinding tool that has been used to discover >1500 bugs in Firefox’s JS engine. This makes me think something might be going wrong with that effort, such as insufficient costs of bugs being passed back to offending developers. I’m tempted to say that it doesn’t matter and they’re better off (economically) with this kind of a quick-and-dirty development style, but on the other hand some significant fraction of these bugs is exploitable.
October 13, 2012 at 8:07 pm |
Interesting comments, and thanks for the pointers to Show Stopper! and Tony Hoare’s article.