[EM] CORRECTING Black box voting repost re how HAVA imploded

[Dave Ketchum]

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
-- 
   davek at clarityconnect.com    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.