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

[Brian Olson]

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/