On Thu, 01 Feb 2007 08:10:49 -0500 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.
Ok, demands better be such as can be tested. Without getting too formal: Better have a list of races, with candidates in each. If voter votes for D in race xx: Unless there is a race xx with D; politely reject. If method is Approval, record the vote; done. If method is Plurality and this would be an overvote; politely reject. Record valid Plurality vote; done. Since method is not one of above; CRY. > > 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. Let's take a couple minutes to think of breaking the load into packages such that each package is simple enough to be testable, yet do useful work: M - master computer, which does what needs centralizing such as maintaining master data. T - as many task computers as may be useful, each given a testable task. DVD(s) - owned exclusively by M. K - keyboards - M must have one, some Ts may have their own. Shared memory - M owns and can read and write; Ts can only read. T->M Data - each T can, as permitted, send data up. T-DRE display - this T owns such a display and keyboard. T-disabled - one or more to interface with voters with special needs. Internet access - I would give M such - packaged such that M can prevent unacceptable transmissions. Vote printer - if such is demanded, M owns. Paper ballot scanner: I mention them because absentees and some others would do paper ballots - not clear if this would be part of the package, or separate, but it needs doing. Proving - this must be thorough for M. Less for he Ts, for they are not able to create as much trouble. > > 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.) > Only need about 3 voting machine builders - thus each with enough volume to talk about reasonable pricing. What I wrote above is into designing for testability. Does not require new code for everything - should be usable code available for such as read/write DVDs, etc. > >>>> 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? I am after a middle ground. One thing I was after with the T computers was tasks that could be borrowed from COTS. > > Michael Poole -- [EMAIL PROTECTED] people.clarityconnect.com/webpages3/davek Dave Ketchum 108 Halstead Ave, Owego, NY 13827-1708 607-687-5026 Do to no one what you would not want done to you. If you want peace, work for justice. ---- election-methods mailing list - see http://electorama.com/em for list info