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 ---- election-methods mailing list - see http://electorama.com/em for list info
