On Thu, 1 Feb 2007, Michael Poole wrote: > Dave Ketchum writes: > >>>> Are there ways to improve DREs so that they can be made secure and >>>> fully auditable? NIST and the STS do not know how to write testable >>>> requirements to satisfy that the software in a DRE is correct. >> >> >> If they ain't that smart, nor even smart enough to hire needed smarts, >> this should have been admitted, to permit intelligent response. > > How would you write testable security requirements for voting > software? Requirements are generally written as black box tests, > since they guide the design process. In my experience with formal > requirement specifications, the only testable kind of requirement is > of the kind "if X happens, the unit must do Y". You cannot perform > black-box testing for requirements of the form "the unit must not do Y > except as specified in this document" (for example, Y could be to > record a vote for candidate 1) -- you have the usual difficulty with > proving a negative. > > Some companies have done rigorous proofs of software correctness for > applications like money-holding smart cards (including proofs for the > related protocols). This is a more-constrained problem than > electronic voting -- primarily in the complexity of I/O channels. > Proving correctness for the money cards still required a lot of > research in formal methods, and a lot of time and money to apply the > formal methods to the software. The last time I looked at the > literature on software proofs, something on the scale of DRE voting > could not be verified by proof. > > Code inspections and tests written for the code can satisfy security > concerns. It takes a lot of time and money, and can take an enormous > amount of both if the software is not designed for testability from > the start. That kind of thing is why other highly-regulated computer > systems -- including most of what you cited -- cost six figures and up > per unit. (ATM machines are relatively cheap, but the usual arguments > apply about why voting machines are harder than ATM machines.) > >>>> The >>>> use of COTS software in DREs causes additional problems; having, for >>>> example, a large opaque COTS operating system to evaluate in >>>> addition to the voting system software is not feasible. >>>> >> >> Obvious response to this is simpler: If some COTS is too complex to be >> testable at tolerable expense, forbid its use. > > Forbidding use of COTS software requires DRE machine vendors to > implement their own device drivers, user interfaces, network protocol > stack, and whatever else they may need. Considering both development > and testing costs, do you think that will have tolerable cost? > > Michael Poole
There are such standards for software written for aircraft, medical devices, and other such failure-is-not-an-options fields. They go by such uninspiring names as DO-178B, 61508, and they are big bureaucratic nasty standards. They are code-inspection based standards and they are annoying and costly. I work for a company that makes an operating system certified for these standards, and I'm sure we'd love to sell it to voting machine manufacturers. :-) Actually, we should hire a lobbiest to make sure that such a standard requirement gets written into any future amendment of HAVA. Either way our system is effectively one of a very few COTS-like options which would be available to someone trying to build a big, complex and certifiable software system. I would guess that it would cost about $1,000,000 to develop the software for a HAVA compliant election machine in this way. But you do that once every five years, factor it into 10,000+ units, and it's manageable. Oh wait, except that I don't believe in voting machines because they're all a waste of money and I think we should have hand counted paper ballots. But, if society insists on voting machines then I'm going to insist we have good ones. Brian Olson http://bolson.org/ ---- election-methods mailing list - see http://electorama.com/em for list info
