Sent: Sunday, September 05, 2004 11:33 AM
Subject: Draft statement on uncertified software

This statement is based on my experience in computer science research and in industry. My research area is formal verification of hardware and software systems, which is concerned with finding flaws in system designs or mathematically proving that those designs are correct. I have been publishing research papers in this area for twenty hears.

Based on my professional experience in this area, it is not feasible to ensure that computer systems will function correctly. Computer systems can produce erroneous results because of accidental flaws (called "bugs"), which are inevitable in the design of these complex systems, or because of malicious design features deliberately introduced to produce fraudulent results (often called "malware").

Computerized voting systems are vulnerable to these problems as are any computerized systems. Fraud is particularly worrying in voting because the high stakes in some elections. On purely economic grounds, there is substantial motivation for election fraud because elected officials often control large budgets and make policy that has significant impact on the financial welfare of interested parties. Given these facts, it is obvious that a high level of diligence must be exercised to ensure the absence of bugs and malware in computerized voting systems.

The current certification process requires a review of the design of the system by Independent Testing Authorities (ITAs) to check that the design conforms to the voting standards of the Federal Elections Commission (FEC). This is called the ITA qualification process. Many states, such as the State of Washington, then certify equipment for use in elections based on a report produced by the ITA. Most states do not repeat the ITA inspections and tests, but rely on the ITA report for an evaluation of the system.

HENCE, THE ITA QUALIFICATION PROCESS IS CURRENTLY THE MAJOR DEFENSE AGAINST SYSTEM BUGS AND THE ONLY DEFENSE AGAINST MALWARE. While diligent pre-election testing may catch the very obvious bugs, it is well-known by designers of computer hardware and software that many bugs, including some of the most damaging, are not at all obvious, and that bugs can evade much more extensive testing than is used in pre-election testing. Malware would be intentionally designed to avoid known testing methods.

If software that has not undergone the ITA qualification process, it is appropriate to assume that software can behave arbitrarily during the election, including changing or losing votes, since there are no effective checks or balances to prevent it from doing so.

There is a simple and cost-effective solution to this problem if voter-verified paper ballots are available, as they are in the optical scan systems used in most parts of Washington State. The election can be audited by doing recounts of a random sample of precincts and comparing the totals with those of the machines. The sampling procedure should be devised in consultation with a statistician. If the votes on the paper ballots differ from those on the machines, the problem should be diagnosed. Some problems are easily explained, such as voters marking the ballots in ways that are difficult for optical scanners to read. Problems that are unexplained, or problems that explained by machine error, should trigger successively broader audit, up to and including a full manual count, until there is sufficient confidence in the accuracy of the election outcome.

Indeed, random audits of computerized voting systems should be required even with the ITA process, since that process is inadequate. But without ITA qualification, the need for such audits is even greater.

David Dill

David L. Dill is a Professor of Computer Science and, by courtesy, Electrical Engineering at Stanford University. He has been on the faculty at Stanford since 1987. His primary research interests relate to the theory and application of formal verification techniques to system designs, including hardware, protocols, and software. Prof. Dill's Ph.D. thesis, "Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits" was named as a Distinguished Dissertation by ACM , and published as such by M.I.T. Press in 1988. He was the recipient of an Presidential Young Investigator award from the National Science Foundation in 1988, and a Young Investigator award from the Office of Naval Research in 1991. From July 1995 to September 1996, he was Chief Scientist at 0-In Design Automation. He has received Best Paper awards at International Conference on Computer Design in 1991 and the Design Automation Conference in 1993 and 1998. He was named a Fellow of the IEEE in 2001 for his contributions to verification of circuits and systems.

Prof. Dill is the author of the "Resolution on Electronic Voting", which has been endorsed by many computer technologist as well as political scientists, lawyers, and other individuals. He served on the California Secretary of State's Ad Hoc Committee on Touch Screen Voting, he is on the IEEE P1583 voting standards committee, and is a member of the DRE Citizen's Oversight Committee for Santa Clara County, California. He recently received the Electronic Frontier Foundation's "Pioneer Award" in 2004 for his work on electronic voting. He is the founder of VerifiedVoting.org and the Verified Voting Foundation, non-profit organizations that champion reliable and publicly verifiable elections in the United States. He is also a member of the National Committee for Voting Integrity.