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

[Michael Poole]

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